let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
max+ f is integrable
let f be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable implies max+ f is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable ; :: thesis: max+ f is integrable
A3: max+ f is total by Th13;
A4: (max+ f) | A is bounded_below by Th15;
A5: (max+ f) | A is bounded_above by A1, Th14;
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0
proof
let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0 )
assume that
A6: delta T is convergent and
A7: lim (delta T) = 0 ; :: thesis: (lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0
A8: lower_sum f,T is convergent by A1, A6, A7, Th8;
A9: upper_sum f,T is convergent by A1, A6, A7, Th9;
then A10: (upper_sum f,T) - (lower_sum f,T) is convergent by A8, SEQ_2:25;
reconsider osc1 = (upper_sum (max+ f),T) - (lower_sum (max+ f),T) as Real_Sequence ;
reconsider osc = (upper_sum f,T) - (lower_sum f,T) as Real_Sequence ;
(lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0 by A1, A2, A6, A7, Th12;
then A11: lim ((upper_sum f,T) - (lower_sum f,T)) = 0 by A9, A8, SEQ_2:26;
A12: for a being real number st 0 < a holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a
proof
let a be real number ; :: thesis: ( 0 < a implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a )
assume 0 < a ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a
then consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
abs ((osc . m) - 0 ) < a by A10, A11, SEQ_2:def 7;
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a
proof
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((osc1 . m) - 0 ) < a )
reconsider D = T . m as Division of A ;
len (upper_volume f,D) = len D by INTEGRA1:def 7;
then reconsider UV = upper_volume f,D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
len (lower_volume f,D) = len D by INTEGRA1:def 8;
then reconsider LV = lower_volume f,D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
len (upper_volume (max+ f),D) = len D by INTEGRA1:def 7;
then reconsider UV1 = upper_volume (max+ f),D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
len (lower_volume (max+ f),D) = len D by INTEGRA1:def 8;
then reconsider LV1 = lower_volume (max+ f),D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
reconsider F = UV1 - LV1 as FinSequence of REAL ;
osc1 . m = ((upper_sum (max+ f),T) . m) + ((- (lower_sum (max+ f),T)) . m) by SEQ_1:11
.= ((upper_sum (max+ f),T) . m) + (- ((lower_sum (max+ f),T) . m)) by SEQ_1:14
.= ((upper_sum (max+ f),T) . m) - ((lower_sum (max+ f),T) . m)
.= (upper_sum (max+ f),(T . m)) - ((lower_sum (max+ f),T) . m) by INTEGRA2:def 4
.= (upper_sum (max+ f),(T . m)) - (lower_sum (max+ f),(T . m)) by INTEGRA2:def 5
.= (Sum (upper_volume (max+ f),D)) - (lower_sum (max+ f),(T . m)) by INTEGRA1:def 9
.= (Sum (upper_volume (max+ f),D)) - (Sum (lower_volume (max+ f),D)) by INTEGRA1:def 10 ;
then A14: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:120;
A15: for j being Nat st j in Seg (len D) holds
(UV1 - LV1) . j <= (UV - LV) . j
proof
let j be Nat; :: thesis: ( j in Seg (len D) implies (UV1 - LV1) . j <= (UV - LV) . j )
set x = (UV1 - LV1) . j;
set y = (UV - LV) . j;
assume A16: j in Seg (len D) ; :: thesis: (UV1 - LV1) . j <= (UV - LV) . j
then A17: j in dom D by FINSEQ_1:def 3;
then A18: LV1 . j = (lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
A19: ( rng (f | (divset D,j)) is bounded & ex r being Real st r in rng (f | (divset D,j)) )
proof
A20: rng f is bounded_below by A1, INTEGRA1:13;
rng f is bounded_above by A1, INTEGRA1:15;
hence rng (f | (divset D,j)) is bounded by A20, RELAT_1:99, XXREAL_2:45; :: thesis: ex r being Real st r in rng (f | (divset D,j))
consider r being Real such that
A21: r in divset D,j by SUBSET_1:10;
j in dom D by A16, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A21;
then r in dom f by FUNCT_2:def 1;
then f . r in rng (f | (divset D,j)) by A21, FUNCT_1:73;
hence ex r being Real st r in rng (f | (divset D,j)) ; :: thesis: verum
end;
A22: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))
proof
set m1 = lower_bound (rng ((max+ f) | (divset D,j)));
set M1 = upper_bound (rng ((max+ f) | (divset D,j)));
set m = lower_bound (rng (f | (divset D,j)));
set M = upper_bound (rng (f | (divset D,j)));
A23: dom f = dom (max+ f) by RFUNCT_3:def 10;
A24: j in dom D by A16, FINSEQ_1:def 3;
A25: rng (f | (divset D,j)) is bounded_above by A1, Th18;
dom (f | (divset D,j)) = (dom f) /\ (divset D,j) by RELAT_1:90;
then dom (f | (divset D,j)) = A /\ (divset D,j) by FUNCT_2:def 1;
then dom (f | (divset D,j)) <> {} by A24, INTEGRA1:10, XBOOLE_1:28;
then A26: rng (f | (divset D,j)) <> {} by RELAT_1:65;
dom f = A by FUNCT_2:def 1;
then dom ((max+ f) | (divset D,j)) = A /\ (divset D,j) by A23, RELAT_1:90;
then dom ((max+ f) | (divset D,j)) <> {} by A24, INTEGRA1:10, XBOOLE_1:28;
then A27: rng ((max+ f) | (divset D,j)) <> {} by RELAT_1:65;
(max+ f) | A is bounded_below by Th15;
then A28: rng ((max+ f) | (divset D,j)) is bounded_below by Th19;
A29: rng (f | (divset D,j)) is bounded_below by A1, Th19;
(max+ f) | A is bounded_above by A1, Th14;
then A30: rng ((max+ f) | (divset D,j)) is bounded_above by Th18;
now
per cases ( ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) >= 0 ) or ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) or ( upper_bound (rng (f | (divset D,j))) <= 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) ) by A19, SEQ_4:24;
suppose A31: ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) >= 0 ) ; :: thesis: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))
A32: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j)))
proof
let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies r <= upper_bound (rng (f | (divset D,j))) )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))
then consider x being Element of A such that
A33: x in dom ((max+ f) | (divset D,j)) and
A34: r = ((max+ f) | (divset D,j)) . x by PARTFUN1:26;
A35: r = (max+ (f | (divset D,j))) . x by A34, RFUNCT_3:47;
A36: x in dom (max+ (f | (divset D,j))) by A33, RFUNCT_3:47;
then A37: x in dom (f | (divset D,j)) by RFUNCT_3:def 10;
hence r <= upper_bound (rng (f | (divset D,j))) ; :: thesis: verum
end;
A39: for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s )
proof
let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) )
assume 0 < s ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s )
then consider r being real number such that
A40: r in rng (f | (divset D,j)) and
A41: r < (lower_bound (rng (f | (divset D,j)))) + s by A26, A29, SEQ_4:def 5;
reconsider r = r as Real by XREAL_0:def 1;
r in rng ((max+ f) | (divset D,j))
proof
A42: r >= lower_bound (rng (f | (divset D,j))) by A29, A40, SEQ_4:def 5;
consider x being Element of A such that
A43: x in dom (f | (divset D,j)) and
A44: r = (f | (divset D,j)) . x by A40, PARTFUN1:26;
A45: x in dom (max+ (f | (divset D,j))) by A43, RFUNCT_3:def 10;
then (max+ (f | (divset D,j))) . x = max+ r by A44, RFUNCT_3:def 10
.= max r,0 by RFUNCT_3:def 1
.= r by A31, A42, XXREAL_0:def 10 ;
then r in rng (max+ (f | (divset D,j))) by A45, FUNCT_1:def 5;
hence r in rng ((max+ f) | (divset D,j)) by RFUNCT_3:47; :: thesis: verum
end;
hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) by A41; :: thesis: verum
end;
A46: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
lower_bound (rng (f | (divset D,j))) <= r
proof
let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies lower_bound (rng (f | (divset D,j))) <= r )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: lower_bound (rng (f | (divset D,j))) <= r
then consider x being Element of A such that
A47: x in dom ((max+ f) | (divset D,j)) and
A48: r = ((max+ f) | (divset D,j)) . x by PARTFUN1:26;
A49: x in dom (max+ (f | (divset D,j))) by A47, RFUNCT_3:47;
x in dom (max+ (f | (divset D,j))) by A47, RFUNCT_3:47;
then x in dom (f | (divset D,j)) by RFUNCT_3:def 10;
then (f | (divset D,j)) . x in rng (f | (divset D,j)) by FUNCT_1:def 5;
then A50: (f | (divset D,j)) . x >= lower_bound (rng (f | (divset D,j))) by A29, SEQ_4:def 5;
r = (max+ (f | (divset D,j))) . x by A48, RFUNCT_3:47
.= max+ ((f | (divset D,j)) . x) by A49, RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1 ;
hence lower_bound (rng (f | (divset D,j))) <= r by A31, A50, XXREAL_0:def 10; :: thesis: verum
end;
for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r )
proof
let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) )
assume 0 < s ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r )
then consider r being real number such that
A51: r in rng (f | (divset D,j)) and
A52: (upper_bound (rng (f | (divset D,j)))) - s < r by A26, A25, SEQ_4:def 4;
r in rng ((max+ f) | (divset D,j))
proof
reconsider r1 = r as Real by XREAL_0:def 1;
consider x being Element of A such that
A53: x in dom (f | (divset D,j)) and
A54: r = (f | (divset D,j)) . x by A51, PARTFUN1:26;
A55: r >= lower_bound (rng (f | (divset D,j))) by A29, A51, SEQ_4:def 5;
A56: x in dom (max+ (f | (divset D,j))) by A53, RFUNCT_3:def 10;
then (max+ (f | (divset D,j))) . x = max+ r1 by A54, RFUNCT_3:def 10
.= max r,0 by RFUNCT_3:def 1
.= r by A31, A55, XXREAL_0:def 10 ;
then r in rng (max+ (f | (divset D,j))) by A56, FUNCT_1:def 5;
hence r in rng ((max+ f) | (divset D,j)) by RFUNCT_3:47; :: thesis: verum
end;
hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) by A52; :: thesis: verum
end;
then upper_bound (rng ((max+ f) | (divset D,j))) = upper_bound (rng (f | (divset D,j))) by A27, A30, A32, SEQ_4:def 4;
hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) by A27, A28, A46, A39, SEQ_4:def 5; :: thesis: verum
end;
suppose A57: ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) ; :: thesis: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))
A58: for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
proof
let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) )
assume A59: s > 0 ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
then consider r being real number such that
A60: r in rng (f | (divset D,j)) and
A61: r < (lower_bound (rng (f | (divset D,j)))) + s by A26, A29, SEQ_4:def 5;
consider x being Element of A such that
A62: x in dom (f | (divset D,j)) and
A63: r = (f | (divset D,j)) . x by A60, PARTFUN1:26;
A64: x in dom (max+ (f | (divset D,j))) by A62, RFUNCT_3:def 10;
then A65: (max+ (f | (divset D,j))) . x = max+ ((f | (divset D,j)) . x) by RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1 ;
(max+ (f | (divset D,j))) . x in rng (max+ (f | (divset D,j))) by A64, FUNCT_1:def 5;
then A66: (max+ (f | (divset D,j))) . x in rng ((max+ f) | (divset D,j)) by RFUNCT_3:47;
A67: r - s < lower_bound (rng (f | (divset D,j))) by A61, XREAL_1:21;
now
per cases ( r < 0 or r >= 0 ) ;
suppose r < 0 ; :: thesis: ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
then 0 in rng ((max+ f) | (divset D,j)) by A63, A66, A65, XXREAL_0:def 10;
hence ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) by A59; :: thesis: verum
end;
suppose A68: r >= 0 ; :: thesis: ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
A69: r < 0 + s by A57, A67, XREAL_1:21;
r in rng ((max+ f) | (divset D,j)) by A63, A66, A65, A68, XXREAL_0:def 10;
hence ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) by A69; :: thesis: verum
end;
end;
end;
hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) ; :: thesis: verum
end;
for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r
proof
let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies 0 <= r )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: 0 <= r
then r in rng (max+ (f | (divset D,j))) by RFUNCT_3:47;
then ex x being Element of A st
( x in dom (max+ (f | (divset D,j))) & r = (max+ (f | (divset D,j))) . x ) by PARTFUN1:26;
hence 0 <= r by RFUNCT_3:40; :: thesis: verum
end;
then A70: lower_bound (rng ((max+ f) | (divset D,j))) = 0 by A27, A28, A58, SEQ_4:def 5;
for r being Real st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j)))
proof
let r be Real; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies r <= upper_bound (rng (f | (divset D,j))) )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))
then consider x being Element of A such that
A71: x in dom ((max+ f) | (divset D,j)) and
A72: r = ((max+ f) | (divset D,j)) . x by PARTFUN1:26;
A73: r = (max+ (f | (divset D,j))) . x by A72, RFUNCT_3:47;
A74: x in dom (max+ (f | (divset D,j))) by A71, RFUNCT_3:47;
then A75: x in dom (f | (divset D,j)) by RFUNCT_3:def 10;
hence r <= upper_bound (rng (f | (divset D,j))) ; :: thesis: verum
end;
then A77: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j))) ;
for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r )
proof
assume ex s being real number st
( 0 < s & ( for r being real number holds
( not r in rng ((max+ f) | (divset D,j)) or not (upper_bound (rng (f | (divset D,j)))) - s < r ) ) ) ; :: thesis: contradiction
then consider s being real number such that
A78: s > 0 and
A79: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
(upper_bound (rng (f | (divset D,j)))) - s >= r ;
consider r1 being real number such that
A80: r1 in rng (f | (divset D,j)) and
A81: (upper_bound (rng (f | (divset D,j)))) - s < r1 by A26, A25, A78, SEQ_4:def 4;
consider x being Element of A such that
A82: x in dom (f | (divset D,j)) and
A83: r1 = (f | (divset D,j)) . x by A80, PARTFUN1:26;
A84: x in dom (max+ (f | (divset D,j))) by A82, RFUNCT_3:def 10;
then x in dom ((max+ f) | (divset D,j)) by RFUNCT_3:47;
then A85: ((max+ f) | (divset D,j)) . x in rng ((max+ f) | (divset D,j)) by FUNCT_1:def 5;
(max+ (f | (divset D,j))) . x >= 0 by RFUNCT_3:40;
then ((max+ f) | (divset D,j)) . x >= 0 by RFUNCT_3:47;
then A86: (upper_bound (rng (f | (divset D,j)))) - s >= 0 by A79, A85;
((max+ f) | (divset D,j)) . x = (max+ (f | (divset D,j))) . x by RFUNCT_3:47
.= max+ ((f | (divset D,j)) . x) by A84, RFUNCT_3:def 10
.= max r1,0 by A83, RFUNCT_3:def 1
.= r1 by A81, A86, XXREAL_0:def 10 ;
hence contradiction by A79, A81, A85; :: thesis: verum
end;
then upper_bound (rng ((max+ f) | (divset D,j))) = upper_bound (rng (f | (divset D,j))) by A27, A30, A77, SEQ_4:def 4;
hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) by A57, A70, XREAL_1:15; :: thesis: verum
end;
suppose A87: ( upper_bound (rng (f | (divset D,j))) <= 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) ; :: thesis: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))
A88: for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
proof
let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) )
assume A89: s > 0 ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
consider r being Real such that
A90: r in rng ((max+ f) | (divset D,j)) by A27, SUBSET_1:10;
consider x being Element of A such that
A91: x in dom ((max+ f) | (divset D,j)) and
A92: r = ((max+ f) | (divset D,j)) . x by A90, PARTFUN1:26;
A93: x in dom (max+ (f | (divset D,j))) by A91, RFUNCT_3:47;
then x in dom (f | (divset D,j)) by RFUNCT_3:def 10;
then (f | (divset D,j)) . x in rng (f | (divset D,j)) by FUNCT_1:def 5;
then A94: (f | (divset D,j)) . x <= upper_bound (rng (f | (divset D,j))) by A25, SEQ_4:def 4;
r = (max+ (f | (divset D,j))) . x by A92, RFUNCT_3:47;
then r = max+ ((f | (divset D,j)) . x) by A93, RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1 ;
then r = 0 by A87, A94, XXREAL_0:def 10;
hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) by A89, A90; :: thesis: verum
end;
for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r
proof
let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies 0 <= r )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: 0 <= r
then consider x being Element of A such that
x in dom ((max+ f) | (divset D,j)) and
A95: r = ((max+ f) | (divset D,j)) . x by PARTFUN1:26;
r = (max+ (f | (divset D,j))) . x by A95, RFUNCT_3:47;
hence 0 <= r by RFUNCT_3:40; :: thesis: verum
end;
then A96: lower_bound (rng ((max+ f) | (divset D,j))) = 0 by A27, A28, A88, SEQ_4:def 5;
A97: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= 0
proof
let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies r <= 0 )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: r <= 0
then consider x being Element of A such that
A98: x in dom ((max+ f) | (divset D,j)) and
A99: r = ((max+ f) | (divset D,j)) . x by PARTFUN1:26;
A100: x in dom (max+ (f | (divset D,j))) by A98, RFUNCT_3:47;
then x in dom (f | (divset D,j)) by RFUNCT_3:def 10;
then (f | (divset D,j)) . x in rng (f | (divset D,j)) by FUNCT_1:def 5;
then A101: (f | (divset D,j)) . x <= upper_bound (rng (f | (divset D,j))) by A25, SEQ_4:def 4;
r = (max+ (f | (divset D,j))) . x by A99, RFUNCT_3:47;
then r = max+ ((f | (divset D,j)) . x) by A100, RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1
.= 0 by A87, A101, XXREAL_0:def 10 ;
hence r <= 0 ; :: thesis: verum
end;
for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r )
proof
let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r ) )
assume A102: s > 0 ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r )
consider r being Real such that
A103: r in rng ((max+ f) | (divset D,j)) by A27, SUBSET_1:10;
consider x being Element of A such that
x in dom ((max+ f) | (divset D,j)) and
A104: r = ((max+ f) | (divset D,j)) . x by A103, PARTFUN1:26;
r = (max+ (f | (divset D,j))) . x by A104, RFUNCT_3:47;
then r >= 0 by RFUNCT_3:40;
hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r ) by A102, A103; :: thesis: verum
end;
then upper_bound (rng ((max+ f) | (divset D,j))) = 0 by A27, A30, A97, SEQ_4:def 4;
hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) by A19, A96, SEQ_4:24, XREAL_1:50; :: thesis: verum
end;
end;
end;
hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) ; :: thesis: verum
end;
A105: LV . j = (lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by A17, INTEGRA1:def 8;
UV . j = (upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by A17, INTEGRA1:def 7;
then A106: (UV - LV) . j = ((upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) by A105, RVSUM_1:48
.= ((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) * (vol (divset D,j)) ;
UV1 . j = (upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) by A17, INTEGRA1:def 7;
then A107: (UV1 - LV1) . j = ((upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) by A18, RVSUM_1:48
.= ((upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))) * (vol (divset D,j)) ;
vol (divset D,j) >= 0 by INTEGRA1:11;
hence (UV1 - LV1) . j <= (UV - LV) . j by A107, A106, A22, XREAL_1:66; :: thesis: verum
end;
assume n <= m ; :: thesis: abs ((osc1 . m) - 0 ) < a
then A108: abs ((osc . m) - 0 ) < a by A13;
for j being Nat st j in dom F holds
0 <= F . j
proof
let j be Nat; :: thesis: ( j in dom F implies 0 <= F . j )
set r = F . j;
(max+ f) | A is bounded_below by Th15;
then A109: rng (max+ f) is bounded_below by INTEGRA1:13;
assume A110: j in dom F ; :: thesis: 0 <= F . j
j in Seg (len F) by A110, FINSEQ_1:def 3;
then A111: j in Seg (len D) by FINSEQ_1:def 18;
then A112: j in dom D by FINSEQ_1:def 3;
then A113: LV1 . j = (lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
A114: ex r being Real st r in rng ((max+ f) | (divset D,j))
proof
consider r being Real such that
A115: r in divset D,j by SUBSET_1:10;
j in dom D by A111, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A115;
then r in dom f by FUNCT_2:def 1;
then r in (dom f) /\ (divset D,j) by A115, XBOOLE_0:def 4;
then r in dom (f | (divset D,j)) by RELAT_1:90;
then r in dom (max+ (f | (divset D,j))) by RFUNCT_3:def 10;
then r in dom ((max+ f) | (divset D,j)) by RFUNCT_3:47;
then ((max+ f) | (divset D,j)) . r in rng ((max+ f) | (divset D,j)) by FUNCT_1:def 5;
hence ex r being Real st r in rng ((max+ f) | (divset D,j)) ; :: thesis: verum
end;
(max+ f) | A is bounded_above by A1, Th14;
then rng (max+ f) is bounded_above by INTEGRA1:15;
then rng ((max+ f) | (divset D,j)) is bounded by A109, RELAT_1:99, XXREAL_2:45;
then A116: (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) >= 0 by A114, SEQ_4:24, XREAL_1:50;
UV1 . j = (upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) by A112, INTEGRA1:def 7;
then A117: F . j = ((upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) by A110, A113, VALUED_1:13
.= ((upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))) * (vol (divset D,j)) ;
vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= F . j by A117, A116; :: thesis: verum
end;
then A118: osc1 . m >= 0 by A14, RVSUM_1:114;
then A119: abs ((osc1 . m) - 0 ) = osc1 . m by ABSVALUE:def 1;
osc . m = ((upper_sum f,T) . m) + ((- (lower_sum f,T)) . m) by SEQ_1:11
.= ((upper_sum f,T) . m) + (- ((lower_sum f,T) . m)) by SEQ_1:14
.= ((upper_sum f,T) . m) - ((lower_sum f,T) . m)
.= (upper_sum f,(T . m)) - ((lower_sum f,T) . m) by INTEGRA2:def 4
.= (upper_sum f,(T . m)) - (lower_sum f,(T . m)) by INTEGRA2:def 5
.= (Sum (upper_volume f,D)) - (lower_sum f,(T . m)) by INTEGRA1:def 9
.= (Sum (upper_volume f,D)) - (Sum (lower_volume f,D)) by INTEGRA1:def 10 ;
then osc . m = Sum (UV - LV) by RVSUM_1:120;
then A120: osc1 . m <= osc . m by A14, A15, RVSUM_1:112;
then abs (osc . m) = osc . m by A118, ABSVALUE:def 1;
hence abs ((osc1 . m) - 0 ) < a by A108, A120, A119, XXREAL_0:2; :: thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a ; :: thesis: verum
end;
then osc1 is convergent by SEQ_2:def 6;
then A121: lim ((upper_sum (max+ f),T) - (lower_sum (max+ f),T)) = 0 by A12, SEQ_2:def 7;
A122: lower_sum (max+ f),T is convergent by A3, A5, A4, A6, A7, Th8;
upper_sum (max+ f),T is convergent by A3, A5, A4, A6, A7, Th9;
hence (lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0 by A122, A121, SEQ_2:26; :: thesis: verum
end;
hence max+ f is integrable by A3, A5, A4, Th12; :: thesis: verum