let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st f | A is non-decreasing & A c= dom f holds
f is_integrable_on A
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | A is non-decreasing & A c= dom f implies f is_integrable_on A )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis: f is_integrable_on A
A3: for D being Division of A
for k being Element of NAT st k in dom D holds
( 0 <= ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) & ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) )
proof
let D be Division of A; :: thesis: for k being Element of NAT st k in dom D holds
( 0 <= ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) & ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) )
let k be Element of NAT ; :: thesis: ( k in dom D implies ( 0 <= ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) & ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) ) )
assume A4: k in dom D ; :: thesis: ( 0 <= ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) & ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) )
then A5: divset D,k c= A by INTEGRA1:10;
A6: f | (divset D,k) is non-decreasing by A1, A4, INTEGRA1:10, RFUNCT_2:62;
divset D,k c= dom f by A2, A5, XBOOLE_1:1;
then A7: ( inf (rng (f | (divset D,k))) = f . (inf (divset D,k)) & sup (rng (f | (divset D,k))) = f . (sup (divset D,k)) ) by A6, Th15;
k in Seg (len D) by A4, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then A8: ( (upper_volume (f || A),D) . k = (sup (rng ((f || A) | (divset D,k)))) * (vol (divset D,k)) & (lower_volume (f || A),D) . k = (inf (rng ((f || A) | (divset D,k)))) * (vol (divset D,k)) ) by INTEGRA1:def 7, INTEGRA1:def 8;
A9: rng (f | (divset D,k)) = rng ((f || A) | (divset D,k)) by A5, FUNCT_1:82;
then A10: ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) = ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (vol (divset D,k)) by A7, A8;
dom (f | (divset D,k)) = (dom f) /\ (divset D,k) by RELAT_1:90
.= divset D,k by A2, A5, XBOOLE_1:1, XBOOLE_1:28 ;
then A11: rng (f | (divset D,k)) <> {} by RELAT_1:65;
rng (f | A) is bounded by A1, A2, Th14;
then rng (f | (divset D,k)) is bounded by A9, RELAT_1:99, XXREAL_2:45;
then A12: (f . (sup (divset D,k))) - (f . (inf (divset D,k))) >= 0 by A7, A11, SEQ_4:24, XREAL_1:50;
vol (divset D,k) >= 0 by INTEGRA1:11;
then 0 * (vol (divset D,k)) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (vol (divset D,k)) by A12;
hence 0 <= ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) by A7, A8, A9; :: thesis: ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D)
vol (divset D,k) <= delta D
proof
A13: k in Seg (len D) by A4, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then A14: vol (divset D,k) = (upper_volume (chi A,A),D) . k by INTEGRA1:22;
k in Seg (len (upper_volume (chi A,A),D)) by A13, INTEGRA1:def 7;
then k in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then vol (divset D,k) in rng (upper_volume (chi A,A),D) by A14, FUNCT_1:def 5;
then vol (divset D,k) <= max (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 8;
hence vol (divset D,k) <= delta D by INTEGRA1:def 19; :: thesis: verum
end;
hence ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) by A10, A12, XREAL_1:66; :: thesis: verum
end;
A15: for D being Division of A holds
( (upper_sum (f || A),D) - (lower_sum (f || A),D) <= (delta D) * ((f . (sup A)) - (f . (inf A))) & (upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0 )
proof
let D be Division of A; :: thesis: ( (upper_sum (f || A),D) - (lower_sum (f || A),D) <= (delta D) * ((f . (sup A)) - (f . (inf A))) & (upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0 )
( len (upper_volume (f || A),D) = len D & len (lower_volume (f || A),D) = len D ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A16: Sum ((upper_volume (f || A),D) - (lower_volume (f || A),D)) = (Sum (upper_volume (f || A),D)) - (Sum (lower_volume (f || A),D)) by Th2
.= (upper_sum (f || A),D) - (Sum (lower_volume (f || A),D)) by INTEGRA1:def 9
.= (upper_sum (f || A),D) - (lower_sum (f || A),D) by INTEGRA1:def 10 ;
A17: (len D) - 1 in NAT
proof
len D >= 1 by NAT_1:14;
then consider j being Nat such that
A18: len D = 1 + j by NAT_1:10;
thus (len D) - 1 in NAT by A18, ORDINAL1:def 13; :: thesis: verum
end;
deffunc H1( Nat) -> Element of REAL = f . (sup (divset D,$1));
consider F1 being FinSequence of REAL such that
A19: ( len F1 = len D & ( for i being Nat st i in dom F1 holds
F1 . i = H1(i) ) ) from FINSEQ_2:sch 1();
 A20: dom F1 = Seg (len D) by A19, FINSEQ_1:def 3;
deffunc H2( Nat) -> Element of REAL = f . (inf (divset D,$1));
consider F2 being FinSequence of REAL such that
A21: ( len F2 = len D & ( for i being Nat st i in dom F2 holds
F2 . i = H2(i) ) ) from FINSEQ_2:sch 1();
 A22: dom F2 = Seg (len D) by A21, FINSEQ_1:def 3;
consider k1 being Element of NAT such that
A23: k1 = (len D) - 1 by A17;
deffunc H3( Nat) -> Element of REAL = f . (sup (divset D,$1));
consider F being FinSequence of REAL such that
A24: ( len F = k1 & ( for i being Nat st i in dom F holds
F . i = H3(i) ) ) from FINSEQ_2:sch 1();
 A25: dom F = Seg k1 by A24, FINSEQ_1:def 3;
( F1 = F ^ <*(f . (sup A))*> & F2 = <*(f . (inf A))*> ^ F )
proof
A26: len (F ^ <*(f . (sup A))*>) = (len F) + (len <*(f . (sup A))*>) by FINSEQ_1:35
.= ((len D) - 1) + 1 by A23, A24, FINSEQ_1:56
.= len D ;
for i being Nat st 1 <= i & i <= len F1 holds
F1 . i = (F ^ <*(f . (sup A))*>) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len F1 implies F1 . i = (F ^ <*(f . (sup A))*>) . i )
assume A27: ( 1 <= i & i <= len F1 ) ; :: thesis: F1 . i = (F ^ <*(f . (sup A))*>) . i
now
per cases ( i <= len F or i > len F ) ;
suppose i <= len F ; :: thesis: F1 . i = (F ^ <*(f . (sup A))*>) . i
then A28: ( i in Seg (len F1) & i in Seg (len F) ) by A27, FINSEQ_1:3;
then A29: ( F1 . i = f . (sup (divset D,i)) & F . i = f . (sup (divset D,i)) ) by A19, A24, A20, A25;
i in dom F by A28, FINSEQ_1:def 3;
hence F1 . i = (F ^ <*(f . (sup A))*>) . i by A29, FINSEQ_1:def 7; :: thesis: verum
end;
suppose i > len F ; :: thesis: F1 . i = (F ^ <*(f . (sup A))*>) . i
then A30: i >= (len F) + 1 by NAT_1:13;
then A31: i = (len F) + 1 by A19, A23, A24, A27, XXREAL_0:1;
i in Seg (len F1) by A27, FINSEQ_1:3;
then A32: ( F1 . i = f . (sup (divset D,i)) & i in dom D ) by A19, A20, FINSEQ_1:def 3;
sup (divset D,i) = D . i
proof
now
per cases ( i = 1 or i <> 1 ) ;
suppose i = 1 ; :: thesis: sup (divset D,i) = D . i
hence sup (divset D,i) = D . i by A32, INTEGRA1:def 5; :: thesis: verum
end;
suppose i <> 1 ; :: thesis: sup (divset D,i) = D . i
hence sup (divset D,i) = D . i by A32, INTEGRA1:def 5; :: thesis: verum
end;
end;
end;
hence sup (divset D,i) = D . i ; :: thesis: verum
end;
then F1 . i = f . (D . (len D)) by A19, A23, A24, A27, A30, A32, XXREAL_0:1
.= f . (sup A) by INTEGRA1:def 2 ;
hence F1 . i = (F ^ <*(f . (sup A))*>) . i by A31, FINSEQ_1:59; :: thesis: verum
end;
end;
end;
hence F1 . i = (F ^ <*(f . (sup A))*>) . i ; :: thesis: verum
end;
hence F1 = F ^ <*(f . (sup A))*> by A19, A26, FINSEQ_1:18; :: thesis: F2 = <*(f . (inf A))*> ^ F
A33: len (<*(f . (inf A))*> ^ F) = (len <*(f . (inf A))*>) + (len F) by FINSEQ_1:35
.= 1 + ((len D) - 1) by A23, A24, FINSEQ_1:56
.= len D ;
for i being Nat st 1 <= i & i <= len F2 holds
F2 . i = (<*(f . (inf A))*> ^ F) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len F2 implies F2 . i = (<*(f . (inf A))*> ^ F) . i )
assume A34: ( 1 <= i & i <= len F2 ) ; :: thesis: F2 . i = (<*(f . (inf A))*> ^ F) . i
per cases ( i = 1 or i <> 1 ) ;
suppose A35: i = 1 ; :: thesis: F2 . i = (<*(f . (inf A))*> ^ F) . i
A36: i in Seg (len D) by A21, A34, FINSEQ_1:3;
then A37: i in dom D by FINSEQ_1:def 3;
F2 . i = f . (inf (divset D,i)) by A21, A36, A22
.= f . (inf A) by A35, A37, INTEGRA1:def 5 ;
hence F2 . i = (<*(f . (inf A))*> ^ F) . i by A35, FINSEQ_1:58; :: thesis: verum
end;
suppose A38: i <> 1 ; :: thesis: F2 . i = (<*(f . (inf A))*> ^ F) . i
A39: i in Seg (len D) by A21, A34, FINSEQ_1:3;
then A40: i in dom D by FINSEQ_1:def 3;
A41: F2 . i = f . (inf (divset D,i)) by A21, A39, A22
.= f . (D . (i - 1)) by A38, A40, INTEGRA1:def 5 ;
A42: i > 1 by A34, A38, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A43: (len <*(f . (inf A))*>) + 1 <= i by FINSEQ_1:56;
len F2 = 1 + ((len D) - 1) by A21
.= (len <*(f . (inf A))*>) + (len F) by A23, A24, FINSEQ_1:56 ;
then A44: (<*(f . (inf A))*> ^ F) . i = F . (i - (len <*(f . (inf A))*>)) by A34, A43, FINSEQ_1:36
.= F . (i - 1) by FINSEQ_1:56 ;
reconsider k2 = i - 1 as Element of NAT by A38, A40, INTEGRA1:9;
( 1 + 1 <= k2 + 1 & k2 + 1 <= len F2 ) by A34, A42, NAT_1:13;
then A45: ( 1 <= k2 & k2 <= (len D) - 1 ) by A21, XREAL_1:21;
then A46: k2 in Seg k1 by A23, FINSEQ_1:3;
sup (divset D,k2) = D . (i - 1)
proof
len D <= (len D) + 1 by NAT_1:13;
then (len D) - 1 <= len D by XREAL_1:22;
then ( 1 <= k2 & k2 <= len D ) by A45, XXREAL_0:2;
then k2 in Seg (len D) by FINSEQ_1:3;
then A47: k2 in dom D by FINSEQ_1:def 3;
per cases ( k2 = 1 or k2 <> 1 ) ;
suppose k2 = 1 ; :: thesis: sup (divset D,k2) = D . (i - 1)
hence sup (divset D,k2) = D . (i - 1) by A47, INTEGRA1:def 5; :: thesis: verum
end;
suppose k2 <> 1 ; :: thesis: sup (divset D,k2) = D . (i - 1)
hence sup (divset D,k2) = D . (i - 1) by A47, INTEGRA1:def 5; :: thesis: verum
end;
end;
end;
hence F2 . i = (<*(f . (inf A))*> ^ F) . i by A24, A41, A44, A46, A25; :: thesis: verum
end;
end;
end;
hence F2 = <*(f . (inf A))*> ^ F by A21, A33, FINSEQ_1:18; :: thesis: verum
end;
then A48: Sum (F1 - F2) = (f . (sup A)) - (f . (inf A)) by Th1;
( len (upper_volume (f || A),D) = len D & len (lower_volume (f || A),D) = len D ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A49: len ((upper_volume (f || A),D) - (lower_volume (f || A),D)) = len D by Th2;
(delta D) * (F1 - F2) = ((delta D) multreal ) * (F1 - F2) by RVSUM_1:def 7;
then A50: len ((delta D) * (F1 - F2)) = len (F1 - F2) by FINSEQ_2:37;
A51: len (F1 - F2) = len D by A19, A21, Th2;
A52: len ((upper_volume (f || A),D) - (lower_volume (f || A),D)) = len ((delta D) * (F1 - F2)) by A19, A21, A49, A50, Th2;
for k being Element of NAT st k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) holds
((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k <= ((delta D) * (F1 - F2)) . k
proof
let k be Element of NAT ; :: thesis: ( k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) implies ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k <= ((delta D) * (F1 - F2)) . k )
assume A53: k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) ; :: thesis: ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k <= ((delta D) * (F1 - F2)) . k
then A54: k in Seg (len D) by A49, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) by A3;
then A55: ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) by A53, VALUED_1:13;
k in Seg (len (F1 - F2)) by A49, A51, A53, FINSEQ_1:def 3;
then A56: k in dom (F1 - F2) by FINSEQ_1:def 3;
( F1 . k = f . (sup (divset D,k)) & F2 . k = f . (inf (divset D,k)) ) by A19, A21, A54, A20, A22;
then ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k <= (delta D) * ((F1 - F2) . k) by A55, A56, VALUED_1:13;
hence ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k <= ((delta D) * (F1 - F2)) . k by RVSUM_1:66; :: thesis: verum
end;
then Sum ((upper_volume (f || A),D) - (lower_volume (f || A),D)) <= Sum ((delta D) * (F1 - F2)) by A52, Th3;
hence (upper_sum (f || A),D) - (lower_sum (f || A),D) <= (delta D) * ((f . (sup A)) - (f . (inf A))) by A16, A48, RVSUM_1:117; :: thesis: (upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0
for k being Nat st k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) holds
0 <= ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k
proof
let k be Nat; :: thesis: ( k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) implies 0 <= ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k )
assume A57: k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) ; :: thesis: 0 <= ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k
set r = ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k;
A58: ( len (upper_volume (f || A),D) = len D & len (lower_volume (f || A),D) = len D ) by INTEGRA1:def 7, INTEGRA1:def 8;
k in Seg (len ((upper_volume (f || A),D) - (lower_volume (f || A),D))) by A57, FINSEQ_1:def 3;
then k in Seg (len D) by A58, Th2;
then A59: k in dom D by FINSEQ_1:def 3;
((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k = ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) by A57, VALUED_1:13;
hence 0 <= ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k by A3, A59; :: thesis: verum
end;
hence (upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0 by A16, RVSUM_1:114; :: thesis: verum
end;
A60: ( f || A is total & (f || A) | A is bounded )
proof
A61: dom (f || A) = (dom f) /\ A by RELAT_1:90
.= A by A2, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def 4; :: thesis: (f || A) | A is bounded
consider x being Real such that
A62: x in A by SUBSET_1:10;
( inf A <= x & x <= sup A ) by A62, INTEGRA2:1;
then A63: inf A <= sup A by XXREAL_0:2;
A64: (f || A) | A is bounded_above
proof
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x <= (f || A) . (sup A)
proof
let x be set ; :: thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x <= (f || A) . (sup A) )
assume A65: x in A /\ (dom (f || A)) ; :: thesis: (f || A) . x <= (f || A) . (sup A)
then A66: x in A ;
A67: sup A in A by A63, INTEGRA2:1;
then A68: ( x in A /\ (dom f) & sup A in A /\ (dom f) ) by A2, A66, XBOOLE_1:28;
reconsider x = x as Element of A by A65;
A69: x <= sup A by INTEGRA2:1;
( f . x = (f | A) . x & f . (sup A) = (f | A) . (sup A) ) by A61, A67, FUNCT_1:70;
hence (f || A) . x <= (f || A) . (sup A) by A1, A68, A69, RFUNCT_2:48; :: thesis: verum
end;
hence (f || A) | A is bounded_above by RFUNCT_1:87; :: thesis: verum
end;
(f || A) | A is bounded_below
proof
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x >= (f || A) . (inf A)
proof
let x be set ; :: thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x >= (f || A) . (inf A) )
assume A70: x in A /\ (dom (f || A)) ; :: thesis: (f || A) . x >= (f || A) . (inf A)
then A71: x in A ;
A72: inf A in A by A63, INTEGRA2:1;
then A73: ( x in A /\ (dom f) & inf A in A /\ (dom f) ) by A2, A71, XBOOLE_1:28;
reconsider x = x as Element of A by A70;
A74: x >= inf A by INTEGRA2:1;
( f . x = (f | A) . x & f . (inf A) = (f | A) . (inf A) ) by A61, A72, FUNCT_1:70;
hence (f || A) . x >= (f || A) . (inf A) by A1, A73, A74, RFUNCT_2:48; :: thesis: verum
end;
hence (f || A) | A is bounded_below by RFUNCT_1:88; :: thesis: verum
end;
hence (f || A) | A is bounded by A64; :: thesis: verum
end;
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f || A),T)) - (lim (lower_sum (f || A),T)) = 0
proof
let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (f || A),T)) - (lim (lower_sum (f || A),T)) = 0 )
assume A76: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum (f || A),T)) - (lim (lower_sum (f || A),T)) = 0
A77: for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
proof
let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r )
assume A78: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
consider x being Real such that
A79: x in A by SUBSET_1:10;
( inf A <= x & x <= sup A ) by A79, INTEGRA2:1;
then A80: inf A <= sup A by XXREAL_0:2;
then A81: ( inf A in A & sup A in A ) by INTEGRA2:1;
A = A /\ (dom f) by A2, XBOOLE_1:28;
then A82: f . (inf A) <= f . (sup A) by A1, A80, A81, RFUNCT_2:48;
now
per cases ( f . (inf A) = f . (sup A) or f . (inf A) < f . (sup A) ) by A82, XXREAL_0:1;
suppose A83: f . (inf A) = f . (sup A) ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
for m being Element of NAT st 0 <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
proof
let m be Element of NAT ; :: thesis: ( 0 <= m implies abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r )
assume 0 <= m ; :: thesis: abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
reconsider D1 = T . m as Division of A ;
A84: ( (upper_sum (f || A),D1) - (lower_sum (f || A),D1) <= (delta D1) * ((f . (sup A)) - (f . (inf A))) & (upper_sum (f || A),D1) - (lower_sum (f || A),D1) >= 0 ) by A15;
((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m = ((upper_sum (f || A),T) . m) + ((- (lower_sum (f || A),T)) . m) by SEQ_1:11
.= ((upper_sum (f || A),T) . m) + (- ((lower_sum (f || A),T) . m)) by SEQ_1:14
.= (upper_sum (f || A),D1) + (- ((lower_sum (f || A),T) . m)) by INTEGRA2:def 4
.= (upper_sum (f || A),D1) + (- (lower_sum (f || A),D1)) by INTEGRA2:def 5 ;
hence abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r by A78, A83, A84, ABSVALUE:def 1; :: thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r ; :: thesis: verum
end;
suppose f . (inf A) < f . (sup A) ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
then A85: (f . (sup A)) - (f . (inf A)) > 0 by XREAL_1:52;
then r / ((f . (sup A)) - (f . (inf A))) > 0 by A78, XREAL_1:141;
then consider n being Element of NAT such that
A86: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0 ) < r / ((f . (sup A)) - (f . (inf A))) by A76, SEQ_2:def 7;
A87: for m being Element of NAT st n <= m holds
(delta T) . m < r / ((f . (sup A)) - (f . (inf A)))
proof
let m be Element of NAT ; :: thesis: ( n <= m implies (delta T) . m < r / ((f . (sup A)) - (f . (inf A))) )
assume n <= m ; :: thesis: (delta T) . m < r / ((f . (sup A)) - (f . (inf A)))
then A88: abs (((delta T) . m) - 0 ) < r / ((f . (sup A)) - (f . (inf A))) by A86;
(delta T) . m <= abs ((delta T) . m) by ABSVALUE:11;
hence (delta T) . m < r / ((f . (sup A)) - (f . (inf A))) by A88, XXREAL_0:2; :: thesis: verum
end;
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
proof
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r )
assume n <= m ; :: thesis: abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r
then (delta T) . m < r / ((f . (sup A)) - (f . (inf A))) by A87;
then A89: ((delta T) . m) * ((f . (sup A)) - (f . (inf A))) < r by A85, XREAL_1:81;
reconsider D = T . m as Division of A ;
A90: (delta D) * ((f . (sup A)) - (f . (inf A))) < r by A89, INTEGRA2:def 3;
A91: ( (upper_sum (f || A),D) - (lower_sum (f || A),D) <= (delta D) * ((f . (sup A)) - (f . (inf A))) & (upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0 ) by A15;
then A92: (upper_sum (f || A),D) - (lower_sum (f || A),D) < r by A90, XXREAL_0:2;
abs ((upper_sum (f || A),D) - (lower_sum (f || A),D)) = abs ((((upper_sum (f || A),T) . m) - (lower_sum (f || A),D)) - 0 ) by INTEGRA2:def 4
.= abs ((((upper_sum (f || A),T) . m) - ((lower_sum (f || A),T) . m)) - 0 ) by INTEGRA2:def 5
.= abs ((((upper_sum (f || A),T) . m) + (- ((lower_sum (f || A),T) . m))) - 0 )
.= abs ((((upper_sum (f || A),T) . m) + ((- (lower_sum (f || A),T)) . m)) - 0 ) by SEQ_1:14
.= abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) by SEQ_1:11 ;
hence abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r by A91, A92, ABSVALUE:def 1; :: thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r ; :: thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r ; :: thesis: verum
end;
A93: ( upper_sum (f || A),T is convergent & lower_sum (f || A),T is convergent ) by A60, A76, INTEGRA4:8, INTEGRA4:9;
then (upper_sum (f || A),T) - (lower_sum (f || A),T) is convergent by SEQ_2:25;
then lim ((upper_sum (f || A),T) - (lower_sum (f || A),T)) = 0 by A77, SEQ_2:def 7;
hence (lim (upper_sum (f || A),T)) - (lim (lower_sum (f || A),T)) = 0 by A93, SEQ_2:26; :: thesis: verum
end;
then f || A is integrable by A60, INTEGRA4:12;
hence f is_integrable_on A by Def2; :: thesis: verum