:: INTEGRA2 semantic presentation
begin
theorem :: INTEGRA2:1
for A being non empty closed_interval Subset of REAL
for x being real number holds
( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for x being real number holds
( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )
let x be real number ; ::_thesis: ( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )
hereby ::_thesis: ( lower_bound A <= x & x <= upper_bound A implies x in A )
assume x in A ; ::_thesis: ( lower_bound A <= x & x <= upper_bound A )
then x in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then x in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by RCOMP_1:def_1;
then ex a being Real st
( a = x & lower_bound A <= a & a <= upper_bound A ) ;
hence ( lower_bound A <= x & x <= upper_bound A ) ; ::_thesis: verum
end;
assume A1: ( lower_bound A <= x & x <= upper_bound A ) ; ::_thesis: x in A
x is Real by XREAL_0:def_1;
then x in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by A1;
then x in [.(lower_bound A),(upper_bound A).] by RCOMP_1:def_1;
hence x in A by INTEGRA1:4; ::_thesis: verum
end;
definition
let IT be FinSequence of REAL ;
attrIT is non-decreasing means :Def1: :: INTEGRA2:def 1
for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n <= IT . (n + 1);
end;
:: deftheorem Def1 defines non-decreasing INTEGRA2:def_1_:_
for IT being FinSequence of REAL holds
( IT is non-decreasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n <= IT . (n + 1) );
registration
cluster Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing for FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st b1 is non-decreasing
proof
take f = <*> REAL; ::_thesis: f is non-decreasing
let n be Element of NAT ; :: according to INTEGRA2:def_1 ::_thesis: ( n in dom f & n + 1 in dom f implies f . n <= f . (n + 1) )
assume that
A1: n in dom f and
n + 1 in dom f ; ::_thesis: f . n <= f . (n + 1)
thus f . n <= f . (n + 1) by A1; ::_thesis: verum
end;
end;
theorem :: INTEGRA2:2
for p being non-decreasing FinSequence of REAL
for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
p . i <= p . j
proof
let p be non-decreasing FinSequence of REAL ; ::_thesis: for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
p . i <= p . j
let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & i <= j implies p . i <= p . j )
assume A1: i in dom p ; ::_thesis: ( not j in dom p or not i <= j or p . i <= p . j )
defpred S1[ Element of NAT ] means for i, j being Element of NAT st j = i + $1 & i in dom p & j in dom p holds
p . i <= p . j;
assume A2: j in dom p ; ::_thesis: ( not i <= j or p . i <= p . j )
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
S1[k + 1]
proof
let i, j be Element of NAT ; ::_thesis: ( j = i + (k + 1) & i in dom p & j in dom p implies p . i <= p . j )
reconsider l = i + k as Element of NAT ;
A5: 0 <= k by NAT_1:2;
assume j = i + (k + 1) ; ::_thesis: ( not i in dom p or not j in dom p or p . i <= p . j )
then A6: j = l + 1 ;
assume A7: i in dom p ; ::_thesis: ( not j in dom p or p . i <= p . j )
then 1 <= i by FINSEQ_3:25;
then A8: 1 + 0 <= l by A5, XREAL_1:7;
assume A9: j in dom p ; ::_thesis: p . i <= p . j
then j <= len p by FINSEQ_3:25;
then l < len p by A6, NAT_1:13;
then A10: l in dom p by A8, FINSEQ_3:25;
then A11: p . i <= p . l by A4, A7;
p . l <= p . j by A9, A6, A10, Def1;
hence p . i <= p . j by A11, XXREAL_0:2; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A12: S1[ 0 ] ;
A13: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A12, A3);
assume i <= j ; ::_thesis: p . i <= p . j
then consider n being Nat such that
A14: j = i + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
j = i + n by A14;
hence p . i <= p . j by A1, A2, A13; ::_thesis: verum
end;
theorem :: INTEGRA2:3
for p being FinSequence of REAL ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent
proof
let p be FinSequence of REAL ; ::_thesis: ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent
consider q being non-increasing FinSequence of REAL such that
A1: p,q are_fiberwise_equipotent by RFINSEQ:22;
for n being Element of NAT st n in dom (Rev q) & n + 1 in dom (Rev q) holds
(Rev q) . n <= (Rev q) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: ( n in dom (Rev q) & n + 1 in dom (Rev q) implies (Rev q) . n <= (Rev q) . (n + 1) )
assume that
A2: n in dom (Rev q) and
A3: n + 1 in dom (Rev q) ; ::_thesis: (Rev q) . n <= (Rev q) . (n + 1)
(Rev q) . n <= (Rev q) . (n + 1)
proof
n in Seg (len (Rev q)) by A2, FINSEQ_1:def_3;
then 1 <= n by FINSEQ_1:1;
then n - 1 >= 0 by XREAL_1:48;
then (len q) + 0 <= (len q) + (n - 1) by XREAL_1:7;
then A4: (len q) - (n - 1) <= len q by XREAL_1:20;
n in Seg (len (Rev q)) by A2, FINSEQ_1:def_3;
then n in Seg (len q) by FINSEQ_5:def_3;
then n <= len q by FINSEQ_1:1;
then consider m being Nat such that
A5: len q = n + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
( m + 1 = ((len q) - n) + 1 & 1 <= ((len q) - n) + 1 ) by A5, NAT_1:11;
then ((len q) - n) + 1 in Seg (len q) by A4, FINSEQ_1:1;
then A6: ((len q) - n) + 1 in dom q by FINSEQ_1:def_3;
set x = (Rev q) . n;
set y = (Rev q) . (n + 1);
A7: ((len q) - (n + 1)) + 1 = (len q) - n ;
len q <= (len q) + n by NAT_1:11;
then A8: ((len q) - (n + 1)) + 1 <= len q by A7, XREAL_1:20;
n + 1 in Seg (len (Rev q)) by A3, FINSEQ_1:def_3;
then n + 1 in Seg (len q) by FINSEQ_5:def_3;
then n + 1 <= len q by FINSEQ_1:1;
then 1 <= ((len q) - (n + 1)) + 1 by A7, XREAL_1:19;
then ((len q) - (n + 1)) + 1 in Seg (len q) by A5, A8, FINSEQ_1:1;
then A9: ((len q) - (n + 1)) + 1 in dom q by FINSEQ_1:def_3;
( (Rev q) . n = q . (((len q) - n) + 1) & (Rev q) . (n + 1) = q . (((len q) - (n + 1)) + 1) ) by A2, A3, FINSEQ_5:def_3;
hence (Rev q) . n <= (Rev q) . (n + 1) by A6, A9, RFINSEQ:def_3; ::_thesis: verum
end;
hence (Rev q) . n <= (Rev q) . (n + 1) ; ::_thesis: verum
end;
then reconsider r = Rev q as non-decreasing FinSequence of REAL by Def1;
take r ; ::_thesis: p,r are_fiberwise_equipotent
p, Rev q are_fiberwise_equipotent
proof
defpred S1[ Element of NAT ] means for p being FinSequence of REAL
for q being non-increasing FinSequence of REAL st len p = $1 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent ;
A10: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; ::_thesis: S1[k + 1]
S1[k + 1]
proof
let p be FinSequence of REAL ; ::_thesis: for q being non-increasing FinSequence of REAL st len p = k + 1 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent
let q be non-increasing FinSequence of REAL ; ::_thesis: ( len p = k + 1 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent )
consider q1 being non-increasing FinSequence of REAL such that
A12: p,q1 are_fiberwise_equipotent by RFINSEQ:22;
reconsider q1k = q1 | k as non-increasing FinSequence of REAL by RFINSEQ:20;
A13: (Rev q1k) ^ <*(q1 . (k + 1))*>,<*(q1 . (k + 1))*> ^ (Rev q1k) are_fiberwise_equipotent by RFINSEQ:2;
assume A14: len p = k + 1 ; ::_thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent )
then A15: len q1 = k + 1 by A12, RFINSEQ:3;
len p = len q1 by A12, RFINSEQ:3;
then len (q1 | k) = k by A14, FINSEQ_1:59, NAT_1:11;
then q1 | k, Rev q1k are_fiberwise_equipotent by A11;
then (q1 | k) ^ <*(q1 . (k + 1))*>,(Rev q1k) ^ <*(q1 . (k + 1))*> are_fiberwise_equipotent by RFINSEQ:1;
then q1,(Rev q1k) ^ <*(q1 . (k + 1))*> are_fiberwise_equipotent by A15, RFINSEQ:7;
then A16: q1,<*(q1 . (k + 1))*> ^ (Rev q1k) are_fiberwise_equipotent by A13, CLASSES1:76;
A17: <*(q1 . (k + 1))*> ^ (Rev q1k) = Rev ((q1 | k) ^ <*(q1 . (k + 1))*>) by FINSEQ_5:63
.= Rev q1 by A15, RFINSEQ:7 ;
assume p,q are_fiberwise_equipotent ; ::_thesis: p, Rev q are_fiberwise_equipotent
then q = q1 by A12, CLASSES1:76, RFINSEQ:23;
hence p, Rev q are_fiberwise_equipotent by A12, A16, A17, CLASSES1:76; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A18: len p = len p ;
A19: S1[ 0 ]
proof
let p be FinSequence of REAL ; ::_thesis: for q being non-increasing FinSequence of REAL st len p = 0 & p,q are_fiberwise_equipotent holds
p, Rev q are_fiberwise_equipotent
let q be non-increasing FinSequence of REAL ; ::_thesis: ( len p = 0 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent )
assume A20: len p = 0 ; ::_thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent )
assume p,q are_fiberwise_equipotent ; ::_thesis: p, Rev q are_fiberwise_equipotent
then len q = 0 by A20, RFINSEQ:3;
then len (Rev q) = 0 by FINSEQ_5:def_3;
then Rev q = {} ;
then A21: rng (Rev q) = {} ;
p = {} by A20;
then A22: rng p = {} ;
for x being set holds card (Coim (p,x)) = card (Coim ((Rev q),x))
proof
let x be set ; ::_thesis: card (Coim (p,x)) = card (Coim ((Rev q),x))
card (p " {x}) = 0 by A22, CARD_1:27, FUNCT_1:72;
hence card (Coim (p,x)) = card (Coim ((Rev q),x)) by A21, CARD_1:27, FUNCT_1:72; ::_thesis: verum
end;
hence p, Rev q are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A19, A10);
hence p, Rev q are_fiberwise_equipotent by A1, A18; ::_thesis: verum
end;
hence p,r are_fiberwise_equipotent ; ::_thesis: verum
end;
theorem :: INTEGRA2:4
for D being non empty set
for f being FinSequence of D
for k1, k2, k3 being Element of NAT st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for k1, k2, k3 being Element of NAT st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)
let f be FinSequence of D; ::_thesis: for k1, k2, k3 being Element of NAT st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)
let k1, k2, k3 be Element of NAT ; ::_thesis: ( 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 implies (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3) )
assume that
A1: 1 <= k1 and
A2: k3 <= len f and
A3: k1 <= k2 and
A4: k2 < k3 ; ::_thesis: (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)
A5: k2 <= len f by A2, A4, XXREAL_0:2;
then A6: k1 <= len f by A3, XXREAL_0:2;
( 1 <= k2 & k2 <= len f ) by A1, A2, A3, A4, XXREAL_0:2;
then A7: len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A1, A3, A6, FINSEQ_6:118
.= (k2 - k1) + 1 by A3, XREAL_1:233 ;
A8: 1 <= k2 by A1, A3, XXREAL_0:2;
then A9: 1 <= k3 by A4, XXREAL_0:2;
A10: k1 < k3 by A3, A4, XXREAL_0:2;
A11: 1 <= k2 + 1 by A8, NAT_1:13;
A12: k2 + 1 <= k3 by A4, NAT_1:13;
then k2 + 1 <= len f by A2, XXREAL_0:2;
then A13: len (mid (f,(k2 + 1),k3)) = (k3 -' (k2 + 1)) + 1 by A2, A9, A12, A11, FINSEQ_6:118
.= (k3 - (k2 + 1)) + 1 by A12, XREAL_1:233
.= k3 - k2 ;
then A14: len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) = ((k2 - k1) + 1) + (k3 - k2) by A7, FINSEQ_1:22
.= (k3 - k1) + 1 ;
A15: 1 <= k2 + 1 by A8, NAT_1:13;
A16: for k being Nat st 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) holds
((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) implies ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k )
assume A17: ( 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) ) ; ::_thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k
then k in Seg (len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)))) by FINSEQ_1:1;
then A18: k in dom ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) by FINSEQ_1:def_3;
now__::_thesis:_((mid_(f,k1,k2))_^_(mid_(f,(k2_+_1),k3)))_._k_=_(mid_(f,k1,k3))_._k
percases ( k in dom (mid (f,k1,k2)) or ex n being Nat st
( n in dom (mid (f,(k2 + 1),k3)) & k = (len (mid (f,k1,k2))) + n ) ) by A18, FINSEQ_1:25;
supposeA19: k in dom (mid (f,k1,k2)) ; ::_thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k
then A20: k in Seg (len (mid (f,k1,k2))) by FINSEQ_1:def_3;
then A21: 1 <= k by FINSEQ_1:1;
A22: k <= (k2 - k1) + 1 by A7, A20, FINSEQ_1:1;
k2 - k1 <= k3 - k1 by A4, XREAL_1:9;
then (k2 - k1) + 1 <= (k3 - k1) + 1 by XREAL_1:6;
then A23: k <= (k3 - k1) + 1 by A22, XXREAL_0:2;
((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k2)) . k by A19, FINSEQ_1:def_7
.= f . ((k - 1) + k1) by A1, A3, A5, A19, A21, A22, FINSEQ_6:122 ;
hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k by A1, A2, A10, A19, A21, A23, FINSEQ_6:122; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom (mid (f,(k2 + 1),k3)) & k = (len (mid (f,k1,k2))) + n ) ; ::_thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k
then consider n being Nat such that
A24: n in dom (mid (f,(k2 + 1),k3)) and
A25: k = (len (mid (f,k1,k2))) + n ;
A26: (mid (f,k1,k3)) . k = f . ((((k2 - (k1 - 1)) + n) + k1) - 1) by A1, A2, A10, A7, A14, A17, A25, FINSEQ_6:122
.= f . (n + k2) ;
n in Seg (len (mid (f,(k2 + 1),k3))) by A24, FINSEQ_1:def_3;
then A27: ( 1 <= n & n <= (k3 - (k2 + 1)) + 1 ) by A13, FINSEQ_1:1;
((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,(k2 + 1),k3)) . n by A24, A25, FINSEQ_1:def_7
.= f . ((n + (k2 + 1)) - 1) by A2, A15, A12, A24, A27, FINSEQ_6:122
.= f . ((n + k2) + 0) ;
hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k by A26; ::_thesis: verum
end;
end;
end;
hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k ; ::_thesis: verum
end;
len (mid (f,k1,k3)) = (k3 -' k1) + 1 by A1, A2, A6, A9, A10, FINSEQ_6:118
.= (k3 - k1) + 1 by A3, A4, XREAL_1:233, XXREAL_0:2 ;
hence (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3) by A14, A16, FINSEQ_1:14; ::_thesis: verum
end;
begin
definition
let A be real-membered set ;
let x be real number ;
:: original: **
redefine funcx ** A -> Subset of REAL;
coherence
x ** A is Subset of REAL by MEMBERED:3;
end;
theorem :: INTEGRA2:5
for X, Y being non empty set
for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds
(f | Y) | Y is bounded_above
proof
let X, Y be non empty set ; ::_thesis: for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds
(f | Y) | Y is bounded_above
let f be PartFunc of X,REAL; ::_thesis: ( f | X is bounded_above & Y c= X implies (f | Y) | Y is bounded_above )
assume f | X is bounded_above ; ::_thesis: ( not Y c= X or (f | Y) | Y is bounded_above )
then consider a being real number such that
A1: for x being set st x in X /\ (dom f) holds
a >= f . x by RFUNCT_1:70;
assume A2: Y c= X ; ::_thesis: (f | Y) | Y is bounded_above
for x being set st x in Y /\ (dom (f | Y)) holds
a >= (f | Y) . x
proof
let x be set ; ::_thesis: ( x in Y /\ (dom (f | Y)) implies a >= (f | Y) . x )
A3: (dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26;
assume x in Y /\ (dom (f | Y)) ; ::_thesis: a >= (f | Y) . x
then A4: x in dom (f | Y) by XBOOLE_0:def_4;
then x in (dom f) /\ Y by RELAT_1:61;
then a >= f . x by A1, A3;
hence a >= (f | Y) . x by A4, FUNCT_1:47; ::_thesis: verum
end;
hence (f | Y) | Y is bounded_above by RFUNCT_1:70; ::_thesis: verum
end;
theorem :: INTEGRA2:6
for X, Y being non empty set
for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds
(f | Y) | Y is bounded_below
proof
let X, Y be non empty set ; ::_thesis: for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds
(f | Y) | Y is bounded_below
let f be PartFunc of X,REAL; ::_thesis: ( f | X is bounded_below & Y c= X implies (f | Y) | Y is bounded_below )
assume f | X is bounded_below ; ::_thesis: ( not Y c= X or (f | Y) | Y is bounded_below )
then consider a being real number such that
A1: for x being set st x in X /\ (dom f) holds
f . x >= a by RFUNCT_1:71;
assume A2: Y c= X ; ::_thesis: (f | Y) | Y is bounded_below
for x being set st x in Y /\ (dom (f | Y)) holds
(f | Y) . x >= a
proof
let x be set ; ::_thesis: ( x in Y /\ (dom (f | Y)) implies (f | Y) . x >= a )
A3: (dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26;
assume x in Y /\ (dom (f | Y)) ; ::_thesis: (f | Y) . x >= a
then A4: x in dom (f | Y) by XBOOLE_0:def_4;
then x in (dom f) /\ Y by RELAT_1:61;
then a <= f . x by A1, A3;
hence (f | Y) . x >= a by A4, FUNCT_1:47; ::_thesis: verum
end;
hence (f | Y) | Y is bounded_below by RFUNCT_1:71; ::_thesis: verum
end;
theorem :: INTEGRA2:7
for X being real-membered set
for a being real number holds
( X is empty iff a ** X is empty ) ;
theorem Th8: :: INTEGRA2:8
for r being Real
for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X }
proof
let r be Real; ::_thesis: for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X }
let X be Subset of REAL; ::_thesis: r ** X = { (r * x) where x is Real : x in X }
thus r ** X c= { (r * x) where x is Real : x in X } :: according to XBOOLE_0:def_10 ::_thesis: { (r * x) where x is Real : x in X } c= r ** X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in r ** X or y in { (r * x) where x is Real : x in X } )
assume y in r ** X ; ::_thesis: y in { (r * x) where x is Real : x in X }
then consider z being Element of ExtREAL such that
A1: ( y = r * z & z in X ) by MEMBER_1:188;
reconsider z1 = z as Element of REAL by A1;
y = r * z1 by A1, XXREAL_3:def_5;
hence y in { (r * x) where x is Real : x in X } by A1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (r * x) where x is Real : x in X } or y in r ** X )
assume y in { (r * x) where x is Real : x in X } ; ::_thesis: y in r ** X
then consider z being Real such that
A2: ( y = r * z & z in X ) ;
thus y in r ** X by A2, MEMBER_1:193; ::_thesis: verum
end;
theorem :: INTEGRA2:9
for r being Real
for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
r ** X is bounded_above
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
r ** X is bounded_above
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & 0 <= r implies r ** X is bounded_above )
assume that
A1: X is bounded_above and
A2: 0 <= r ; ::_thesis: r ** X is bounded_above
consider b being real number such that
A3: b is UpperBound of X by A1, XXREAL_2:def_10;
A4: for x being real number st x in X holds
x <= b by A3, XXREAL_2:def_1;
r * b is UpperBound of r ** X
proof
let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not y in r ** X or y <= r * b )
assume y in r ** X ; ::_thesis: y <= r * b
then y in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A5: y = r * x and
A6: x in X ;
x <= b by A4, A6;
hence y <= r * b by A2, A5, XREAL_1:64; ::_thesis: verum
end;
hence r ** X is bounded_above by XXREAL_2:def_10; ::_thesis: verum
end;
theorem :: INTEGRA2:10
for r being Real
for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
r ** X is bounded_below
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
r ** X is bounded_below
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & r <= 0 implies r ** X is bounded_below )
assume that
A1: X is bounded_above and
A2: r <= 0 ; ::_thesis: r ** X is bounded_below
consider b being real number such that
A3: b is UpperBound of X by A1, XXREAL_2:def_10;
A4: for x being real number st x in X holds
x <= b by A3, XXREAL_2:def_1;
r * b is LowerBound of r ** X
proof
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not y in r ** X or r * b <= y )
assume y in r ** X ; ::_thesis: r * b <= y
then y in { (r * x) where x is Real : x in X } by Th8;
then ex x being Real st
( y = r * x & x in X ) ;
hence r * b <= y by A2, A4, XREAL_1:65; ::_thesis: verum
end;
hence r ** X is bounded_below by XXREAL_2:def_9; ::_thesis: verum
end;
theorem :: INTEGRA2:11
for r being Real
for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
r ** X is bounded_below
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
r ** X is bounded_below
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & 0 <= r implies r ** X is bounded_below )
assume that
A1: X is bounded_below and
A2: 0 <= r ; ::_thesis: r ** X is bounded_below
consider b being real number such that
A3: b is LowerBound of X by A1, XXREAL_2:def_9;
A4: for x being real number st x in X holds
b <= x by A3, XXREAL_2:def_2;
r * b is LowerBound of r ** X
proof
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not y in r ** X or r * b <= y )
assume y in r ** X ; ::_thesis: r * b <= y
then y in { (r * x) where x is Real : x in X } by Th8;
then ex x being Real st
( y = r * x & x in X ) ;
hence r * b <= y by A2, A4, XREAL_1:64; ::_thesis: verum
end;
hence r ** X is bounded_below by XXREAL_2:def_9; ::_thesis: verum
end;
theorem :: INTEGRA2:12
for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
r ** X is bounded_above
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
r ** X is bounded_above
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & r <= 0 implies r ** X is bounded_above )
assume that
A1: X is bounded_below and
A2: r <= 0 ; ::_thesis: r ** X is bounded_above
consider b being real number such that
A3: b is LowerBound of X by A1, XXREAL_2:def_9;
A4: for x being real number st x in X holds
b <= x by A3, XXREAL_2:def_2;
r * b is UpperBound of r ** X
proof
let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not y in r ** X or y <= r * b )
assume y in r ** X ; ::_thesis: y <= r * b
then y in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A5: y = r * x and
A6: x in X ;
b <= x by A4, A6;
hence y <= r * b by A2, A5, XREAL_1:65; ::_thesis: verum
end;
hence r ** X is bounded_above by XXREAL_2:def_10; ::_thesis: verum
end;
theorem Th13: :: INTEGRA2:13
for r being Real
for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
upper_bound (r ** X) = r * (upper_bound X)
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
upper_bound (r ** X) = r * (upper_bound X)
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & 0 <= r implies upper_bound (r ** X) = r * (upper_bound X) )
assume that
A1: X is bounded_above and
A2: 0 <= r ; ::_thesis: upper_bound (r ** X) = r * (upper_bound X)
A3: for a being real number st a in r ** X holds
a <= r * (upper_bound X)
proof
let a be real number ; ::_thesis: ( a in r ** X implies a <= r * (upper_bound X) )
assume a in r ** X ; ::_thesis: a <= r * (upper_bound X)
then a in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A4: a = r * x and
A5: x in X ;
x <= upper_bound X by A1, A5, SEQ_4:def_1;
hence a <= r * (upper_bound X) by A2, A4, XREAL_1:64; ::_thesis: verum
end;
for b being real number st ( for a being real number st a in r ** X holds
a <= b ) holds
r * (upper_bound X) <= b
proof
consider x being Real such that
A6: x in X by SUBSET_1:4;
let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds
a <= b ) implies r * (upper_bound X) <= b )
assume A7: for a being real number st a in r ** X holds
a <= b ; ::_thesis: r * (upper_bound X) <= b
r * x in { (r * y) where y is Real : y in X } by A6;
then A8: r * x in r ** X by Th8;
now__::_thesis:_r_*_(upper_bound_X)_<=_b
percases ( r = 0 or r > 0 ) by A2;
suppose r = 0 ; ::_thesis: r * (upper_bound X) <= b
hence r * (upper_bound X) <= b by A7, A8; ::_thesis: verum
end;
supposeA9: r > 0 ; ::_thesis: r * (upper_bound X) <= b
for z being real number st z in X holds
z <= b / r
proof
let z be real number ; ::_thesis: ( z in X implies z <= b / r )
assume z in X ; ::_thesis: z <= b / r
then r * z in { (r * y) where y is Real : y in X } ;
then r * z in r ** X by Th8;
hence z <= b / r by A7, A9, XREAL_1:77; ::_thesis: verum
end;
then upper_bound X <= b / r by SEQ_4:45;
then r * (upper_bound X) <= (b / r) * r by A9, XREAL_1:64;
hence r * (upper_bound X) <= b by A9, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence r * (upper_bound X) <= b ; ::_thesis: verum
end;
hence upper_bound (r ** X) = r * (upper_bound X) by A3, SEQ_4:46; ::_thesis: verum
end;
theorem Th14: :: INTEGRA2:14
for r being Real
for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
lower_bound (r ** X) = r * (upper_bound X)
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
lower_bound (r ** X) = r * (upper_bound X)
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & r <= 0 implies lower_bound (r ** X) = r * (upper_bound X) )
assume that
A1: X is bounded_above and
A2: r <= 0 ; ::_thesis: lower_bound (r ** X) = r * (upper_bound X)
A3: for a being real number st a in r ** X holds
r * (upper_bound X) <= a
proof
let a be real number ; ::_thesis: ( a in r ** X implies r * (upper_bound X) <= a )
assume a in r ** X ; ::_thesis: r * (upper_bound X) <= a
then a in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A4: a = r * x and
A5: x in X ;
x <= upper_bound X by A1, A5, SEQ_4:def_1;
hence r * (upper_bound X) <= a by A2, A4, XREAL_1:65; ::_thesis: verum
end;
for b being real number st ( for a being real number st a in r ** X holds
a >= b ) holds
r * (upper_bound X) >= b
proof
consider x being Real such that
A6: x in X by SUBSET_1:4;
let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds
a >= b ) implies r * (upper_bound X) >= b )
assume A7: for a being real number st a in r ** X holds
a >= b ; ::_thesis: r * (upper_bound X) >= b
r * x in { (r * y) where y is Real : y in X } by A6;
then A8: r * x in r ** X by Th8;
now__::_thesis:_r_*_(upper_bound_X)_>=_b
percases ( r = 0 or r < 0 ) by A2;
suppose r = 0 ; ::_thesis: r * (upper_bound X) >= b
hence r * (upper_bound X) >= b by A7, A8; ::_thesis: verum
end;
supposeA9: r < 0 ; ::_thesis: r * (upper_bound X) >= b
for z being real number st z in X holds
z <= b / r
proof
let z be real number ; ::_thesis: ( z in X implies z <= b / r )
assume z in X ; ::_thesis: z <= b / r
then r * z in { (r * y) where y is Real : y in X } ;
then r * z in r ** X by Th8;
hence z <= b / r by A7, A9, XREAL_1:80; ::_thesis: verum
end;
then upper_bound X <= b / r by SEQ_4:45;
then r * (upper_bound X) >= (b / r) * r by A9, XREAL_1:65;
hence r * (upper_bound X) >= b by A9, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence r * (upper_bound X) >= b ; ::_thesis: verum
end;
hence lower_bound (r ** X) = r * (upper_bound X) by A3, SEQ_4:44; ::_thesis: verum
end;
theorem Th15: :: INTEGRA2:15
for r being Real
for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
lower_bound (r ** X) = r * (lower_bound X)
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
lower_bound (r ** X) = r * (lower_bound X)
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & 0 <= r implies lower_bound (r ** X) = r * (lower_bound X) )
assume that
A1: X is bounded_below and
A2: 0 <= r ; ::_thesis: lower_bound (r ** X) = r * (lower_bound X)
A3: for a being real number st a in r ** X holds
r * (lower_bound X) <= a
proof
let a be real number ; ::_thesis: ( a in r ** X implies r * (lower_bound X) <= a )
assume a in r ** X ; ::_thesis: r * (lower_bound X) <= a
then a in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A4: a = r * x and
A5: x in X ;
lower_bound X <= x by A1, A5, SEQ_4:def_2;
hence r * (lower_bound X) <= a by A2, A4, XREAL_1:64; ::_thesis: verum
end;
for b being real number st ( for a being real number st a in r ** X holds
a >= b ) holds
r * (lower_bound X) >= b
proof
consider x being Real such that
A6: x in X by SUBSET_1:4;
let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds
a >= b ) implies r * (lower_bound X) >= b )
assume A7: for a being real number st a in r ** X holds
a >= b ; ::_thesis: r * (lower_bound X) >= b
r * x in { (r * y) where y is Real : y in X } by A6;
then A8: r * x in r ** X by Th8;
now__::_thesis:_r_*_(lower_bound_X)_>=_b
percases ( r = 0 or r > 0 ) by A2;
suppose r = 0 ; ::_thesis: r * (lower_bound X) >= b
hence r * (lower_bound X) >= b by A7, A8; ::_thesis: verum
end;
supposeA9: r > 0 ; ::_thesis: r * (lower_bound X) >= b
for z being real number st z in X holds
z >= b / r
proof
let z be real number ; ::_thesis: ( z in X implies z >= b / r )
assume z in X ; ::_thesis: z >= b / r
then r * z in { (r * y) where y is Real : y in X } ;
then r * z in r ** X by Th8;
hence z >= b / r by A7, A9, XREAL_1:79; ::_thesis: verum
end;
then lower_bound X >= b / r by SEQ_4:43;
then r * (lower_bound X) >= (b / r) * r by A9, XREAL_1:64;
hence r * (lower_bound X) >= b by A9, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence r * (lower_bound X) >= b ; ::_thesis: verum
end;
hence lower_bound (r ** X) = r * (lower_bound X) by A3, SEQ_4:44; ::_thesis: verum
end;
theorem Th16: :: INTEGRA2:16
for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
upper_bound (r ** X) = r * (lower_bound X)
proof
let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
upper_bound (r ** X) = r * (lower_bound X)
let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & r <= 0 implies upper_bound (r ** X) = r * (lower_bound X) )
assume that
A1: X is bounded_below and
A2: r <= 0 ; ::_thesis: upper_bound (r ** X) = r * (lower_bound X)
A3: for a being real number st a in r ** X holds
r * (lower_bound X) >= a
proof
let a be real number ; ::_thesis: ( a in r ** X implies r * (lower_bound X) >= a )
assume a in r ** X ; ::_thesis: r * (lower_bound X) >= a
then a in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A4: a = r * x and
A5: x in X ;
lower_bound X <= x by A1, A5, SEQ_4:def_2;
hence r * (lower_bound X) >= a by A2, A4, XREAL_1:65; ::_thesis: verum
end;
for b being real number st ( for a being real number st a in r ** X holds
a <= b ) holds
r * (lower_bound X) <= b
proof
consider x being Real such that
A6: x in X by SUBSET_1:4;
let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds
a <= b ) implies r * (lower_bound X) <= b )
assume A7: for a being real number st a in r ** X holds
a <= b ; ::_thesis: r * (lower_bound X) <= b
r * x in { (r * y) where y is Real : y in X } by A6;
then A8: r * x in r ** X by Th8;
now__::_thesis:_r_*_(lower_bound_X)_<=_b
percases ( r = 0 or r < 0 ) by A2;
suppose r = 0 ; ::_thesis: r * (lower_bound X) <= b
hence r * (lower_bound X) <= b by A7, A8; ::_thesis: verum
end;
supposeA9: r < 0 ; ::_thesis: r * (lower_bound X) <= b
for z being real number st z in X holds
z >= b / r
proof
let z be real number ; ::_thesis: ( z in X implies z >= b / r )
assume z in X ; ::_thesis: z >= b / r
then r * z in { (r * y) where y is Real : y in X } ;
then r * z in r ** X by Th8;
hence z >= b / r by A7, A9, XREAL_1:78; ::_thesis: verum
end;
then lower_bound X >= b / r by SEQ_4:43;
then r * (lower_bound X) <= (b / r) * r by A9, XREAL_1:65;
hence r * (lower_bound X) <= b by A9, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence r * (lower_bound X) <= b ; ::_thesis: verum
end;
hence upper_bound (r ** X) = r * (lower_bound X) by A3, SEQ_4:46; ::_thesis: verum
end;
begin
theorem Th17: :: INTEGRA2:17
for r being Real
for X being non empty set
for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)
proof
let r be Real; ::_thesis: for X being non empty set
for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)
let X be non empty set ; ::_thesis: for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)
let f be Function of X,REAL; ::_thesis: rng (r (#) f) = r ** (rng f)
for y being Real st y in r ** (rng f) holds
y in rng (r (#) f)
proof
let y be Real; ::_thesis: ( y in r ** (rng f) implies y in rng (r (#) f) )
assume y in r ** (rng f) ; ::_thesis: y in rng (r (#) f)
then y in { (r * b) where b is Real : b in rng f } by Th8;
then consider b being Real such that
A1: y = r * b and
A2: b in rng f ;
consider x being Element of X such that
A3: x in dom f and
A4: b = f . x by A2, PARTFUN1:3;
x in dom (r (#) f) by A3, VALUED_1:def_5;
then (r (#) f) . x in rng (r (#) f) by FUNCT_1:def_3;
hence y in rng (r (#) f) by A1, A4, RFUNCT_1:57; ::_thesis: verum
end;
then A5: r ** (rng f) c= rng (r (#) f) by SUBSET_1:2;
for y being Real st y in rng (r (#) f) holds
y in r ** (rng f)
proof
let y be Real; ::_thesis: ( y in rng (r (#) f) implies y in r ** (rng f) )
assume y in rng (r (#) f) ; ::_thesis: y in r ** (rng f)
then consider x being Element of X such that
A6: x in dom (r (#) f) and
A7: y = (r (#) f) . x by PARTFUN1:3;
x in dom f by A6, VALUED_1:def_5;
then A8: f . x in rng f by FUNCT_1:def_3;
y = r * (f . x) by A7, RFUNCT_1:57;
then y in { (r * b) where b is Real : b in rng f } by A8;
hence y in r ** (rng f) by Th8; ::_thesis: verum
end;
then rng (r (#) f) c= r ** (rng f) by SUBSET_1:2;
hence rng (r (#) f) = r ** (rng f) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th18: :: INTEGRA2:18
for r being Real
for X, Z being non empty set
for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z))
proof
let r be Real; ::_thesis: for X, Z being non empty set
for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z))
let X, Z be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z))
let f be PartFunc of X,REAL; ::_thesis: rng (r (#) (f | Z)) = r ** (rng (f | Z))
for y being Real st y in r ** (rng (f | Z)) holds
y in rng (r (#) (f | Z))
proof
let y be Real; ::_thesis: ( y in r ** (rng (f | Z)) implies y in rng (r (#) (f | Z)) )
assume y in r ** (rng (f | Z)) ; ::_thesis: y in rng (r (#) (f | Z))
then y in { (r * b) where b is Real : b in rng (f | Z) } by Th8;
then consider b being Real such that
A1: y = r * b and
A2: b in rng (f | Z) ;
consider x being Element of X such that
A3: x in dom (f | Z) and
A4: b = (f | Z) . x by A2, PARTFUN1:3;
A5: x in dom (r (#) (f | Z)) by A3, VALUED_1:def_5;
then y = (r (#) (f | Z)) . x by A1, A4, VALUED_1:def_5;
hence y in rng (r (#) (f | Z)) by A5, FUNCT_1:def_3; ::_thesis: verum
end;
then A6: r ** (rng (f | Z)) c= rng (r (#) (f | Z)) by SUBSET_1:2;
for y being Real st y in rng (r (#) (f | Z)) holds
y in r ** (rng (f | Z))
proof
let y be Real; ::_thesis: ( y in rng (r (#) (f | Z)) implies y in r ** (rng (f | Z)) )
assume y in rng (r (#) (f | Z)) ; ::_thesis: y in r ** (rng (f | Z))
then consider x being Element of X such that
A7: x in dom (r (#) (f | Z)) and
A8: y = (r (#) (f | Z)) . x by PARTFUN1:3;
x in dom (f | Z) by A7, VALUED_1:def_5;
then A9: (f | Z) . x in rng (f | Z) by FUNCT_1:def_3;
y = r * ((f | Z) . x) by A7, A8, VALUED_1:def_5;
then y in { (r * b) where b is Real : b in rng (f | Z) } by A9;
hence y in r ** (rng (f | Z)) by Th8; ::_thesis: verum
end;
then rng (r (#) (f | Z)) c= r ** (rng (f | Z)) by SUBSET_1:2;
hence rng (r (#) (f | Z)) = r ** (rng (f | Z)) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th19: :: INTEGRA2:19
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r >= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)
let D be Division of A; ::_thesis: ( f | A is bounded & r >= 0 implies (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) )
assume that
A1: f | A is bounded and
A2: r >= 0 ; ::_thesis: (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A)
A3: rng f is bounded_below by A1, INTEGRA1:11;
A4: (r (#) f) | A is bounded by A1, RFUNCT_1:80;
then A5: lower_sum ((r (#) f),D) >= (lower_bound (rng (r (#) f))) * (vol A) by INTEGRA1:25;
(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def_10;
then A6: (upper_sum_set (r (#) f)) . D >= lower_sum ((r (#) f),D) by A4, INTEGRA1:28;
lower_bound (rng (r (#) f)) = lower_bound (r ** (rng f)) by Th17
.= r * (lower_bound (rng f)) by A2, A3, Th15 ;
hence (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th20: :: INTEGRA2:20
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)
let D be Division of A; ::_thesis: ( f | A is bounded & r <= 0 implies (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) )
assume that
A1: f | A is bounded and
A2: r <= 0 ; ::_thesis: (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)
A3: rng f is bounded_above by A1, INTEGRA1:13;
A4: (r (#) f) | A is bounded by A1, RFUNCT_1:80;
then A5: lower_sum ((r (#) f),D) >= (lower_bound (rng (r (#) f))) * (vol A) by INTEGRA1:25;
(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def_10;
then A6: (upper_sum_set (r (#) f)) . D >= lower_sum ((r (#) f),D) by A4, INTEGRA1:28;
lower_bound (rng (r (#) f)) = lower_bound (r ** (rng f)) by Th17
.= r * (upper_bound (rng f)) by A2, A3, Th14 ;
hence (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th21: :: INTEGRA2:21
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded & r >= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r >= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)
let D be Division of A; ::_thesis: ( f | A is bounded & r >= 0 implies (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) )
assume that
A1: f | A is bounded and
A2: r >= 0 ; ::_thesis: (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A)
A3: rng f is bounded_above by A1, INTEGRA1:13;
A4: (r (#) f) | A is bounded by A1, RFUNCT_1:80;
then A5: upper_sum ((r (#) f),D) <= (upper_bound (rng (r (#) f))) * (vol A) by INTEGRA1:27;
(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def_11;
then A6: (lower_sum_set (r (#) f)) . D <= upper_sum ((r (#) f),D) by A4, INTEGRA1:28;
upper_bound (rng (r (#) f)) = upper_bound (r ** (rng f)) by Th17
.= r * (upper_bound (rng f)) by A2, A3, Th13 ;
hence (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th22: :: INTEGRA2:22
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
let D be Division of A; ::_thesis: ( f | A is bounded & r <= 0 implies (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) )
assume that
A1: f | A is bounded and
A2: r <= 0 ; ::_thesis: (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
A3: rng f is bounded_below by A1, INTEGRA1:11;
A4: (r (#) f) | A is bounded by A1, RFUNCT_1:80;
then A5: upper_sum ((r (#) f),D) <= (upper_bound (rng (r (#) f))) * (vol A) by INTEGRA1:27;
(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def_11;
then A6: (lower_sum_set (r (#) f)) . D <= upper_sum ((r (#) f),D) by A4, INTEGRA1:28;
upper_bound (rng (r (#) f)) = upper_bound (r ** (rng f)) by Th17
.= r * (lower_bound (rng f)) by A2, A3, Th16 ;
hence (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th23: :: INTEGRA2:23
for r being Real
for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
proof
let r be Real; ::_thesis: for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_above & r >= 0 implies (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) )
assume that
A1: i in dom D and
A2: f | A is bounded_above and
A3: r >= 0 ; ::_thesis: (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61
.= A /\ (divset (D,i)) by FUNCT_2:def_1
.= divset (D,i) by A1, INTEGRA1:8, XBOOLE_1:28 ;
then A4: not rng (f | (divset (D,i))) is empty by RELAT_1:42;
rng f is bounded_above by A2, INTEGRA1:13;
then A5: rng (f | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43;
(upper_volume ((r (#) f),D)) . i = (upper_bound (rng ((r (#) f) | (divset (D,i))))) * (vol (divset (D,i))) by A1, INTEGRA1:def_6
.= (upper_bound (rng (r (#) (f | (divset (D,i)))))) * (vol (divset (D,i))) by RFUNCT_1:49
.= (upper_bound (r ** (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by Th18
.= (r * (upper_bound (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by A3, A4, A5, Th13
.= r * ((upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))))
.= r * ((upper_volume (f,D)) . i) by A1, INTEGRA1:def_6 ;
hence (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) ; ::_thesis: verum
end;
theorem Th24: :: INTEGRA2:24
for r being Real
for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
proof
let r be Real; ::_thesis: for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_above & r <= 0 implies (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) )
assume that
A1: i in dom D and
A2: f | A is bounded_above and
A3: r <= 0 ; ::_thesis: (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i)
dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61
.= A /\ (divset (D,i)) by FUNCT_2:def_1
.= divset (D,i) by A1, INTEGRA1:8, XBOOLE_1:28 ;
then A4: not rng (f | (divset (D,i))) is empty by RELAT_1:42;
rng f is bounded_above by A2, INTEGRA1:13;
then A5: rng (f | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43;
(lower_volume ((r (#) f),D)) . i = (lower_bound (rng ((r (#) f) | (divset (D,i))))) * (vol (divset (D,i))) by A1, INTEGRA1:def_7
.= (lower_bound (rng (r (#) (f | (divset (D,i)))))) * (vol (divset (D,i))) by RFUNCT_1:49
.= (lower_bound (r ** (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by Th18
.= (r * (upper_bound (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by A3, A4, A5, Th14
.= r * ((upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))))
.= r * ((upper_volume (f,D)) . i) by A1, INTEGRA1:def_6 ;
hence (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) ; ::_thesis: verum
end;
theorem Th25: :: INTEGRA2:25
for r being Real
for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
proof
let r be Real; ::_thesis: for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_below & r >= 0 implies (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) )
assume that
A1: i in dom D and
A2: f | A is bounded_below and
A3: r >= 0 ; ::_thesis: (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61
.= A /\ (divset (D,i)) by FUNCT_2:def_1
.= divset (D,i) by A1, INTEGRA1:8, XBOOLE_1:28 ;
then A4: not rng (f | (divset (D,i))) is empty by RELAT_1:42;
rng f is bounded_below by A2, INTEGRA1:11;
then A5: rng (f | (divset (D,i))) is bounded_below by RELAT_1:70, XXREAL_2:44;
(lower_volume ((r (#) f),D)) . i = (lower_bound (rng ((r (#) f) | (divset (D,i))))) * (vol (divset (D,i))) by A1, INTEGRA1:def_7
.= (lower_bound (rng (r (#) (f | (divset (D,i)))))) * (vol (divset (D,i))) by RFUNCT_1:49
.= (lower_bound (r ** (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by Th18
.= (r * (lower_bound (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by A3, A4, A5, Th15
.= r * ((lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))))
.= r * ((lower_volume (f,D)) . i) by A1, INTEGRA1:def_7 ;
hence (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ; ::_thesis: verum
end;
theorem Th26: :: INTEGRA2:26
for r being Real
for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
proof
let r be Real; ::_thesis: for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds
(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_below & r <= 0 implies (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) )
assume that
A1: i in dom D and
A2: f | A is bounded_below and
A3: r <= 0 ; ::_thesis: (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61
.= A /\ (divset (D,i)) by FUNCT_2:def_1
.= divset (D,i) by A1, INTEGRA1:8, XBOOLE_1:28 ;
then A4: not rng (f | (divset (D,i))) is empty by RELAT_1:42;
rng f is bounded_below by A2, INTEGRA1:11;
then A5: rng (f | (divset (D,i))) is bounded_below by RELAT_1:70, XXREAL_2:44;
(upper_volume ((r (#) f),D)) . i = (upper_bound (rng ((r (#) f) | (divset (D,i))))) * (vol (divset (D,i))) by A1, INTEGRA1:def_6
.= (upper_bound (rng (r (#) (f | (divset (D,i)))))) * (vol (divset (D,i))) by RFUNCT_1:49
.= (upper_bound (r ** (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by Th18
.= (r * (lower_bound (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by A3, A4, A5, Th16
.= r * ((lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))))
.= r * ((lower_volume (f,D)) . i) by A1, INTEGRA1:def_7 ;
hence (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ; ::_thesis: verum
end;
theorem Th27: :: INTEGRA2:27
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r >= 0 holds
upper_sum ((r (#) f),D) = r * (upper_sum (f,D))
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r >= 0 holds
upper_sum ((r (#) f),D) = r * (upper_sum (f,D))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r >= 0 holds
upper_sum ((r (#) f),D) = r * (upper_sum (f,D))
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_above & r >= 0 holds
upper_sum ((r (#) f),D) = r * (upper_sum (f,D))
let D be Division of A; ::_thesis: ( f | A is bounded_above & r >= 0 implies upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) )
assume A1: ( f | A is bounded_above & r >= 0 ) ; ::_thesis: upper_sum ((r (#) f),D) = r * (upper_sum (f,D))
A2: for i being Nat st 1 <= i & i <= len (upper_volume ((r (#) f),D)) holds
(upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) implies (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i )
assume A3: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) ) ; ::_thesis: (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
len D = len (upper_volume ((r (#) f),D)) by INTEGRA1:def_6;
then i in dom D by A3, FINSEQ_3:25;
then (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) by A1, Th23
.= (r * (upper_volume (f,D))) . i by RVSUM_1:44 ;
hence (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ; ::_thesis: verum
end;
len (upper_volume ((r (#) f),D)) = len D by INTEGRA1:def_6
.= len (upper_volume (f,D)) by INTEGRA1:def_6
.= len (r * (upper_volume (f,D))) by NEWTON:2 ;
then upper_volume ((r (#) f),D) = r * (upper_volume (f,D)) by A2, FINSEQ_1:14;
then upper_sum ((r (#) f),D) = Sum (r * (upper_volume (f,D))) by INTEGRA1:def_8
.= r * (Sum (upper_volume (f,D))) by RVSUM_1:87
.= r * (upper_sum (f,D)) by INTEGRA1:def_8 ;
hence upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) ; ::_thesis: verum
end;
theorem Th28: :: INTEGRA2:28
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_above & r <= 0 holds
lower_sum ((r (#) f),D) = r * (upper_sum (f,D))
let D be Division of A; ::_thesis: ( f | A is bounded_above & r <= 0 implies lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) )
assume A1: ( f | A is bounded_above & r <= 0 ) ; ::_thesis: lower_sum ((r (#) f),D) = r * (upper_sum (f,D))
A2: for i being Nat st 1 <= i & i <= len (lower_volume ((r (#) f),D)) holds
(lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) implies (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i )
assume A3: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) ) ; ::_thesis: (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i
len D = len (lower_volume ((r (#) f),D)) by INTEGRA1:def_7;
then i in dom D by A3, FINSEQ_3:25;
then (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) by A1, Th24
.= (r * (upper_volume (f,D))) . i by RVSUM_1:44 ;
hence (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ; ::_thesis: verum
end;
len (lower_volume ((r (#) f),D)) = len D by INTEGRA1:def_7
.= len (upper_volume (f,D)) by INTEGRA1:def_6
.= len (r * (upper_volume (f,D))) by NEWTON:2 ;
then lower_volume ((r (#) f),D) = r * (upper_volume (f,D)) by A2, FINSEQ_1:14;
then lower_sum ((r (#) f),D) = Sum (r * (upper_volume (f,D))) by INTEGRA1:def_9
.= r * (Sum (upper_volume (f,D))) by RVSUM_1:87
.= r * (upper_sum (f,D)) by INTEGRA1:def_8 ;
hence lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) ; ::_thesis: verum
end;
theorem Th29: :: INTEGRA2:29
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r >= 0 holds
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r >= 0 holds
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r >= 0 holds
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_below & r >= 0 holds
lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
let D be Division of A; ::_thesis: ( f | A is bounded_below & r >= 0 implies lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) )
assume A1: ( f | A is bounded_below & r >= 0 ) ; ::_thesis: lower_sum ((r (#) f),D) = r * (lower_sum (f,D))
A2: for i being Nat st 1 <= i & i <= len (lower_volume ((r (#) f),D)) holds
(lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) implies (lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i )
assume A3: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) ) ; ::_thesis: (lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i
len D = len (lower_volume ((r (#) f),D)) by INTEGRA1:def_7;
then i in dom D by A3, FINSEQ_3:25;
then (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) by A1, Th25
.= (r * (lower_volume (f,D))) . i by RVSUM_1:44 ;
hence (lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ; ::_thesis: verum
end;
len (lower_volume ((r (#) f),D)) = len D by INTEGRA1:def_7
.= len (lower_volume (f,D)) by INTEGRA1:def_7
.= len (r * (lower_volume (f,D))) by NEWTON:2 ;
then lower_volume ((r (#) f),D) = r * (lower_volume (f,D)) by A2, FINSEQ_1:14;
then lower_sum ((r (#) f),D) = Sum (r * (lower_volume (f,D))) by INTEGRA1:def_9
.= r * (Sum (lower_volume (f,D))) by RVSUM_1:87
.= r * (lower_sum (f,D)) by INTEGRA1:def_9 ;
hence lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) ; ::_thesis: verum
end;
theorem Th30: :: INTEGRA2:30
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_below & r <= 0 holds
upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
let D be Division of A; ::_thesis: ( f | A is bounded_below & r <= 0 implies upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) )
assume A1: ( f | A is bounded_below & r <= 0 ) ; ::_thesis: upper_sum ((r (#) f),D) = r * (lower_sum (f,D))
A2: for i being Nat st 1 <= i & i <= len (upper_volume ((r (#) f),D)) holds
(upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) implies (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i )
assume A3: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) ) ; ::_thesis: (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i
len D = len (upper_volume ((r (#) f),D)) by INTEGRA1:def_6;
then i in dom D by A3, FINSEQ_3:25;
then (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) by A1, Th26
.= (r * (lower_volume (f,D))) . i by RVSUM_1:44 ;
hence (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ; ::_thesis: verum
end;
len (upper_volume ((r (#) f),D)) = len D by INTEGRA1:def_6
.= len (lower_volume (f,D)) by INTEGRA1:def_7
.= len (r * (lower_volume (f,D))) by NEWTON:2 ;
then upper_volume ((r (#) f),D) = r * (lower_volume (f,D)) by A2, FINSEQ_1:14;
then upper_sum ((r (#) f),D) = Sum (r * (lower_volume (f,D))) by INTEGRA1:def_8
.= r * (Sum (lower_volume (f,D))) by RVSUM_1:87
.= r * (lower_sum (f,D)) by INTEGRA1:def_9 ;
hence upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) ; ::_thesis: verum
end;
theorem Th31: :: INTEGRA2:31
for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
( r (#) f is integrable & integral (r (#) f) = r * (integral f) )
proof
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable holds
( r (#) f is integrable & integral (r (#) f) = r * (integral f) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
( r (#) f is integrable & integral (r (#) f) = r * (integral f) )
let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) )
assume that
A1: f | A is bounded and
A2: f is integrable ; ::_thesis: ( r (#) f is integrable & integral (r (#) f) = r * (integral f) )
f is upper_integrable by A2, INTEGRA1:def_16;
then A3: rng (upper_sum_set f) is bounded_below by INTEGRA1:def_12;
f is lower_integrable by A2, INTEGRA1:def_16;
then A4: rng (lower_sum_set f) is bounded_above by INTEGRA1:def_13;
A5: now__::_thesis:_(_upper_integral_(r_(#)_f)_=_lower_integral_(r_(#)_f)_&_upper_integral_(r_(#)_f)_=_r_*_(integral_f)_)
percases ( r >= 0 or r < 0 ) ;
supposeA6: r >= 0 ; ::_thesis: ( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) )
A7: for D being set st D in divs A holds
(upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D
proof
let D be set ; ::_thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D )
assume A8: D in divs A ; ::_thesis: (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D
then reconsider D = D as Division of A by INTEGRA1:def_3;
(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def_10
.= r * (upper_sum (f,D)) by A1, A6, Th27
.= r * ((upper_sum_set f) . D) by INTEGRA1:def_10
.= (r (#) (upper_sum_set f)) . D by A8, RFUNCT_1:57 ;
hence (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; ::_thesis: verum
end;
A9: divs A = dom (upper_sum_set f) by FUNCT_2:def_1
.= dom (r (#) (upper_sum_set f)) by VALUED_1:def_5 ;
divs A = dom (upper_sum_set (r (#) f)) by FUNCT_2:def_1;
then upper_sum_set (r (#) f) = r (#) (upper_sum_set f) by A9, A7, FUNCT_1:2;
then A10: upper_integral (r (#) f) = lower_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def_14
.= lower_bound (r ** (rng (upper_sum_set f))) by Th17
.= r * (lower_bound (rng (upper_sum_set f))) by A3, A6, Th15
.= r * (upper_integral f) by INTEGRA1:def_14 ;
A11: for D being set st D in divs A holds
(lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D
proof
let D be set ; ::_thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D )
assume A12: D in divs A ; ::_thesis: (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D
then reconsider D = D as Division of A by INTEGRA1:def_3;
(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def_11
.= r * (lower_sum (f,D)) by A1, A6, Th29
.= r * ((lower_sum_set f) . D) by INTEGRA1:def_11
.= (r (#) (lower_sum_set f)) . D by A12, RFUNCT_1:57 ;
hence (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; ::_thesis: verum
end;
A13: divs A = dom (lower_sum_set f) by FUNCT_2:def_1
.= dom (r (#) (lower_sum_set f)) by VALUED_1:def_5 ;
divs A = dom (lower_sum_set (r (#) f)) by FUNCT_2:def_1;
then lower_sum_set (r (#) f) = r (#) (lower_sum_set f) by A13, A11, FUNCT_1:2;
then lower_integral (r (#) f) = upper_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def_15
.= upper_bound (r ** (rng (lower_sum_set f))) by Th17
.= r * (upper_bound (rng (lower_sum_set f))) by A4, A6, Th13
.= r * (lower_integral f) by INTEGRA1:def_15
.= r * (upper_integral f) by A2, INTEGRA1:def_16 ;
hence upper_integral (r (#) f) = lower_integral (r (#) f) by A10; ::_thesis: upper_integral (r (#) f) = r * (integral f)
thus upper_integral (r (#) f) = r * (integral f) by A10, INTEGRA1:def_17; ::_thesis: verum
end;
supposeA14: r < 0 ; ::_thesis: ( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) )
A15: for D being set st D in divs A holds
(upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D
proof
let D be set ; ::_thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D )
assume A16: D in divs A ; ::_thesis: (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D
then reconsider D = D as Division of A by INTEGRA1:def_3;
(upper_sum_set (r (#) f)) . D = upper_sum ((r (#) f),D) by INTEGRA1:def_10
.= r * (lower_sum (f,D)) by A1, A14, Th30
.= r * ((lower_sum_set f) . D) by INTEGRA1:def_11
.= (r (#) (lower_sum_set f)) . D by A16, RFUNCT_1:57 ;
hence (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; ::_thesis: verum
end;
A17: divs A = dom (lower_sum_set f) by FUNCT_2:def_1
.= dom (r (#) (lower_sum_set f)) by VALUED_1:def_5 ;
divs A = dom (upper_sum_set (r (#) f)) by FUNCT_2:def_1;
then upper_sum_set (r (#) f) = r (#) (lower_sum_set f) by A17, A15, FUNCT_1:2;
then A18: upper_integral (r (#) f) = lower_bound (rng (r (#) (lower_sum_set f))) by INTEGRA1:def_14
.= lower_bound (r ** (rng (lower_sum_set f))) by Th17
.= r * (upper_bound (rng (lower_sum_set f))) by A4, A14, Th14
.= r * (lower_integral f) by INTEGRA1:def_15 ;
A19: for D being set st D in divs A holds
(lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D
proof
let D be set ; ::_thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D )
assume A20: D in divs A ; ::_thesis: (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D
then reconsider D = D as Division of A by INTEGRA1:def_3;
(lower_sum_set (r (#) f)) . D = lower_sum ((r (#) f),D) by INTEGRA1:def_11
.= r * (upper_sum (f,D)) by A1, A14, Th28
.= r * ((upper_sum_set f) . D) by INTEGRA1:def_10
.= (r (#) (upper_sum_set f)) . D by A20, RFUNCT_1:57 ;
hence (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; ::_thesis: verum
end;
A21: divs A = dom (upper_sum_set f) by FUNCT_2:def_1
.= dom (r (#) (upper_sum_set f)) by VALUED_1:def_5 ;
divs A = dom (lower_sum_set (r (#) f)) by FUNCT_2:def_1;
then lower_sum_set (r (#) f) = r (#) (upper_sum_set f) by A21, A19, FUNCT_1:2;
then lower_integral (r (#) f) = upper_bound (rng (r (#) (upper_sum_set f))) by INTEGRA1:def_15
.= upper_bound (r ** (rng (upper_sum_set f))) by Th17
.= r * (lower_bound (rng (upper_sum_set f))) by A3, A14, Th16
.= r * (upper_integral f) by INTEGRA1:def_14
.= r * (lower_integral f) by A2, INTEGRA1:def_16 ;
hence upper_integral (r (#) f) = lower_integral (r (#) f) by A18; ::_thesis: upper_integral (r (#) f) = r * (integral f)
upper_integral (r (#) f) = r * (upper_integral f) by A2, A18, INTEGRA1:def_16
.= r * (integral f) by INTEGRA1:def_17 ;
hence upper_integral (r (#) f) = r * (integral f) ; ::_thesis: verum
end;
end;
end;
ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D
proof
now__::_thesis:_ex_a_being_Real_st_
for_D_being_set_st_D_in_(divs_A)_/\_(dom_(lower_sum_set_(r_(#)_f)))_holds_
a_>=_(lower_sum_set_(r_(#)_f))_._D
percases ( r >= 0 or r < 0 ) ;
supposeA22: r >= 0 ; ::_thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
(r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D
proof
let D be set ; ::_thesis: ( D in (divs A) /\ (dom (lower_sum_set (r (#) f))) implies (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D )
assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; ::_thesis: (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D
then D is Division of A by INTEGRA1:def_3;
hence (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A22, Th21; ::_thesis: verum
end;
hence ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D ; ::_thesis: verum
end;
supposeA23: r < 0 ; ::_thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
(r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D
proof
let D be set ; ::_thesis: ( D in (divs A) /\ (dom (lower_sum_set (r (#) f))) implies (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D )
assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; ::_thesis: (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D
then D is Division of A by INTEGRA1:def_3;
hence (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A23, Th22; ::_thesis: verum
end;
hence ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D ; ::_thesis: verum
end;
end;
end;
hence ex a being Real st
for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds
a >= (lower_sum_set (r (#) f)) . D ; ::_thesis: verum
end;
then (lower_sum_set (r (#) f)) | (divs A) is bounded_above by RFUNCT_1:70;
then rng (lower_sum_set (r (#) f)) is bounded_above by INTEGRA1:13;
then A24: r (#) f is lower_integrable by INTEGRA1:def_13;
ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D
proof
now__::_thesis:_ex_a_being_Real_st_
for_D_being_set_st_D_in_(divs_A)_/\_(dom_(upper_sum_set_(r_(#)_f)))_holds_
a_<=_(upper_sum_set_(r_(#)_f))_._D
percases ( r >= 0 or r < 0 ) ;
supposeA25: r >= 0 ; ::_thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
(r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D
proof
let D be set ; ::_thesis: ( D in (divs A) /\ (dom (upper_sum_set (r (#) f))) implies (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D )
assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; ::_thesis: (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D
then D is Division of A by INTEGRA1:def_3;
hence (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A25, Th19; ::_thesis: verum
end;
hence ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D ; ::_thesis: verum
end;
supposeA26: r < 0 ; ::_thesis: ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
(r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D
proof
let D be set ; ::_thesis: ( D in (divs A) /\ (dom (upper_sum_set (r (#) f))) implies (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D )
assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; ::_thesis: (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D
then D is Division of A by INTEGRA1:def_3;
hence (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A26, Th20; ::_thesis: verum
end;
hence ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D ; ::_thesis: verum
end;
end;
end;
hence ex a being Real st
for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds
a <= (upper_sum_set (r (#) f)) . D ; ::_thesis: verum
end;
then (upper_sum_set (r (#) f)) | (divs A) is bounded_below by RFUNCT_1:71;
then rng (upper_sum_set (r (#) f)) is bounded_below by INTEGRA1:11;
then r (#) f is upper_integrable by INTEGRA1:def_12;
hence ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) by A24, A5, INTEGRA1:def_16, INTEGRA1:def_17; ::_thesis: verum
end;
begin
theorem Th32: :: INTEGRA2:32
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & ( for x being Real st x in A holds
f . x >= 0 ) holds
integral f >= 0
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & ( for x being Real st x in A holds
f . x >= 0 ) holds
integral f >= 0
let f be Function of A,REAL; ::_thesis: ( f | A is bounded & ( for x being Real st x in A holds
f . x >= 0 ) implies integral f >= 0 )
assume that
A1: f | A is bounded and
A2: for x being Real st x in A holds
f . x >= 0 ; ::_thesis: integral f >= 0
A3: for a being real number st a in rng (upper_sum_set f) holds
a >= 0
proof
let a be real number ; ::_thesis: ( a in rng (upper_sum_set f) implies a >= 0 )
assume a in rng (upper_sum_set f) ; ::_thesis: a >= 0
then consider D being Element of divs A such that
A4: ( D in dom (upper_sum_set f) & a = (upper_sum_set f) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def_3;
A5: for i being Nat st i in dom (upper_volume (f,D)) holds
0 <= (upper_volume (f,D)) . i
proof
let i be Nat; ::_thesis: ( i in dom (upper_volume (f,D)) implies 0 <= (upper_volume (f,D)) . i )
set r = (upper_volume (f,D)) . i;
assume A6: i in dom (upper_volume (f,D)) ; ::_thesis: 0 <= (upper_volume (f,D)) . i
len D = len (upper_volume (f,D)) by INTEGRA1:def_6;
then A7: i in dom D by A6, FINSEQ_3:29;
A8: upper_bound (rng (f | (divset (D,i)))) >= 0
proof
rng f is bounded_above by A1, INTEGRA1:13;
then A9: rng (f | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43;
( dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) & dom f = A ) by FUNCT_2:def_1, RELAT_1:61;
then dom (f | (divset (D,i))) is non empty Subset of REAL by A7, INTEGRA1:8, XBOOLE_1:28;
then consider x being Real such that
A10: x in dom (f | (divset (D,i))) by SUBSET_1:4;
f . x >= 0 by A2, A10;
then A11: (f | (divset (D,i))) . x >= 0 by A10, FUNCT_1:47;
(f | (divset (D,i))) . x in rng (f | (divset (D,i))) by A10, FUNCT_1:def_3;
hence upper_bound (rng (f | (divset (D,i)))) >= 0 by A9, A11, SEQ_4:def_1; ::_thesis: verum
end;
A12: vol (divset (D,i)) >= 0 by INTEGRA1:9;
(upper_volume (f,D)) . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A7, INTEGRA1:def_6;
hence 0 <= (upper_volume (f,D)) . i by A12, A8; ::_thesis: verum
end;
a = upper_sum (f,D) by A4, INTEGRA1:def_10
.= Sum (upper_volume (f,D)) by INTEGRA1:def_8 ;
hence a >= 0 by A5, RVSUM_1:84; ::_thesis: verum
end;
( upper_integral f = lower_bound (rng (upper_sum_set f)) & not rng (upper_sum_set f) is empty ) by INTEGRA1:def_14;
then upper_integral f >= 0 by A3, SEQ_4:43;
hence integral f >= 0 by INTEGRA1:def_17; ::_thesis: verum
end;
theorem Th33: :: INTEGRA2:33
for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
( f - g is integrable & integral (f - g) = (integral f) - (integral g) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
( f - g is integrable & integral (f - g) = (integral f) - (integral g) )
let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable implies ( f - g is integrable & integral (f - g) = (integral f) - (integral g) ) )
assume that
A1: ( f | A is bounded & f is integrable ) and
A2: g | A is bounded and
A3: g is integrable ; ::_thesis: ( f - g is integrable & integral (f - g) = (integral f) - (integral g) )
- g = (- 1) (#) g ;
then A4: - g is integrable by A2, A3, Th31;
A5: (- g) | A is bounded by A2, RFUNCT_1:82;
hence f - g is integrable by A1, A4, INTEGRA1:57; ::_thesis: integral (f - g) = (integral f) - (integral g)
integral (- g) = (- 1) * (integral g) by A2, A3, Th31;
then integral (f - g) = (integral f) + (- (integral g)) by A1, A5, A4, INTEGRA1:57;
hence integral (f - g) = (integral f) - (integral g) ; ::_thesis: verum
end;
theorem :: INTEGRA2:34
for A being non empty closed_interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds
f . x >= g . x ) holds
integral f >= integral g
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds
f . x >= g . x ) holds
integral f >= integral g
let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds
f . x >= g . x ) implies integral f >= integral g )
assume that
A1: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable ) and
A2: for x being Real st x in A holds
f . x >= g . x ; ::_thesis: integral f >= integral g
A3: dom (f - g) = A by FUNCT_2:def_1;
A4: for x being Real st x in A holds
(f - g) . x >= 0
proof
let x be Real; ::_thesis: ( x in A implies (f - g) . x >= 0 )
assume A5: x in A ; ::_thesis: (f - g) . x >= 0
then (f - g) . x = (f . x) - (g . x) by A3, VALUED_1:13;
hence (f - g) . x >= 0 by A2, A5, XREAL_1:48; ::_thesis: verum
end;
( integral (f - g) = (integral f) - (integral g) & (f - g) | (A /\ A) is bounded ) by A1, Th33, RFUNCT_1:84;
hence integral f >= integral g by A4, Th32, XREAL_1:49; ::_thesis: verum
end;
begin
theorem :: INTEGRA2:35
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
rng (upper_sum_set f) is bounded_below
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds
rng (upper_sum_set f) is bounded_below
let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies rng (upper_sum_set f) is bounded_below )
set D1 = the Division of A;
assume A1: f | A is bounded ; ::_thesis: rng (upper_sum_set f) is bounded_below
take lower_sum (f, the Division of A) ; :: according to XXREAL_2:def_9 ::_thesis: lower_sum (f, the Division of A) is LowerBound of rng (upper_sum_set f)
let a be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not a in rng (upper_sum_set f) or lower_sum (f, the Division of A) <= a )
assume a in rng (upper_sum_set f) ; ::_thesis: lower_sum (f, the Division of A) <= a
then consider D being Element of divs A such that
A2: ( D in dom (upper_sum_set f) & a = (upper_sum_set f) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def_3;
a = upper_sum (f,D) by A2, INTEGRA1:def_10;
hence lower_sum (f, the Division of A) <= a by A1, INTEGRA1:48; ::_thesis: verum
end;
theorem :: INTEGRA2:36
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
rng (lower_sum_set f) is bounded_above
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds
rng (lower_sum_set f) is bounded_above
let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies rng (lower_sum_set f) is bounded_above )
set D1 = the Division of A;
assume A1: f | A is bounded ; ::_thesis: rng (lower_sum_set f) is bounded_above
take upper_sum (f, the Division of A) ; :: according to XXREAL_2:def_10 ::_thesis: upper_sum (f, the Division of A) is UpperBound of rng (lower_sum_set f)
let a be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not a in rng (lower_sum_set f) or a <= upper_sum (f, the Division of A) )
assume a in rng (lower_sum_set f) ; ::_thesis: a <= upper_sum (f, the Division of A)
then consider D being Element of divs A such that
A2: ( D in dom (lower_sum_set f) & a = (lower_sum_set f) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def_3;
a = lower_sum (f,D) by A2, INTEGRA1:def_11;
hence a <= upper_sum (f, the Division of A) by A1, INTEGRA1:48; ::_thesis: verum
end;
definition
let A be non empty closed_interval Subset of REAL;
mode DivSequence of A is Function of NAT,(divs A);
end;
definition
let A be non empty closed_interval Subset of REAL;
let T be DivSequence of A;
let i be Element of NAT ;
:: original: .
redefine funcT . i -> Division of A;
coherence
T . i is Division of A
proof
T . i is Element of divs A ;
hence T . i is Division of A by INTEGRA1:def_3; ::_thesis: verum
end;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of A,REAL;
let T be DivSequence of A;
func upper_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 2
for i being Element of NAT holds it . i = upper_sum (f,(T . i));
existence
ex b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = upper_sum (f,(T . i))
proof
deffunc H1( Element of NAT ) -> Element of REAL = upper_sum (f,(T . $1));
thus ex IT being Real_Sequence st
for i being Element of NAT holds IT . i = H1(i) from SEQ_1:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = upper_sum (f,(T . i)) ) & ( for i being Element of NAT holds b2 . i = upper_sum (f,(T . i)) ) holds
b1 = b2
proof
let F1, F2 be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds F1 . i = upper_sum (f,(T . i)) ) & ( for i being Element of NAT holds F2 . i = upper_sum (f,(T . i)) ) implies F1 = F2 )
assume that
A1: for i being Element of NAT holds F1 . i = upper_sum (f,(T . i)) and
A2: for i being Element of NAT holds F2 . i = upper_sum (f,(T . i)) ; ::_thesis: F1 = F2
for i being Element of NAT holds F1 . i = F2 . i
proof
let i be Element of NAT ; ::_thesis: F1 . i = F2 . i
F1 . i = upper_sum (f,(T . i)) by A1
.= F2 . i by A2 ;
hence F1 . i = F2 . i ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
func lower_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 3
for i being Element of NAT holds it . i = lower_sum (f,(T . i));
existence
ex b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = lower_sum (f,(T . i))
proof
deffunc H1( Element of NAT ) -> Element of REAL = lower_sum (f,(T . $1));
thus ex IT being Real_Sequence st
for i being Element of NAT holds IT . i = H1(i) from SEQ_1:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = lower_sum (f,(T . i)) ) & ( for i being Element of NAT holds b2 . i = lower_sum (f,(T . i)) ) holds
b1 = b2
proof
let F1, F2 be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds F1 . i = lower_sum (f,(T . i)) ) & ( for i being Element of NAT holds F2 . i = lower_sum (f,(T . i)) ) implies F1 = F2 )
assume that
A3: for i being Element of NAT holds F1 . i = lower_sum (f,(T . i)) and
A4: for i being Element of NAT holds F2 . i = lower_sum (f,(T . i)) ; ::_thesis: F1 = F2
for i being Element of NAT holds F1 . i = F2 . i
proof
let i be Element of NAT ; ::_thesis: F1 . i = F2 . i
F1 . i = lower_sum (f,(T . i)) by A3
.= F2 . i by A4 ;
hence F1 . i = F2 . i ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem defines upper_sum INTEGRA2:def_2_:_
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for T being DivSequence of A
for b4 being Real_Sequence holds
( b4 = upper_sum (f,T) iff for i being Element of NAT holds b4 . i = upper_sum (f,(T . i)) );
:: deftheorem defines lower_sum INTEGRA2:def_3_:_
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for T being DivSequence of A
for b4 being Real_Sequence holds
( b4 = lower_sum (f,T) iff for i being Element of NAT holds b4 . i = lower_sum (f,(T . i)) );
theorem :: INTEGRA2:37
for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A st D1 <= D2 holds
for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for D1, D2 being Division of A st D1 <= D2 holds
for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )
let D1, D2 be Division of A; ::_thesis: ( D1 <= D2 implies for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset (D2,j) c= divset (D1,i) ) )
assume A1: D1 <= D2 ; ::_thesis: for j being Element of NAT st j in dom D2 holds
ex i being Element of NAT st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )
let j be Element of NAT ; ::_thesis: ( j in dom D2 implies ex i being Element of NAT st
( i in dom D1 & divset (D2,j) c= divset (D1,i) ) )
defpred S1[ set ] means ( D2 . $1 in rng D1 & D2 . $1 >= D2 . j );
consider X being Subset of (dom D2) such that
A2: for x1 being set holds
( x1 in X iff ( x1 in dom D2 & S1[x1] ) ) from SUBSET_1:sch_1();
reconsider X = X as Subset of NAT by XBOOLE_1:1;
assume A3: j in dom D2 ; ::_thesis: ex i being Element of NAT st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )
ex n being Element of NAT st
( n in dom D2 & D2 . n in rng D1 & D2 . n >= D2 . j )
proof
take len D2 ; ::_thesis: ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j )
len D2 in Seg (len D2) by FINSEQ_1:3;
then A4: len D2 in dom D2 by FINSEQ_1:def_3;
len D1 in Seg (len D1) by FINSEQ_1:3;
then A5: len D1 in dom D1 by FINSEQ_1:def_3;
D2 . (len D2) = upper_bound A by INTEGRA1:def_2;
then A6: D1 . (len D1) = D2 . (len D2) by INTEGRA1:def_2;
j in Seg (len D2) by A3, FINSEQ_1:def_3;
then j <= len D2 by FINSEQ_1:1;
hence ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j ) by A3, A5, A6, A4, FUNCT_1:def_3, SEQ_4:137; ::_thesis: verum
end;
then reconsider X = X as non empty Subset of NAT by A2;
A7: min X in X by XXREAL_2:def_7;
then A8: D2 . (min X) >= D2 . j by A2;
D2 . (min X) in rng D1 by A2, A7;
then consider i being Element of NAT such that
A9: i in dom D1 and
A10: D2 . (min X) = D1 . i by PARTFUN1:3;
take i ; ::_thesis: ( i in dom D1 & divset (D2,j) c= divset (D1,i) )
A11: D1 . i >= D2 . j by A2, A7, A10;
divset (D2,j) c= divset (D1,i)
proof
now__::_thesis:_divset_(D2,j)_c=_divset_(D1,i)
percases ( i = 1 or i <> 1 ) ;
suppose i = 1 ; ::_thesis: divset (D2,j) c= divset (D1,i)
then ( lower_bound (divset (D1,i)) = lower_bound A & upper_bound (divset (D1,i)) = D1 . i ) by A9, INTEGRA1:def_4;
then A12: divset (D1,i) = [.(lower_bound A),(D1 . i).] by INTEGRA1:4;
now__::_thesis:_divset_(D2,j)_c=_divset_(D1,i)
percases ( j = 1 or j <> 1 ) ;
supposeA13: j = 1 ; ::_thesis: divset (D2,j) c= divset (D1,i)
( D1 . i in rng D1 & rng D1 c= A ) by A9, FUNCT_1:def_3, INTEGRA1:def_2;
then A14: D1 . i in A ;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then D1 . i in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A14, RCOMP_1:def_1;
then ex x being Real st
( x = D1 . i & lower_bound A <= x & x <= upper_bound A ) ;
then lower_bound A in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } ;
then A15: lower_bound A in [.(lower_bound A),(D1 . i).] by RCOMP_1:def_1;
( D2 . j in rng D2 & rng D2 c= A ) by A3, FUNCT_1:def_3, INTEGRA1:def_2;
then A16: D2 . j in A ;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A16, RCOMP_1:def_1;
then ex x being Real st
( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A8, A10;
then A17: D2 . j in [.(lower_bound A),(D1 . i).] by RCOMP_1:def_1;
( lower_bound (divset (D2,j)) = lower_bound A & upper_bound (divset (D2,j)) = D2 . j ) by A3, A13, INTEGRA1:def_4;
then divset (D2,j) = [.(lower_bound A),(D2 . j).] by INTEGRA1:4;
hence divset (D2,j) c= divset (D1,i) by A12, A15, A17, XXREAL_2:def_12; ::_thesis: verum
end;
supposeA18: j <> 1 ; ::_thesis: divset (D2,j) c= divset (D1,i)
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A19: A = { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def_1;
( D2 . j in rng D2 & rng D2 c= A ) by A3, FUNCT_1:def_3, INTEGRA1:def_2;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A19;
then ex x being Real st
( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A8, A10;
then A20: D2 . j in [.(lower_bound A),(D1 . i).] by RCOMP_1:def_1;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A21: A = { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def_1;
A22: rng D2 c= A by INTEGRA1:def_2;
A23: j - 1 in dom D2 by A3, A18, INTEGRA1:7;
then D2 . (j - 1) in rng D2 by FUNCT_1:def_3;
then D2 . (j - 1) in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A21, A22;
then A24: ex x being Real st
( x = D2 . (j - 1) & lower_bound A <= x & x <= upper_bound A ) ;
j <= j + 1 by NAT_1:11;
then j - 1 <= j by XREAL_1:20;
then D2 . (j - 1) <= D2 . j by A3, A23, SEQ_4:137;
then D2 . (j - 1) <= D1 . i by A8, A10, XXREAL_0:2;
then D2 . (j - 1) in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A24;
then A25: D2 . (j - 1) in [.(lower_bound A),(D1 . i).] by RCOMP_1:def_1;
( lower_bound (divset (D2,j)) = D2 . (j - 1) & upper_bound (divset (D2,j)) = D2 . j ) by A3, A18, INTEGRA1:def_4;
then divset (D2,j) = [.(D2 . (j - 1)),(D2 . j).] by INTEGRA1:4;
hence divset (D2,j) c= divset (D1,i) by A12, A25, A20, XXREAL_2:def_12; ::_thesis: verum
end;
end;
end;
hence divset (D2,j) c= divset (D1,i) ; ::_thesis: verum
end;
supposeA26: i <> 1 ; ::_thesis: divset (D2,j) c= divset (D1,i)
A27: j <> 1
proof
assume A28: j = 1 ; ::_thesis: contradiction
A29: i in Seg (len D1) by A9, FINSEQ_1:def_3;
then A30: 1 <= i by FINSEQ_1:1;
i <= len D1 by A29, FINSEQ_1:1;
then 1 <= len D1 by A30, XXREAL_0:2;
then 1 in Seg (len D1) by FINSEQ_1:1;
then A31: 1 in dom D1 by FINSEQ_1:def_3;
then A32: D1 . 1 in rng D1 by FUNCT_1:def_3;
rng D1 c= rng D2 by A1, INTEGRA1:def_18;
then consider n being Element of NAT such that
A33: n in dom D2 and
A34: D1 . 1 = D2 . n by A32, PARTFUN1:3;
A35: n in Seg (len D2) by A33, FINSEQ_1:def_3;
then A36: 1 <= n by FINSEQ_1:1;
n <= len D2 by A35, FINSEQ_1:1;
then 1 <= len D2 by A36, XXREAL_0:2;
then 1 in Seg (len D2) by FINSEQ_1:1;
then 1 in dom D2 by FINSEQ_1:def_3;
then D2 . j <= D2 . n by A28, A33, A36, SEQ_4:137;
then n in X by A2, A32, A33, A34;
then n >= min X by XXREAL_2:def_7;
then A37: D1 . 1 >= D1 . i by A7, A10, A33, A34, SEQ_4:137;
i > 1 by A26, A30, XXREAL_0:1;
hence contradiction by A9, A31, A37, SEQM_3:def_1; ::_thesis: verum
end;
then A38: j - 1 in dom D2 by A3, INTEGRA1:7;
A39: D1 . (i - 1) <= D2 . (j - 1)
proof
A40: i - 1 in dom D1 by A9, A26, INTEGRA1:7;
then A41: D1 . (i - 1) in rng D1 by FUNCT_1:def_3;
rng D1 c= rng D2 by A1, INTEGRA1:def_18;
then consider n being Element of NAT such that
A42: ( n in dom D2 & D1 . (i - 1) = D2 . n ) by A41, PARTFUN1:3;
assume D1 . (i - 1) > D2 . (j - 1) ; ::_thesis: contradiction
then n > j - 1 by A38, A42, SEQ_4:137;
then n + 1 > j by XREAL_1:19;
then n >= j by NAT_1:13;
then D1 . (i - 1) >= D2 . j by A3, A42, SEQ_4:137;
then n in X by A2, A41, A42;
then n >= min X by XXREAL_2:def_7;
then D1 . (i - 1) >= D1 . i by A7, A10, A42, SEQ_4:137;
then i - 1 >= i by A9, A40, SEQM_3:def_1;
then A43: i >= i + 1 by XREAL_1:19;
i <= i + 1 by NAT_1:11;
then i = i + 1 by A43, XXREAL_0:1;
hence contradiction ; ::_thesis: verum
end;
j <= j + 1 by NAT_1:11;
then j - 1 <= j by XREAL_1:20;
then A44: D2 . (j - 1) <= D2 . j by A3, A38, SEQ_4:137;
then A45: D1 . (i - 1) <= D2 . j by A39, XXREAL_0:2;
D2 . (j - 1) <= D1 . i by A11, A44, XXREAL_0:2;
then D2 . (j - 1) in { r where r is Real : ( D1 . (i - 1) <= r & r <= D1 . i ) } by A39;
then A46: D2 . (j - 1) in [.(D1 . (i - 1)),(D1 . i).] by RCOMP_1:def_1;
D2 . j <= D1 . i by A2, A7, A10;
then D2 . j in { r where r is Real : ( D1 . (i - 1) <= r & r <= D1 . i ) } by A45;
then A47: D2 . j in [.(D1 . (i - 1)),(D1 . i).] by RCOMP_1:def_1;
( lower_bound (divset (D2,j)) = D2 . (j - 1) & upper_bound (divset (D2,j)) = D2 . j ) by A3, A27, INTEGRA1:def_4;
then A48: divset (D2,j) = [.(D2 . (j - 1)),(D2 . j).] by INTEGRA1:4;
( lower_bound (divset (D1,i)) = D1 . (i - 1) & upper_bound (divset (D1,i)) = D1 . i ) by A9, A26, INTEGRA1:def_4;
then divset (D1,i) = [.(D1 . (i - 1)),(D1 . i).] by INTEGRA1:4;
hence divset (D2,j) c= divset (D1,i) by A48, A46, A47, XXREAL_2:def_12; ::_thesis: verum
end;
end;
end;
hence divset (D2,j) c= divset (D1,i) ; ::_thesis: verum
end;
hence ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) by A9; ::_thesis: verum
end;
theorem :: INTEGRA2:38
for A, B being non empty closed_interval Subset of REAL st A c= B holds
vol A <= vol B
proof
let A, B be non empty closed_interval Subset of REAL; ::_thesis: ( A c= B implies vol A <= vol B )
assume A1: A c= B ; ::_thesis: vol A <= vol B
vol A = (upper_bound A) - (lower_bound A) by INTEGRA1:def_5;
then upper_bound B >= (vol A) + (lower_bound A) by A1, SEQ_4:48;
then A2: (upper_bound B) - (vol A) >= lower_bound A by XREAL_1:19;
lower_bound A >= lower_bound B by A1, SEQ_4:47;
then (upper_bound B) - (vol A) >= lower_bound B by A2, XXREAL_0:2;
then (upper_bound B) - (lower_bound B) >= vol A by XREAL_1:11;
hence vol A <= vol B by INTEGRA1:def_5; ::_thesis: verum
end;
theorem :: INTEGRA2:39
for A being Subset of REAL
for a, x being Real st x in a ** A holds
ex b being Real st
( b in A & x = a * b )
proof
let A be Subset of REAL; ::_thesis: for a, x being Real st x in a ** A holds
ex b being Real st
( b in A & x = a * b )
let a, x be Real; ::_thesis: ( x in a ** A implies ex b being Real st
( b in A & x = a * b ) )
assume x in a ** A ; ::_thesis: ex b being Real st
( b in A & x = a * b )
then x in { (a * b) where b is Element of ExtREAL : b in A } by MEMBER_1:187;
then consider b being Element of ExtREAL such that
A1: ( x = a * b & b in A ) ;
reconsider b = b as Real by A1;
take b ; ::_thesis: ( b in A & x = a * b )
x = a * b by A1, XXREAL_3:def_5;
hence ( b in A & x = a * b ) by A1; ::_thesis: verum
end;
begin
theorem :: INTEGRA2:40
for A being non empty ext-real-membered set holds 0 ** A = {0}
proof
let A be non empty ext-real-membered set ; ::_thesis: 0 ** A = {0}
for e being set holds
( e in 0 ** A iff e = 0 )
proof
let e be set ; ::_thesis: ( e in 0 ** A iff e = 0 )
consider r being ext-real number such that
A1: r in A by MEMBERED:8;
hereby ::_thesis: ( e = 0 implies e in 0 ** A )
assume e in 0 ** A ; ::_thesis: e = 0
then ex z being Element of ExtREAL st
( e = 0 * z & z in A ) by MEMBER_1:188;
hence e = 0 ; ::_thesis: verum
end;
assume e = 0 ; ::_thesis: e in 0 ** A
then e = 0 * r ;
hence e in 0 ** A by A1, MEMBER_1:186; ::_thesis: verum
end;
hence 0 ** A = {0} by TARSKI:def_1; ::_thesis: verum
end;