:: INTEGRA6 semantic presentation
begin
theorem Th1: :: INTEGRA6:1
for a, b, c, d being real number st a <= b & c <= d & a + c = b + d holds
( a = b & c = d )
proof
let a, b, c, d be real number ; ::_thesis: ( a <= b & c <= d & a + c = b + d implies ( a = b & c = d ) )
assume that
A1: ( a <= b & c <= d ) and
A2: a + c = b + d ; ::_thesis: ( a = b & c = d )
assume ( not a = b or not c = d ) ; ::_thesis: contradiction
then ( a < b or c < d ) by A1, XXREAL_0:1;
hence contradiction by A1, A2, XREAL_1:8; ::_thesis: verum
end;
theorem Th2: :: INTEGRA6:2
for a, b, x being real number st a <= b holds
].(x - a),(x + a).[ c= ].(x - b),(x + b).[
proof
let a, b, x be real number ; ::_thesis: ( a <= b implies ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ )
assume a <= b ; ::_thesis: ].(x - a),(x + a).[ c= ].(x - b),(x + b).[
then ( x - b <= x - a & x + a <= x + b ) by XREAL_1:7, XREAL_1:10;
hence ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ by XXREAL_1:46; ::_thesis: verum
end;
theorem Th3: :: INTEGRA6:3
for R being Relation
for A, B, C being set st A c= B & A c= C holds
(R | B) | A = (R | C) | A
proof
let R be Relation; ::_thesis: for A, B, C being set st A c= B & A c= C holds
(R | B) | A = (R | C) | A
let A, B, C be set ; ::_thesis: ( A c= B & A c= C implies (R | B) | A = (R | C) | A )
assume that
A1: A c= B and
A2: A c= C ; ::_thesis: (R | B) | A = (R | C) | A
(R | C) | A = R | A by A2, RELAT_1:74;
hence (R | B) | A = (R | C) | A by A1, RELAT_1:74; ::_thesis: verum
end;
theorem Th4: :: INTEGRA6:4
for A, B, C being set st A c= B & A c= C holds
(chi (B,B)) | A = (chi (C,C)) | A
proof
let A, B, C be set ; ::_thesis: ( A c= B & A c= C implies (chi (B,B)) | A = (chi (C,C)) | A )
assume that
A1: A c= B and
A2: A c= C ; ::_thesis: (chi (B,B)) | A = (chi (C,C)) | A
A3: now__::_thesis:_(_not_A_is_empty_implies_(chi_(B,B))_|_A_=_(chi_(C,C))_|_A_)
A4: dom ((chi (C,C)) | A) = (dom (chi (C,C))) /\ A by RELAT_1:61;
assume A5: not A is empty ; ::_thesis: (chi (B,B)) | A = (chi (C,C)) | A
then not C is empty by A2, XBOOLE_1:58, XBOOLE_1:61;
then dom ((chi (C,C)) | A) = C /\ A by A4, RFUNCT_1:61;
then A6: dom ((chi (C,C)) | A) = A by A2, XBOOLE_1:28;
A7: dom ((chi (B,B)) | A) = (dom (chi (B,B))) /\ A by RELAT_1:61;
not B is empty by A1, A5, XBOOLE_1:58, XBOOLE_1:61;
then dom ((chi (B,B)) | A) = B /\ A by A7, RFUNCT_1:61;
then A8: dom ((chi (B,B)) | A) = A by A1, XBOOLE_1:28;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
((chi_(B,B))_|_A)_._x_=_((chi_(C,C))_|_A)_._x
let x be set ; ::_thesis: ( x in A implies ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x )
assume A9: x in A ; ::_thesis: ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x
then ((chi (B,B)) | A) . x = (chi (B,B)) . x by A8, FUNCT_1:47;
then ((chi (B,B)) | A) . x = 1 by A1, A9, RFUNCT_1:61;
then ((chi (B,B)) | A) . x = (chi (C,C)) . x by A2, A9, RFUNCT_1:61;
hence ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x by A6, A9, FUNCT_1:47; ::_thesis: verum
end;
hence (chi (B,B)) | A = (chi (C,C)) | A by A8, A6, FUNCT_1:2; ::_thesis: verum
end;
now__::_thesis:_(_A_is_empty_implies_(chi_(B,B))_|_A_=_(chi_(C,C))_|_A_)
assume A10: A is empty ; ::_thesis: (chi (B,B)) | A = (chi (C,C)) | A
then (chi (B,B)) | A = {} ;
hence (chi (B,B)) | A = (chi (C,C)) | A by A10; ::_thesis: verum
end;
hence (chi (B,B)) | A = (chi (C,C)) | A by A3; ::_thesis: verum
end;
theorem Th5: :: INTEGRA6:5
for a, b being real number st a <= b holds
vol ['a,b'] = b - a
proof
let a, b be real number ; ::_thesis: ( a <= b implies vol ['a,b'] = b - a )
assume a <= b ; ::_thesis: vol ['a,b'] = b - a
then A1: ['a,b'] = [.a,b.] by INTEGRA5:def_3;
then A2: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by INTEGRA1:4;
then a = lower_bound [.a,b.] by A1, INTEGRA1:5;
hence vol ['a,b'] = b - a by A1, A2, INTEGRA1:5; ::_thesis: verum
end;
theorem Th6: :: INTEGRA6:6
for a, b being real number holds vol ['(min (a,b)),(max (a,b))'] = abs (b - a)
proof
let a, b be real number ; ::_thesis: vol ['(min (a,b)),(max (a,b))'] = abs (b - a)
percases ( a <= b or not a <= b ) ;
supposeA1: a <= b ; ::_thesis: vol ['(min (a,b)),(max (a,b))'] = abs (b - a)
then ( min (a,b) = a & max (a,b) = b ) by XXREAL_0:def_9, XXREAL_0:def_10;
then A2: vol ['(min (a,b)),(max (a,b))'] = b - a by Th5, XXREAL_0:25;
0 <= b - a by A1, XREAL_1:48;
hence vol ['(min (a,b)),(max (a,b))'] = abs (b - a) by A2, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA3: not a <= b ; ::_thesis: vol ['(min (a,b)),(max (a,b))'] = abs (b - a)
then 0 <= a - b by XREAL_1:48;
then A4: a - b = abs (a - b) by ABSVALUE:def_1
.= abs (b - a) by COMPLEX1:60 ;
( min (a,b) = b & max (a,b) = a ) by A3, XXREAL_0:def_9, XXREAL_0:def_10;
hence vol ['(min (a,b)),(max (a,b))'] = abs (b - a) by A4, Th5, XXREAL_0:17; ::_thesis: verum
end;
end;
end;
begin
Lm1: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f holds
f || A is Function of A,REAL
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st A c= dom f holds
f || A is Function of A,REAL
let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f implies f || A is Function of A,REAL )
rng f c= REAL ;
then A1: f is Function of (dom f),REAL by FUNCT_2:2;
assume A c= dom f ; ::_thesis: f || A is Function of A,REAL
hence f || A is Function of A,REAL by A1, FUNCT_2:32; ::_thesis: verum
end;
theorem Th7: :: INTEGRA6:7
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f & f is_integrable_on A & f | A is bounded holds
( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st A c= dom f & f is_integrable_on A & f | A is bounded holds
( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) )
let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) )
A1: abs (f || A) = (abs f) || A by RFUNCT_1:46;
assume A c= dom f ; ::_thesis: ( not f is_integrable_on A or not f | A is bounded or ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) )
then A2: f || A is Function of A,REAL by Lm1;
assume ( f is_integrable_on A & f | A is bounded ) ; ::_thesis: ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) )
then A3: ( f || A is integrable & (f || A) | A is bounded ) by INTEGRA5:def_1;
thus ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) by A3, A2, A1, INTEGRA4:23, INTEGRA5:def_1; ::_thesis: verum
end;
theorem Th8: :: INTEGRA6:8
for a, b being real number
for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
abs (integral (f,a,b)) <= integral ((abs f),a,b)
proof
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
abs (integral (f,a,b)) <= integral ((abs f),a,b)
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies abs (integral (f,a,b)) <= integral ((abs f),a,b) )
assume a <= b ; ::_thesis: ( not ['a,b'] c= dom f or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or abs (integral (f,a,b)) <= integral ((abs f),a,b) )
then ( integral (f,a,b) = integral (f,['a,b']) & integral ((abs f),a,b) = integral ((abs f),['a,b']) ) by INTEGRA5:def_4;
hence ( not ['a,b'] c= dom f or not f is_integrable_on ['a,b'] or not f | ['a,b'] is bounded or abs (integral (f,a,b)) <= integral ((abs f),a,b) ) by Th7; ::_thesis: verum
end;
theorem Th9: :: INTEGRA6:9
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL
for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL
for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let f be PartFunc of REAL,REAL; ::_thesis: for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let r be Real; ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) )
assume that
A1: A c= dom f and
A2: ( f is_integrable_on A & f | A is bounded ) ; ::_thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
A3: ( f || A is integrable & (f || A) | A is bounded ) by A2, INTEGRA5:def_1;
rng f c= REAL ;
then f is Function of (dom f),REAL by FUNCT_2:2;
then A4: f | A is Function of A,REAL by A1, FUNCT_2:32;
r (#) (f || A) = (r (#) f) | A by RFUNCT_1:49;
then (r (#) f) || A is integrable by A3, A4, INTEGRA2:31;
hence r (#) f is_integrable_on A by INTEGRA5:def_1; ::_thesis: integral ((r (#) f),A) = r * (integral (f,A))
integral ((r (#) f),A) = integral (r (#) (f || A)) by RFUNCT_1:49;
hence integral ((r (#) f),A) = r * (integral (f,A)) by A3, A4, INTEGRA2:31; ::_thesis: verum
end;
theorem Th10: :: INTEGRA6:10
for a, b, c being real number
for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
integral ((c (#) f),a,b) = c * (integral (f,a,b))
proof
let a, b, c be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
integral ((c (#) f),a,b) = c * (integral (f,a,b))
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies integral ((c (#) f),a,b) = c * (integral (f,a,b)) )
A1: c is Real by XREAL_0:def_1;
assume that
A2: a <= b and
A3: ( ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ; ::_thesis: integral ((c (#) f),a,b) = c * (integral (f,a,b))
( integral (f,a,b) = integral (f,['a,b']) & integral ((c (#) f),a,b) = integral ((c (#) f),['a,b']) ) by A2, INTEGRA5:def_4;
hence integral ((c (#) f),a,b) = c * (integral (f,a,b)) by A1, A3, Th9; ::_thesis: verum
end;
theorem Th11: :: INTEGRA6:11
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds
( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds
( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) )
let f, g be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded implies ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) )
assume that
A1: ( A c= dom f & A c= dom g ) and
A2: f is_integrable_on A and
A3: f | A is bounded and
A4: g is_integrable_on A and
A5: g | A is bounded ; ::_thesis: ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) )
A6: ( (f || A) | A is bounded & (g || A) | A is bounded ) by A3, A5;
A7: ( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1;
A8: ( (f || A) + (g || A) = (f + g) || A & (f || A) - (g || A) = (f - g) || A ) by RFUNCT_1:44, RFUNCT_1:47;
A9: ( f || A is integrable & g || A is integrable ) by A2, A4, INTEGRA5:def_1;
then ( (f || A) + (g || A) is integrable & (f || A) - (g || A) is integrable ) by A6, A7, INTEGRA1:57, INTEGRA2:33;
hence ( f + g is_integrable_on A & f - g is_integrable_on A ) by A8, INTEGRA5:def_1; ::_thesis: ( integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) )
thus ( integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) by A9, A6, A7, A8, INTEGRA1:57, INTEGRA2:33; ::_thesis: verum
end;
theorem Th12: :: INTEGRA6:12
for a, b being real number
for f, g being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded holds
( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
proof
let a, b be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded holds
( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded implies ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) )
assume that
A1: a <= b and
A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) ; ::_thesis: ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
A3: ( integral ((f + g),a,b) = integral ((f + g),['a,b']) & integral ((f - g),a,b) = integral ((f - g),['a,b']) ) by A1, INTEGRA5:def_4;
( integral (f,a,b) = integral (f,['a,b']) & integral (g,a,b) = integral (g,['a,b']) ) by A1, INTEGRA5:def_4;
hence ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) by A2, A3, Th11; ::_thesis: verum
end;
theorem :: INTEGRA6:13
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL st f | A is bounded & g | A is bounded holds
(f (#) g) | A is bounded
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL st f | A is bounded & g | A is bounded holds
(f (#) g) | A is bounded
let f, g be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded & g | A is bounded implies (f (#) g) | A is bounded )
assume ( f | A is bounded & g | A is bounded ) ; ::_thesis: (f (#) g) | A is bounded
then (f (#) g) | (A /\ A) is bounded by RFUNCT_1:84;
hence (f (#) g) | A is bounded ; ::_thesis: verum
end;
theorem :: INTEGRA6:14
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds
f (#) g is_integrable_on A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds
f (#) g is_integrable_on A
let f, g be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded implies f (#) g is_integrable_on A )
assume that
A1: ( A c= dom f & A c= dom g ) and
A2: ( f is_integrable_on A & f | A is bounded ) and
A3: ( g is_integrable_on A & g | A is bounded ) ; ::_thesis: f (#) g is_integrable_on A
A4: ( f || A is integrable & (f || A) | A is bounded ) by A2, INTEGRA5:def_1;
A5: ( g || A is integrable & (g || A) | A is bounded ) by A3, INTEGRA5:def_1;
A6: (f || A) (#) (g || A) = (f (#) g) || A by INTEGRA5:4;
( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1;
then (f (#) g) || A is integrable by A4, A5, A6, INTEGRA4:29;
hence f (#) g is_integrable_on A by INTEGRA5:def_1; ::_thesis: verum
end;
theorem Th15: :: INTEGRA6:15
for A being non empty closed_interval Subset of REAL
for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
let n be Element of NAT ; ::_thesis: ( n > 0 & vol A > 0 implies ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) ) )
assume that
A1: n > 0 and
A2: vol A > 0 ; ::_thesis: ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
deffunc H1( Nat) -> Element of REAL = (lower_bound A) + (((vol A) / n) * $1);
consider D being FinSequence of REAL such that
A3: ( len D = n & ( for i being Nat st i in dom D holds
D . i = H1(i) ) ) from FINSEQ_2:sch_1();
A4: for i, j being Element of NAT st i in dom D & j in dom D & i < j holds
D . i < D . j
proof
let i, j be Element of NAT ; ::_thesis: ( i in dom D & j in dom D & i < j implies D . i < D . j )
assume that
A5: i in dom D and
A6: j in dom D and
A7: i < j ; ::_thesis: D . i < D . j
(vol A) / n > 0 by A1, A2, XREAL_1:139;
then ((vol A) / n) * i < ((vol A) / n) * j by A7, XREAL_1:68;
then (lower_bound A) + (((vol A) / n) * i) < (lower_bound A) + (((vol A) / n) * j) by XREAL_1:6;
then D . i < (lower_bound A) + (((vol A) / n) * j) by A3, A5;
hence D . i < D . j by A3, A6; ::_thesis: verum
end;
A8: dom D = Seg n by A3, FINSEQ_1:def_3;
reconsider D = D as non empty increasing FinSequence of REAL by A1, A3, A4, SEQM_3:def_1;
D . (len D) = (lower_bound A) + (((vol A) / n) * n) by A3, A8, FINSEQ_1:3;
then A9: D . (len D) = (lower_bound A) + (vol A) by A1, XCMPLX_1:87;
for x1 being set st x1 in rng D holds
x1 in A
proof
let x1 be set ; ::_thesis: ( x1 in rng D implies x1 in A )
assume x1 in rng D ; ::_thesis: x1 in A
then consider i being Element of NAT such that
A10: i in dom D and
A11: D . i = x1 by PARTFUN1:3;
A12: 1 <= i by A10, FINSEQ_3:25;
i <= len D by A10, FINSEQ_3:25;
then ((vol A) / n) * i <= ((vol A) / n) * n by A2, A3, XREAL_1:64;
then ((vol A) / n) * i <= vol A by A1, XCMPLX_1:87;
then A13: (lower_bound A) + (((vol A) / n) * i) <= (lower_bound A) + (vol A) by XREAL_1:6;
(vol A) / n > 0 by A1, A2, XREAL_1:139;
then A14: lower_bound A <= (lower_bound A) + (((vol A) / n) * i) by A12, XREAL_1:29, XREAL_1:129;
x1 = (lower_bound A) + (((vol A) / n) * i) by A3, A10, A11;
hence x1 in A by A14, A13, INTEGRA2:1; ::_thesis: verum
end;
then rng D c= A by TARSKI:def_3;
then reconsider D = D as Division of A by A9, INTEGRA1:def_2;
take D ; ::_thesis: ( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
thus ( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) ) by A3; ::_thesis: verum
end;
begin
theorem Th16: :: INTEGRA6:16
for A being non empty closed_interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: ( vol A > 0 implies ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) )
defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of A st
( n = $1 & e = $2 & e divide_into_equal n + 1 );
assume A1: vol A > 0 ; ::_thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) )
A2: for n being Element of NAT ex D being Element of divs A st S1[n,D]
proof
let n be Element of NAT ; ::_thesis: ex D being Element of divs A st S1[n,D]
consider D being Division of A such that
A3: ( len D = n + 1 & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / (n + 1)) * i) ) ) by A1, Th15;
reconsider D1 = D as Element of divs A by INTEGRA1:def_3;
take D1 ; ::_thesis: S1[n,D1]
D divide_into_equal n + 1 by A3, INTEGRA4:def_1;
hence S1[n,D1] ; ::_thesis: verum
end;
consider T being Function of NAT,(divs A) such that
A4: for n being Element of NAT holds S1[n,T . n] from FUNCT_2:sch_3(A2);
reconsider T = T as DivSequence of A ;
A5: for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn )
proof
let n be Element of NAT ; ::_thesis: ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn )
ex n1 being Element of NAT ex Tn being Division of A st
( n1 = n & Tn = T . n & Tn divide_into_equal n1 + 1 ) by A4;
hence ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ; ::_thesis: verum
end;
A6: for i being Element of NAT holds (delta T) . i = (vol A) / (i + 1)
proof
let i be Element of NAT ; ::_thesis: (delta T) . i = (vol A) / (i + 1)
for x1 being set st x1 in rng (upper_volume ((chi (A,A)),(T . i))) holds
x1 in {((vol A) / (i + 1))}
proof
reconsider D = T . i as Division of A ;
let x1 be set ; ::_thesis: ( x1 in rng (upper_volume ((chi (A,A)),(T . i))) implies x1 in {((vol A) / (i + 1))} )
assume x1 in rng (upper_volume ((chi (A,A)),(T . i))) ; ::_thesis: x1 in {((vol A) / (i + 1))}
then consider k being Element of NAT such that
A7: k in dom (upper_volume ((chi (A,A)),(T . i))) and
A8: (upper_volume ((chi (A,A)),(T . i))) . k = x1 by PARTFUN1:3;
k in Seg (len (upper_volume ((chi (A,A)),(T . i)))) by A7, FINSEQ_1:def_3;
then k in Seg (len D) by INTEGRA1:def_6;
then A9: k in dom D by FINSEQ_1:def_3;
A10: ex n being Element of NAT ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A4;
A11: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
proof
A12: now__::_thesis:_(_k_=_1_implies_(upper_bound_(divset_(D,k)))_-_(lower_bound_(divset_(D,k)))_=_(vol_A)_/_(i_+_1)_)
A13: len D = i + 1 by A10, INTEGRA4:def_1;
assume A14: k = 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
then upper_bound (divset (D,k)) = D . 1 by A9, INTEGRA1:def_4;
then upper_bound (divset (D,k)) = (lower_bound A) + (((vol A) / (i + 1)) * 1) by A10, A9, A14, A13, INTEGRA4:def_1;
then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = ((lower_bound A) + ((vol A) / (i + 1))) - (lower_bound A) by A9, A14, INTEGRA1:def_4;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; ::_thesis: verum
end;
now__::_thesis:_(_k_<>_1_implies_(upper_bound_(divset_(D,k)))_-_(lower_bound_(divset_(D,k)))_=_(vol_A)_/_(i_+_1)_)
assume A15: k <> 1 ; ::_thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
then k - 1 in dom D by A9, INTEGRA1:7;
then A16: D . (k - 1) = (lower_bound A) + (((vol A) / (len D)) * (k - 1)) by A10, INTEGRA4:def_1;
A17: D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A10, A9, INTEGRA4:def_1;
( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by A9, A15, INTEGRA1:def_4;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A10, A16, A17, INTEGRA4:def_1; ::_thesis: verum
end;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A12; ::_thesis: verum
end;
x1 = vol (divset (D,k)) by A8, A9, INTEGRA1:20;
hence x1 in {((vol A) / (i + 1))} by A11, TARSKI:def_1; ::_thesis: verum
end;
then A18: rng (upper_volume ((chi (A,A)),(T . i))) c= {((vol A) / (i + 1))} by TARSKI:def_3;
for x1 being set st x1 in {((vol A) / (i + 1))} holds
x1 in rng (upper_volume ((chi (A,A)),(T . i)))
proof
reconsider D = T . i as Division of A ;
let x1 be set ; ::_thesis: ( x1 in {((vol A) / (i + 1))} implies x1 in rng (upper_volume ((chi (A,A)),(T . i))) )
assume x1 in {((vol A) / (i + 1))} ; ::_thesis: x1 in rng (upper_volume ((chi (A,A)),(T . i)))
then A19: x1 = (vol A) / (i + 1) by TARSKI:def_1;
A20: ex n being Element of NAT ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A4;
rng D <> {} ;
then A21: 1 in dom D by FINSEQ_3:32;
then upper_bound (divset (D,1)) = D . 1 by INTEGRA1:def_4;
then upper_bound (divset (D,1)) = (lower_bound A) + (((vol A) / (len D)) * 1) by A21, A20, INTEGRA4:def_1;
then A22: vol (divset (D,1)) = ((lower_bound A) + ((vol A) / (len D))) - (lower_bound A) by A21, INTEGRA1:def_4;
1 in Seg (len D) by A21, FINSEQ_1:def_3;
then 1 in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3;
then A23: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3;
(upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by A21, INTEGRA1:20;
hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by A19, A23, A20, A22, INTEGRA4:def_1; ::_thesis: verum
end;
then {((vol A) / (i + 1))} c= rng (upper_volume ((chi (A,A)),(T . i))) by TARSKI:def_3;
then ( (delta T) . i = delta (T . i) & rng (upper_volume ((chi (A,A)),(T . i))) = {((vol A) / (i + 1))} ) by A18, INTEGRA3:def_2, XBOOLE_0:def_10;
then (delta T) . i in {((vol A) / (i + 1))} by XXREAL_2:def_8;
hence (delta T) . i = (vol A) / (i + 1) by TARSKI:def_1; ::_thesis: verum
end;
A24: for a being Real st 0 < a holds
ex i being Element of NAT st abs (((delta T) . i) - 0) < a
proof
let a be Real; ::_thesis: ( 0 < a implies ex i being Element of NAT st abs (((delta T) . i) - 0) < a )
A25: vol A >= 0 by INTEGRA1:9;
reconsider i1 = [\((vol A) / a)/] + 1 as Integer ;
assume A26: 0 < a ; ::_thesis: ex i being Element of NAT st abs (((delta T) . i) - 0) < a
then [\((vol A) / a)/] + 1 > 0 by A25, INT_1:29;
then reconsider i1 = i1 as Element of NAT by INT_1:3;
i1 < i1 + 1 by NAT_1:13;
then (vol A) / a < 1 * (i1 + 1) by INT_1:29, XXREAL_0:2;
then A27: (vol A) / (i1 + 1) < 1 * a by A26, XREAL_1:113;
A28: (delta T) . i1 = (vol A) / (i1 + 1) by A6;
((vol A) / (i1 + 1)) - 0 = abs (((vol A) / (i1 + 1)) - 0) by A25, ABSVALUE:def_1;
hence ex i being Element of NAT st abs (((delta T) . i) - 0) < a by A27, A28; ::_thesis: verum
end;
A29: for i, j being Element of NAT st i <= j holds
(delta T) . i >= (delta T) . j
proof
let i, j be Element of NAT ; ::_thesis: ( i <= j implies (delta T) . i >= (delta T) . j )
assume i <= j ; ::_thesis: (delta T) . i >= (delta T) . j
then A30: i + 1 <= j + 1 by XREAL_1:6;
vol A >= 0 by INTEGRA1:9;
then (vol A) / (i + 1) >= (vol A) / (j + 1) by A30, XREAL_1:118;
then (delta T) . i >= (vol A) / (j + 1) by A6;
hence (delta T) . i >= (delta T) . j by A6; ::_thesis: verum
end;
A31: for a being real number st 0 < a holds
ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a
proof
let a be real number ; ::_thesis: ( 0 < a implies ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a )
assume A32: 0 < a ; ::_thesis: ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a
a is Real by XREAL_0:def_1;
then consider i being Element of NAT such that
A33: abs (((delta T) . i) - 0) < a by A24, A32;
(delta T) . i = delta (T . i) by INTEGRA3:def_2;
then (delta T) . i >= 0 by INTEGRA3:9;
then A34: (delta T) . i < a by A33, ABSVALUE:def_1;
now__::_thesis:_for_j_being_Element_of_NAT_st_i_<=_j_holds_
abs_(((delta_T)_._j)_-_0)_<_a
let j be Element of NAT ; ::_thesis: ( i <= j implies abs (((delta T) . j) - 0) < a )
assume i <= j ; ::_thesis: abs (((delta T) . j) - 0) < a
then (delta T) . j <= (delta T) . i by A29;
then A35: (delta T) . j < a by A34, XXREAL_0:2;
(delta T) . j = delta (T . j) by INTEGRA3:def_2;
then (delta T) . j >= 0 by INTEGRA3:9;
hence abs (((delta T) . j) - 0) < a by A35, ABSVALUE:def_1; ::_thesis: verum
end;
hence ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0) < a ; ::_thesis: verum
end;
then A36: delta T is convergent by SEQ_2:def_6;
then lim (delta T) = 0 by A31, SEQ_2:def_7;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) by A5, A36; ::_thesis: verum
end;
Lm2: for a, b, c being real number
for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c holds
( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
proof
let a, b, c be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c holds
( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c implies ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) )
assume that
A1: a <= b and
A2: ['a,b'] c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f | ['a,b'] is bounded and
A5: c in ['a,b'] and
A6: b <> c ; ::_thesis: ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A8: c <= b by A5, XXREAL_1:1;
then A9: ['c,b'] = [.c,b.] by INTEGRA5:def_3;
then A10: [.c,b.] = [.(lower_bound [.c,b.]),(upper_bound [.c,b.]).] by INTEGRA1:4;
then A11: upper_bound ['c,b'] = b by A9, INTEGRA1:5;
set FAB = f || ['a,b'];
set FAC = f || ['a,c'];
set FCB = f || ['c,b'];
A12: f || ['a,b'] is Function of ['a,b'],REAL by A2, Lm1;
A13: a <= c by A5, A7, XXREAL_1:1;
then A14: ['a,c'] = [.a,c.] by INTEGRA5:def_3;
then A15: [.a,c.] = [.(lower_bound [.a,c.]),(upper_bound [.a,c.]).] by INTEGRA1:4;
then A16: lower_bound ['a,c'] = a by A14, INTEGRA1:5;
A17: ['c,b'] c= ['a,b'] by A7, A13, A9, XXREAL_1:34;
then f | ['c,b'] is bounded by A4, RFUNCT_1:74;
then A18: (f || ['c,b']) | ['c,b'] is bounded ;
A19: lower_bound ['c,b'] = c by A9, A10, INTEGRA1:5;
ex PS2 being DivSequence of ['c,b'] st
( delta PS2 is convergent & lim (delta PS2) = 0 & ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = PS2 . i & 2 <= len S2i ) )
proof
c < b by A6, A8, XXREAL_0:1;
then vol ['c,b'] > 0 by A19, A11, XREAL_1:50;
then consider T being DivSequence of ['c,b'] such that
A20: ( delta T is convergent & lim (delta T) = 0 ) and
A21: for n being Element of NAT ex Tn being Division of ['c,b'] st
( Tn divide_into_equal n + 1 & T . n = Tn ) by Th16;
take T ; ::_thesis: ( delta T is convergent & lim (delta T) = 0 & ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = T . i & 2 <= len S2i ) )
now__::_thesis:_for_i_being_Element_of_NAT_st_2_<=_i_holds_
ex_Tn_being_Division_of_['c,b']_st_
(_Tn_=_T_._i_&_2_<=_len_Tn_)
let i be Element of NAT ; ::_thesis: ( 2 <= i implies ex Tn being Division of ['c,b'] st
( Tn = T . i & 2 <= len Tn ) )
assume A22: 2 <= i ; ::_thesis: ex Tn being Division of ['c,b'] st
( Tn = T . i & 2 <= len Tn )
consider Tn being Division of ['c,b'] such that
A23: Tn divide_into_equal i + 1 and
A24: T . i = Tn by A21;
reconsider Tn = Tn as Division of ['c,b'] ;
take Tn = Tn; ::_thesis: ( Tn = T . i & 2 <= len Tn )
thus Tn = T . i by A24; ::_thesis: 2 <= len Tn
len Tn = i + 1 by A23, INTEGRA4:def_1;
then i <= len Tn by NAT_1:11;
hence 2 <= len Tn by A22, XXREAL_0:2; ::_thesis: verum
end;
hence ( delta T is convergent & lim (delta T) = 0 & ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = T . i & 2 <= len S2i ) ) by A20; ::_thesis: verum
end;
then consider PS2 being DivSequence of ['c,b'] such that
A25: ( delta PS2 is convergent & lim (delta PS2) = 0 ) and
A26: ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = PS2 . i & 2 <= len S2i ) ;
consider K being Element of NAT such that
A27: for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = PS2 . i & 2 <= len S2i ) by A26;
defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of ['c,b'] st
( n = $1 & e = $2 & e = PS2 . (n + K) );
A28: for n being Element of NAT ex D being Element of divs ['c,b'] st S1[n,D]
proof
let n be Element of NAT ; ::_thesis: ex D being Element of divs ['c,b'] st S1[n,D]
reconsider D = PS2 . (n + K) as Element of divs ['c,b'] by INTEGRA1:def_3;
take D ; ::_thesis: S1[n,D]
thus S1[n,D] ; ::_thesis: verum
end;
consider S2 being Function of NAT,(divs ['c,b']) such that
A29: for n being Element of NAT holds S1[n,S2 . n] from FUNCT_2:sch_3(A28);
reconsider S2 = S2 as DivSequence of ['c,b'] ;
defpred S2[ Element of NAT , set ] means ex S being Division of ['c,b'] st
( S = S2 . $1 & $2 = S /^ 1 );
A30: now__::_thesis:_for_i_being_Element_of_NAT_ex_S2i_being_Division_of_['c,b']_st_
(_S2i_=_S2_._i_&_2_<=_len_S2i_)
let i be Element of NAT ; ::_thesis: ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i )
ex n being Element of NAT ex e being Division of ['c,b'] st
( n = i & e = S2 . i & e = PS2 . (n + K) ) by A29;
hence ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i ) by A27, NAT_1:11; ::_thesis: verum
end;
A31: for i being Element of NAT ex T being Element of divs ['c,b'] st S2[i,T]
proof
let i be Element of NAT ; ::_thesis: ex T being Element of divs ['c,b'] st S2[i,T]
consider S being Division of ['c,b'] such that
A32: S = S2 . i and
A33: 2 <= len S by A30;
set T = S /^ 1;
A34: 1 <= len S by A33, XXREAL_0:2;
2 - 1 <= (len S) - 1 by A33, XREAL_1:13;
then A35: 1 <= len (S /^ 1) by A34, RFINSEQ:def_1;
then len (S /^ 1) in Seg (len (S /^ 1)) ;
then len (S /^ 1) in dom (S /^ 1) by FINSEQ_1:def_3;
then (S /^ 1) . (len (S /^ 1)) = S . ((len (S /^ 1)) + 1) by A34, RFINSEQ:def_1;
then (S /^ 1) . (len (S /^ 1)) = S . (((len S) - 1) + 1) by A34, RFINSEQ:def_1;
then A36: (S /^ 1) . (len (S /^ 1)) = upper_bound ['c,b'] by INTEGRA1:def_2;
( rng S c= ['c,b'] & rng (S /^ 1) c= rng S ) by FINSEQ_5:33, INTEGRA1:def_2;
then A37: rng (S /^ 1) c= ['c,b'] by XBOOLE_1:1;
( not S /^ 1 is empty & S /^ 1 is increasing ) by A33, A35, INTEGRA1:34, XXREAL_0:2;
then S /^ 1 is Division of ['c,b'] by A37, A36, INTEGRA1:def_2;
then S /^ 1 is Element of divs ['c,b'] by INTEGRA1:def_3;
hence ex T being Element of divs ['c,b'] st S2[i,T] by A32; ::_thesis: verum
end;
consider T2 being DivSequence of ['c,b'] such that
A38: for i being Element of NAT holds S2[i,T2 . i] from FUNCT_2:sch_3(A31);
A39: for n being Element of NAT ex D being Division of ['c,b'] st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )
proof
let n be Element of NAT ; ::_thesis: ex D being Division of ['c,b'] st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )
reconsider D = T2 . n as Division of ['c,b'] ;
take D ; ::_thesis: ( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )
consider E being Division of ['c,b'] such that
A40: E = S2 . n and
A41: T2 . n = E /^ 1 by A38;
A42: ex E1 being Division of ['c,b'] st
( E1 = S2 . n & 2 <= len E1 ) by A30;
then A43: 2 - 1 <= (len E) - 1 by A40, XREAL_1:13;
A44: 1 <= len E by A40, A42, XXREAL_0:2;
then 1 in Seg (len E) ;
then A45: 1 in dom E by FINSEQ_1:def_3;
then ( rng E c= ['c,b'] & E . 1 in rng E ) by FUNCT_1:def_3, INTEGRA1:def_2;
then A46: c <= E . 1 by A9, XXREAL_1:1;
2 in Seg (len E) by A40, A42;
then 2 in dom E by FINSEQ_1:def_3;
then A47: E . 1 < E . 2 by A45, SEQM_3:def_1;
len D = (len E) - 1 by A41, A44, RFINSEQ:def_1;
then 1 in Seg (len D) by A43;
then A48: 1 in dom D by FINSEQ_1:def_3;
then A49: D . 1 = E . (1 + 1) by A41, A44, RFINSEQ:def_1;
then A50: c < D . 1 by A46, A47, XXREAL_0:2;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_D_holds_
(_(_i_<>_1_implies_c_<_D_._i_)_&_c_<_D_._i_)
let i be Element of NAT ; ::_thesis: ( i in dom D implies ( ( i <> 1 implies c < D . i ) & c < D . i ) )
assume A51: i in dom D ; ::_thesis: ( ( i <> 1 implies c < D . i ) & c < D . i )
then A52: 1 <= i by FINSEQ_3:25;
hereby ::_thesis: c < D . i
assume i <> 1 ; ::_thesis: c < D . i
then 1 < i by A52, XXREAL_0:1;
then D . 1 < D . i by A48, A51, SEQM_3:def_1;
hence c < D . i by A50, XXREAL_0:2; ::_thesis: verum
end;
hence c < D . i by A49, A46, A47, XXREAL_0:2; ::_thesis: verum
end;
hence ( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) ) ; ::_thesis: verum
end;
set XAC = chi (['a,c'],['a,c']);
set XCB = chi (['c,b'],['c,b']);
consider T1 being DivSequence of ['a,c'] such that
A53: ( delta T1 is convergent & lim (delta T1) = 0 ) by INTEGRA4:11;
A54: for n being Element of NAT ex D being Division of ['c,b'] st
( D = T2 . n & 1 <= len D )
proof
let n be Element of NAT ; ::_thesis: ex D being Division of ['c,b'] st
( D = T2 . n & 1 <= len D )
reconsider D = T2 . n as Division of ['c,b'] ;
take D ; ::_thesis: ( D = T2 . n & 1 <= len D )
consider E being Division of ['c,b'] such that
A55: E = S2 . n and
A56: T2 . n = E /^ 1 by A38;
ex E1 being Division of ['c,b'] st
( E1 = S2 . n & 2 <= len E1 ) by A30;
then ( 1 <= len E & 2 - 1 <= (len E) - 1 ) by A55, XREAL_1:13, XXREAL_0:2;
hence ( D = T2 . n & 1 <= len D ) by A56, RFINSEQ:def_1; ::_thesis: verum
end;
A57: integral (f,c,b) = integral (f,['c,b']) by A8, INTEGRA5:def_4
.= integral (f || ['c,b']) ;
A58: integral (f,a,c) = integral (f,['a,c']) by A13, INTEGRA5:def_4;
defpred S3[ Element of NAT , set ] means ex S1 being Division of ['a,c'] ex S2 being Division of ['c,b'] st
( S1 = T1 . $1 & S2 = T2 . $1 & $2 = S1 ^ S2 );
A59: [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] by A7, INTEGRA1:4;
then A60: upper_bound ['a,b'] = b by A7, INTEGRA1:5;
A61: for i being Element of NAT ex T being Element of divs ['a,b'] st S3[i,T]
proof
let i0 be Element of NAT ; ::_thesis: ex T being Element of divs ['a,b'] st S3[i0,T]
reconsider S1 = T1 . i0 as Division of ['a,c'] ;
reconsider S2 = T2 . i0 as Division of ['c,b'] ;
set T = S1 ^ S2;
ex D being Division of ['c,b'] st
( D = T2 . i0 & 1 <= len D ) by A54;
then len S2 in Seg (len S2) ;
then A62: len S2 in dom S2 by FINSEQ_1:def_3;
A63: rng S1 c= ['a,c'] by INTEGRA1:def_2;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(S1_^_S2)_&_j_in_dom_(S1_^_S2)_&_i_<_j_holds_
(S1_^_S2)_._i_<_(S1_^_S2)_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j implies (S1 ^ S2) . i < (S1 ^ S2) . j )
assume that
A64: i in dom (S1 ^ S2) and
A65: j in dom (S1 ^ S2) and
A66: i < j ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
A67: 1 <= i by A64, FINSEQ_3:25;
A68: j <= len (S1 ^ S2) by A65, FINSEQ_3:25;
A69: i <= len (S1 ^ S2) by A64, FINSEQ_3:25;
A70: now__::_thesis:_(_j_>_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_)
j <= (len S1) + (len S2) by A68, FINSEQ_1:22;
then A71: j - (len S1) <= len S2 by XREAL_1:20;
assume A72: j > len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A73: (S1 ^ S2) . j = S2 . (j - (len S1)) by A68, FINSEQ_1:24;
A74: (len S1) + 1 <= j by A72, NAT_1:13;
then consider m being Nat such that
A75: ((len S1) + 1) + m = j by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
1 + m = j - (len S1) by A75;
then 1 <= 1 + m by A74, XREAL_1:19;
then 1 + m in Seg (len S2) by A75, A71;
then A76: j - (len S1) in dom S2 by A75, FINSEQ_1:def_3;
A77: now__::_thesis:_(_i_>_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_)
i <= (len S1) + (len S2) by A69, FINSEQ_1:22;
then A78: i - (len S1) <= len S2 by XREAL_1:20;
A79: i - (len S1) < j - (len S1) by A66, XREAL_1:14;
assume A80: i > len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A81: (len S1) + 1 <= i by NAT_1:13;
then consider m being Nat such that
A82: ((len S1) + 1) + m = i by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
1 + m = i - (len S1) by A82;
then 1 <= 1 + m by A81, XREAL_1:19;
then 1 + m in Seg (len S2) by A82, A78;
then A83: i - (len S1) in dom S2 by A82, FINSEQ_1:def_3;
(S1 ^ S2) . i = S2 . (i - (len S1)) by A69, A80, FINSEQ_1:24;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A79, A83, SEQM_3:def_1; ::_thesis: verum
end;
now__::_thesis:_(_i_<=_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_)
assume i <= len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A84: i in dom S1 by A67, FINSEQ_3:25;
then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def_7;
then (S1 ^ S2) . i in rng S1 by A84, FUNCT_1:def_3;
then A85: (S1 ^ S2) . i <= c by A14, A63, XXREAL_1:1;
ex DD being Division of ['c,b'] st
( DD = T2 . i0 & ( for k being Element of NAT st k in dom DD holds
c < DD . k ) ) by A39;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A73, A76, A85, XXREAL_0:2; ::_thesis: verum
end;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A77; ::_thesis: verum
end;
A86: 1 <= j by A65, FINSEQ_3:25;
now__::_thesis:_(_j_<=_len_S1_implies_(S1_^_S2)_._i_<_(S1_^_S2)_._j_)
assume A87: j <= len S1 ; ::_thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A88: j in dom S1 by A86, FINSEQ_3:25;
then A89: (S1 ^ S2) . j = S1 . j by FINSEQ_1:def_7;
i <= len S1 by A66, A87, XXREAL_0:2;
then A90: i in dom S1 by A67, FINSEQ_3:25;
then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def_7;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A66, A90, A88, A89, SEQM_3:def_1; ::_thesis: verum
end;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A70; ::_thesis: verum
end;
then A91: S1 ^ S2 is non empty increasing FinSequence of REAL by SEQM_3:def_1;
rng S2 c= ['c,b'] by INTEGRA1:def_2;
then (rng S1) \/ (rng S2) c= ['a,c'] \/ ['c,b'] by A63, XBOOLE_1:13;
then (rng S1) \/ (rng S2) c= [.a,b.] by A13, A8, A14, A9, XXREAL_1:174;
then A92: rng (S1 ^ S2) c= ['a,b'] by A7, FINSEQ_1:31;
(S1 ^ S2) . (len (S1 ^ S2)) = (S1 ^ S2) . ((len S1) + (len S2)) by FINSEQ_1:22
.= S2 . (len S2) by A62, FINSEQ_1:def_7
.= upper_bound ['a,b'] by A60, A11, INTEGRA1:def_2 ;
then S1 ^ S2 is Division of ['a,b'] by A92, A91, INTEGRA1:def_2;
then S1 ^ S2 is Element of divs ['a,b'] by INTEGRA1:def_3;
hence ex T being Element of divs ['a,b'] st S3[i0,T] ; ::_thesis: verum
end;
consider T being DivSequence of ['a,b'] such that
A93: for i being Element of NAT holds S3[i,T . i] from FUNCT_2:sch_3(A61);
A94: lower_bound ['a,b'] = a by A7, A59, INTEGRA1:5;
A95: for i, k being Element of NAT
for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T . i),k) = divset ((T1 . i),k)
proof
let i, k be Element of NAT ; ::_thesis: for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T . i),k) = divset ((T1 . i),k)
let S0 be Division of ['a,c']; ::_thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) )
assume A96: S0 = T1 . i ; ::_thesis: ( not k in Seg (len S0) or divset ((T . i),k) = divset ((T1 . i),k) )
reconsider S = T . i as Division of ['a,b'] ;
A97: divset ((T1 . i),k) = [.(lower_bound (divset ((T1 . i),k))),(upper_bound (divset ((T1 . i),k))).] by INTEGRA1:4;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A98: S1 = T1 . i and
S2 = T2 . i and
A99: T . i = S1 ^ S2 by A93;
assume A100: k in Seg (len S0) ; ::_thesis: divset ((T . i),k) = divset ((T1 . i),k)
then A101: k in dom S1 by A96, A98, FINSEQ_1:def_3;
len S = (len S1) + (len S2) by A99, FINSEQ_1:22;
then len S1 <= len S by NAT_1:11;
then Seg (len S1) c= Seg (len S) by FINSEQ_1:5;
then k in Seg (len S) by A96, A100, A98;
then A102: k in dom S by FINSEQ_1:def_3;
A103: divset ((T . i),k) = [.(lower_bound (divset ((T . i),k))),(upper_bound (divset ((T . i),k))).] by INTEGRA1:4;
A104: now__::_thesis:_(_k_<>_1_implies_divset_((T_._i),k)_=_divset_((T1_._i),k)_)
( k <= len S1 & k - 1 <= k - 0 ) by A96, A100, A98, FINSEQ_1:1, XREAL_1:10;
then A105: k - 1 <= len S1 by XXREAL_0:2;
assume A106: k <> 1 ; ::_thesis: divset ((T . i),k) = divset ((T1 . i),k)
1 <= k by A100, FINSEQ_1:1;
then A107: 1 < k by A106, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A108: 2 - 1 <= k - 1 by XREAL_1:9;
k - 1 is Element of NAT by A107, NAT_1:20;
then k - 1 in Seg (len S1) by A105, A108;
then A109: k - 1 in dom S1 by FINSEQ_1:def_3;
thus divset ((T . i),k) = [.(S . (k - 1)),(upper_bound (divset ((T . i),k))).] by A102, A103, A106, INTEGRA1:def_4
.= [.(S . (k - 1)),(S . k).] by A102, A106, INTEGRA1:def_4
.= [.(S . (k - 1)),(S1 . k).] by A99, A101, FINSEQ_1:def_7
.= [.(S1 . (k - 1)),(S1 . k).] by A99, A109, FINSEQ_1:def_7
.= [.(lower_bound (divset ((T1 . i),k))),(S1 . k).] by A98, A101, A106, INTEGRA1:def_4
.= divset ((T1 . i),k) by A98, A101, A97, A106, INTEGRA1:def_4 ; ::_thesis: verum
end;
now__::_thesis:_(_k_=_1_implies_divset_((T_._i),k)_=_divset_((T1_._i),k)_)
assume A110: k = 1 ; ::_thesis: divset ((T . i),k) = divset ((T1 . i),k)
hence divset ((T . i),k) = [.(lower_bound ['a,b']),(upper_bound (divset ((T . i),k))).] by A102, A103, INTEGRA1:def_4
.= [.(lower_bound ['a,b']),(S . k).] by A102, A110, INTEGRA1:def_4
.= [.(lower_bound ['a,b']),(S1 . k).] by A99, A101, FINSEQ_1:def_7
.= [.(lower_bound (divset ((T1 . i),k))),(S1 . 1).] by A94, A16, A98, A101, A110, INTEGRA1:def_4
.= divset ((T1 . i),k) by A98, A101, A97, A110, INTEGRA1:def_4 ;
::_thesis: verum
end;
hence divset ((T . i),k) = divset ((T1 . i),k) by A104; ::_thesis: verum
end;
A111: upper_bound ['a,c'] = c by A14, A15, INTEGRA1:5;
A112: for i, k being Element of NAT
for S01 being Division of ['a,c']
for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
proof
let i, k be Element of NAT ; ::_thesis: for S01 being Division of ['a,c']
for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
let S01 be Division of ['a,c']; ::_thesis: for S02 being Division of ['c,b'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
let S02 be Division of ['c,b']; ::_thesis: ( S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) implies divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )
assume that
A113: S01 = T1 . i and
A114: S02 = T2 . i ; ::_thesis: ( not k in Seg (len S02) or divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )
reconsider S = T . i as Division of ['a,b'] ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A115: S1 = T1 . i and
A116: S2 = T2 . i and
A117: T . i = S1 ^ S2 by A93;
assume A118: k in Seg (len S02) ; ::_thesis: divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
then A119: k in dom S2 by A114, A116, FINSEQ_1:def_3;
then A120: (len S1) + k in dom S by A117, FINSEQ_1:28;
A121: divset ((T2 . i),k) = [.(lower_bound (divset ((T2 . i),k))),(upper_bound (divset ((T2 . i),k))).] by INTEGRA1:4;
A122: divset ((T . i),((len S1) + k)) = [.(lower_bound (divset ((T . i),((len S1) + k)))),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:4;
A123: now__::_thesis:_(_k_<>_1_implies_divset_((T_._i),((len_S1)_+_k))_=_divset_((T2_._i),k)_)
( k <= len S2 & k - 1 <= k - 0 ) by A114, A118, A116, FINSEQ_1:1, XREAL_1:10;
then A124: k - 1 <= len S2 by XXREAL_0:2;
assume A125: k <> 1 ; ::_thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)
A126: 1 <= k by A118, FINSEQ_1:1;
then A127: 1 < k by A125, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A128: 2 - 1 <= k - 1 by XREAL_1:9;
k - 1 is Element of NAT by A127, NAT_1:20;
then k - 1 in Seg (len S2) by A124, A128;
then A129: k - 1 in dom S2 by FINSEQ_1:def_3;
A130: 1 + 0 < k + (len S1) by A126, XREAL_1:8;
hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A120, A122, INTEGRA1:def_4
.= [.(S . (((len S1) + k) - 1)),(S . ((len S1) + k)).] by A120, A130, INTEGRA1:def_4
.= [.(S . ((len S1) + (k - 1))),(S2 . k).] by A117, A119, FINSEQ_1:def_7
.= [.(S2 . (k - 1)),(S2 . k).] by A117, A129, FINSEQ_1:def_7
.= [.(lower_bound (divset ((T2 . i),k))),(S2 . k).] by A116, A119, A125, INTEGRA1:def_4
.= divset ((T2 . i),k) by A116, A119, A121, A125, INTEGRA1:def_4 ;
::_thesis: verum
end;
now__::_thesis:_(_k_=_1_implies_divset_((T_._i),((len_S1)_+_k))_=_divset_((T2_._i),k)_)
len S1 in Seg (len S1) by FINSEQ_1:3;
then A131: len S1 in dom S1 by FINSEQ_1:def_3;
assume A132: k = 1 ; ::_thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)
len S1 <> 0 ;
then A133: (len S1) + k <> 1 by A132;
hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A120, A122, INTEGRA1:def_4
.= [.(S1 . (len S1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A117, A132, A131, FINSEQ_1:def_7
.= [.(upper_bound ['a,c']),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:def_2
.= [.(lower_bound ['c,b']),(S . ((len S1) + k)).] by A19, A111, A120, A133, INTEGRA1:def_4
.= [.(lower_bound ['c,b']),(S2 . k).] by A117, A119, FINSEQ_1:def_7
.= [.(lower_bound (divset ((T2 . i),k))),(S2 . 1).] by A116, A119, A132, INTEGRA1:def_4
.= divset ((T2 . i),k) by A116, A119, A121, A132, INTEGRA1:def_4 ;
::_thesis: verum
end;
hence divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) by A113, A115, A123; ::_thesis: verum
end;
set XAB = chi (['a,b'],['a,b']);
A134: for i, k being Element of NAT
for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds
divset ((T2 . i),k) c= ['c,b']
proof
let i, k be Element of NAT ; ::_thesis: for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds
divset ((T2 . i),k) c= ['c,b']
let S0 be Division of ['c,b']; ::_thesis: ( S0 = T2 . i & k in Seg (len S0) implies divset ((T2 . i),k) c= ['c,b'] )
assume that
A135: S0 = T2 . i and
A136: k in Seg (len S0) ; ::_thesis: divset ((T2 . i),k) c= ['c,b']
k in dom S0 by A136, FINSEQ_1:def_3;
hence divset ((T2 . i),k) c= ['c,b'] by A135, INTEGRA1:8; ::_thesis: verum
end;
A137: ['a,c'] c= ['a,b'] by A7, A8, A14, XXREAL_1:34;
then f | ['a,c'] is bounded by A4, RFUNCT_1:74;
then A138: (f || ['a,c']) | ['a,c'] is bounded ;
A139: for i, k being Element of NAT
for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T1 . i),k) c= ['a,c']
proof
let i, k be Element of NAT ; ::_thesis: for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T1 . i),k) c= ['a,c']
let S0 be Division of ['a,c']; ::_thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T1 . i),k) c= ['a,c'] )
assume that
A140: S0 = T1 . i and
A141: k in Seg (len S0) ; ::_thesis: divset ((T1 . i),k) c= ['a,c']
k in dom S0 by A141, FINSEQ_1:def_3;
hence divset ((T1 . i),k) c= ['a,c'] by A140, INTEGRA1:8; ::_thesis: verum
end;
A142: for i being Element of NAT holds upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i)))
proof
let i be Element of NAT ; ::_thesis: upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i)))
reconsider F = upper_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;
reconsider F1 = upper_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;
reconsider F2 = upper_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;
reconsider S = T . i as Division of ['a,b'] ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A143: S1 = T1 . i and
A144: S2 = T2 . i and
A145: T . i = S1 ^ S2 by A93;
A146: len F = len S by INTEGRA1:def_6
.= (len S1) + (len S2) by A145, FINSEQ_1:22
.= (len F1) + (len S2) by A143, INTEGRA1:def_6
.= (len F1) + (len F2) by A144, INTEGRA1:def_6 ;
A147: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F2_holds_
F_._((len_F1)_+_k)_=_F2_._k
let k be Nat; ::_thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )
assume A148: k in dom F2 ; ::_thesis: F . ((len F1) + k) = F2 . k
then A149: k in Seg (len F2) by FINSEQ_1:def_3;
then 1 <= k by FINSEQ_1:1;
then A150: 1 + (len F1) <= k + (len F1) by XREAL_1:6;
k <= len F2 by A149, FINSEQ_1:1;
then A151: (len F1) + k <= len F by A146, XREAL_1:6;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by A150, XXREAL_0:2;
then k + (len F1) in Seg (len F) by A151;
then (len F1) + k in Seg (len S) by INTEGRA1:def_6;
then (len F1) + k in dom S by FINSEQ_1:def_3;
then A152: F . ((len F1) + k) = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def_6;
k in Seg (len F2) by A148, FINSEQ_1:def_3;
then A153: k in Seg (len S2) by A144, INTEGRA1:def_6;
then A154: k in dom S2 by FINSEQ_1:def_3;
len F1 = len S1 by A143, INTEGRA1:def_6;
then A155: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A143, A144, A153;
then A156: divset ((T . i),((len F1) + k)) c= ['c,b'] by A134, A144, A153;
then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17, XBOOLE_1:1;
then F . ((len F1) + k) = (upper_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A152, A155, A156, Th3;
hence F . ((len F1) + k) = F2 . k by A144, A154, INTEGRA1:def_6; ::_thesis: verum
end;
A157: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_
F_._k_=_F1_._k
let k be Nat; ::_thesis: ( k in dom F1 implies F . k = F1 . k )
assume k in dom F1 ; ::_thesis: F . k = F1 . k
then A158: k in Seg (len F1) by FINSEQ_1:def_3;
then A159: k in Seg (len S1) by A143, INTEGRA1:def_6;
then A160: k in dom S1 by FINSEQ_1:def_3;
len F1 <= len F by A146, NAT_1:11;
then Seg (len F1) c= Seg (len F) by FINSEQ_1:5;
then k in Seg (len F) by A158;
then k in Seg (len S) by INTEGRA1:def_6;
then k in dom S by FINSEQ_1:def_3;
then A161: F . k = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by INTEGRA1:def_6;
A162: divset ((T . i),k) = divset ((T1 . i),k) by A95, A143, A159;
then A163: divset ((T . i),k) c= ['a,c'] by A139, A143, A159;
then divset ((T . i),k) c= ['a,b'] by A137, XBOOLE_1:1;
then F . k = (upper_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A161, A162, A163, Th3;
hence F . k = F1 . k by A143, A160, INTEGRA1:def_6; ::_thesis: verum
end;
dom F = Seg ((len F1) + (len F2)) by A146, FINSEQ_1:def_3;
hence upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A157, A147, FINSEQ_1:def_7; ::_thesis: verum
end;
A164: for i being Element of NAT holds Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i))))
proof
let i be Element of NAT ; ::_thesis: Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i))))
upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A142;
hence Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_holds_(upper_sum_((f_||_['a,b']),T))_._i_=_((upper_sum_((f_||_['a,c']),T1))_._i)_+_((upper_sum_((f_||_['c,b']),T2))_._i)
let i be Element of NAT ; ::_thesis: (upper_sum ((f || ['a,b']),T)) . i = ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i)
thus (upper_sum ((f || ['a,b']),T)) . i = upper_sum ((f || ['a,b']),(T . i)) by INTEGRA2:def_2
.= (upper_sum ((f || ['a,c']),(T1 . i))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) by A164
.= ((upper_sum ((f || ['a,c']),T1)) . i) + (upper_sum ((f || ['c,b']),(T2 . i))) by INTEGRA2:def_2
.= ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def_2 ; ::_thesis: verum
end;
then A165: upper_sum ((f || ['a,b']),T) = (upper_sum ((f || ['a,c']),T1)) + (upper_sum ((f || ['c,b']),T2)) by SEQ_1:7;
A166: f || ['c,b'] is Function of ['c,b'],REAL by A2, A17, Lm1, XBOOLE_1:1;
then A167: lower_integral (f || ['c,b']) <= upper_integral (f || ['c,b']) by A18, INTEGRA1:49;
A168: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_(((delta_S2)_._n)_-_0)_<_e
let e be real number ; ::_thesis: ( 0 < e implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((delta S2) . n) - 0) < e )
assume 0 < e ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((delta S2) . n) - 0) < e
then consider m being Element of NAT such that
A169: for n being Element of NAT st m <= n holds
abs (((delta PS2) . n) - 0) < e by A25, SEQ_2:def_7;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
abs (((delta S2) . n) - 0) < e
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( m <= n implies abs (((delta S2) . n) - 0) < e )
A170: n <= n + K by NAT_1:11;
assume m <= n ; ::_thesis: abs (((delta S2) . n) - 0) < e
then m <= n + K by A170, XXREAL_0:2;
then abs (((delta PS2) . (n + K)) - 0) < e by A169;
then A171: abs ((delta (PS2 . (n + K))) - 0) < e by INTEGRA3:def_2;
ex k being Element of NAT ex e1 being Division of ['c,b'] st
( k = n & e1 = S2 . n & e1 = PS2 . (k + K) ) by A29;
hence abs (((delta S2) . n) - 0) < e by A171, INTEGRA3:def_2; ::_thesis: verum
end;
end;
A172: now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_(((delta_T2)_._n)_-_0)_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((delta T2) . n) - 0) < e )
assume A173: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((delta T2) . n) - 0) < e
then consider m being Element of NAT such that
A174: for n being Element of NAT st m <= n holds
abs (((delta S2) . n) - 0) < e / 2 by A168, XREAL_1:215;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
abs (((delta T2) . n) - 0) < e
A175: e / 2 < e by A173, XREAL_1:216;
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_(((delta_T2)_._n)_-_0)_<_e
let n be Element of NAT ; ::_thesis: ( m <= n implies abs (((delta T2) . n) - 0) < e )
assume m <= n ; ::_thesis: abs (((delta T2) . n) - 0) < e
then abs (((delta S2) . n) - 0) < e / 2 by A174;
then ( 0 <= delta (S2 . n) & abs (delta (S2 . n)) < e / 2 ) by INTEGRA3:9, INTEGRA3:def_2;
then A176: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) < e / 2 by ABSVALUE:def_1;
A177: for y being real number st y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) holds
y < e
proof
reconsider D = T2 . n as Division of ['c,b'] ;
let y be real number ; ::_thesis: ( y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) implies y < e )
assume y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) ; ::_thesis: y < e
then consider x being set such that
A178: x in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) and
A179: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A178;
A180: x in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) by A178, FINSEQ_1:def_3;
consider E1 being Division of ['c,b'] such that
A181: E1 = S2 . n and
A182: 2 <= len E1 by A30;
set i1 = i + 1;
consider E being Division of ['c,b'] such that
A183: E = S2 . n and
A184: T2 . n = E /^ 1 by A38;
A185: 1 <= len E1 by A182, XXREAL_0:2;
then A186: len D = (len E) - 1 by A183, A184, A181, RFINSEQ:def_1;
A187: len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = len D by INTEGRA1:def_6;
then A188: dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = dom D by FINSEQ_3:29;
A189: now__::_thesis:_(_i_=_1_implies_y_<_e_)
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by A183, INTEGRA1:def_6;
then 2 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A183, A181, A182;
then 2 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def_3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def_3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def_8;
then A190: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 < e / 2 by A176, XXREAL_0:2;
assume A191: i = 1 ; ::_thesis: y < e
then A192: 1 in dom D by A180, A187, FINSEQ_1:def_3;
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by A183, A186, INTEGRA1:def_6;
then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def_6;
then 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A180, A191, FINSEQ_2:8;
then 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def_3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def_3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def_8;
then A193: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 < e / 2 by A176, XXREAL_0:2;
A194: 2 in dom E by A183, A181, A182, FINSEQ_3:25;
1 in Seg (len E) by A183, A181, A185;
then A195: 1 in dom E by FINSEQ_1:def_3;
divset ((S2 . n),1) = [.(lower_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),1))).] by INTEGRA1:4;
then A196: divset ((S2 . n),1) = [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] by A183, A195, INTEGRA1:def_4;
then A197: [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]).] by INTEGRA1:4;
A198: divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),1))),(upper_bound (divset ((T2 . n),1))).] by A191, INTEGRA1:4
.= [.(lower_bound ['c,b']),(upper_bound (divset ((T2 . n),1))).] by A192, INTEGRA1:def_4
.= [.(lower_bound ['c,b']),(D . 1).] by A192, INTEGRA1:def_4
.= [.(lower_bound ['c,b']),(E . (1 + 1)).] by A183, A184, A181, A185, A192, RFINSEQ:def_1
.= [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] by A183, A194, INTEGRA1:def_4 ;
then [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;
then A199: ( lower_bound ['c,b'] = lower_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] & upper_bound (divset ((S2 . n),2)) = upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).] ) by A198, INTEGRA1:5;
y = vol (divset ((T2 . n),1)) by A178, A179, A188, A191, INTEGRA1:20;
then y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + ((upper_bound [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]) - (lower_bound ['c,b'])) by A191, A198, A199, A196;
then A200: y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + (vol (divset ((S2 . n),1))) by A196, A197, INTEGRA1:5;
divset ((S2 . n),2) = [.(lower_bound (divset ((S2 . n),2))),(upper_bound (divset ((S2 . n),2))).] by INTEGRA1:4;
then divset ((S2 . n),2) = [.(E . (2 - 1)),(upper_bound (divset ((S2 . n),2))).] by A183, A194, INTEGRA1:def_4;
then A201: divset ((S2 . n),2) = [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] by A183, A195, INTEGRA1:def_4;
then [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;
then y = (vol (divset ((S2 . n),2))) + (vol (divset ((S2 . n),1))) by A201, A200, INTEGRA1:5;
then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + (vol (divset ((S2 . n),1))) by A183, A194, INTEGRA1:20;
then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1) by A183, A195, INTEGRA1:20;
then y < (e / 2) + (e / 2) by A190, A193, XREAL_1:8;
hence y < e ; ::_thesis: verum
end;
A202: y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . n),i))))) * (vol (divset ((T2 . n),i))) by A178, A179, A188, INTEGRA1:def_6;
now__::_thesis:_(_i_<>_1_implies_y_<_e_)
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by A183, A186, INTEGRA1:def_6;
then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def_6;
then A203: i + 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by A180, FINSEQ_1:60;
then A204: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def_3;
A205: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A203, FINSEQ_1:def_3;
A206: i in dom D by A180, A187, FINSEQ_1:def_3;
Seg ((len D) + 1) = Seg (len E) by A186;
then i + 1 in Seg (len E) by A180, A187, FINSEQ_1:60;
then A207: i + 1 in dom E by FINSEQ_1:def_3;
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by A183, INTEGRA1:def_6;
then A208: dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = dom E by FINSEQ_3:29;
assume A209: i <> 1 ; ::_thesis: y < e
i in Seg (len D) by A178, A187, FINSEQ_1:def_3;
then 1 <= i by FINSEQ_1:1;
then A210: 1 < i by A209, XXREAL_0:1;
then A211: i - 1 in Seg (len D) by A180, A187, FINSEQ_3:12;
then A212: i - 1 in dom D by FINSEQ_1:def_3;
reconsider i9 = i - 1 as Element of NAT by A211;
1 + 1 < i + 1 by A210, XREAL_1:8;
then A213: i + 1 <> 1 ;
divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),i))),(upper_bound (divset ((T2 . n),i))).] by INTEGRA1:4
.= [.(D . (i - 1)),(upper_bound (divset ((T2 . n),i))).] by A209, A206, INTEGRA1:def_4
.= [.(D . (i - 1)),(D . i).] by A209, A206, INTEGRA1:def_4
.= [.(E . (i9 + 1)),(D . i).] by A183, A184, A181, A185, A212, RFINSEQ:def_1
.= [.(E . ((i - 1) + 1)),(E . (i + 1)).] by A183, A184, A181, A185, A206, RFINSEQ:def_1
.= [.(E . ((i + 1) - 1)),(upper_bound (divset ((S2 . n),(i + 1)))).] by A183, A213, A207, INTEGRA1:def_4
.= [.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).] by A183, A213, A207, INTEGRA1:def_4
.= divset ((S2 . n),(i + 1)) by INTEGRA1:4 ;
then y = (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . (i + 1) by A202, A183, A204, A208, INTEGRA1:def_6;
then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by A205, FUNCT_1:def_3;
then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def_8;
then y < e / 2 by A176, XXREAL_0:2;
hence y < e by A175, XXREAL_0:2; ::_thesis: verum
end;
hence y < e by A189; ::_thesis: verum
end;
max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) by XXREAL_2:def_8;
then ( 0 <= delta (T2 . n) & delta (T2 . n) < e ) by A177, INTEGRA3:9;
then abs (delta (T2 . n)) < e by ABSVALUE:def_1;
hence abs (((delta T2) . n) - 0) < e by INTEGRA3:def_2; ::_thesis: verum
end;
hence for n being Element of NAT st m <= n holds
abs (((delta T2) . n) - 0) < e ; ::_thesis: verum
end;
then A214: delta T2 is convergent by SEQ_2:def_6;
then A215: lim (delta T2) = 0 by A172, SEQ_2:def_7;
then A216: ( upper_sum ((f || ['c,b']),T2) is convergent & lim (upper_sum ((f || ['c,b']),T2)) = upper_integral (f || ['c,b']) ) by A166, A18, A214, INTEGRA4:9;
A217: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((delta_T)_._m)_-_0)_<_e
let e be real number ; ::_thesis: ( 0 < e implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0) < e )
assume A218: 0 < e ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0) < e
then consider n1 being Element of NAT such that
A219: for m being Element of NAT st n1 <= m holds
abs (((delta T1) . m) - 0) < e by A53, SEQ_2:def_7;
consider n2 being Element of NAT such that
A220: for m being Element of NAT st n2 <= m holds
abs (((delta T2) . m) - 0) < e by A172, A218;
reconsider n = max (n1,n2) as Element of NAT by XXREAL_0:16;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0) < e
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((delta_T)_._m)_-_0)_<_e
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((delta T) . m) - 0) < e )
assume A221: n <= m ; ::_thesis: abs (((delta T) . m) - 0) < e
n2 <= n by XXREAL_0:25;
then n2 <= m by A221, XXREAL_0:2;
then abs (((delta T2) . m) - 0) < e by A220;
then A222: abs (delta (T2 . m)) < e by INTEGRA3:def_2;
0 <= delta (T2 . m) by INTEGRA3:9;
then A223: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) < e by A222, ABSVALUE:def_1;
n1 <= n by XXREAL_0:25;
then n1 <= m by A221, XXREAL_0:2;
then abs (((delta T1) . m) - 0) < e by A219;
then A224: abs (delta (T1 . m)) < e by INTEGRA3:def_2;
0 <= delta (T1 . m) by INTEGRA3:9;
then A225: max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) < e by A224, ABSVALUE:def_1;
A226: for r being real number st r in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) holds
r < e
proof
reconsider Tm = T . m as Division of ['a,b'] ;
let y be real number ; ::_thesis: ( y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) implies y < e )
assume y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) ; ::_thesis: y < e
then consider x being set such that
A227: x in dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) and
A228: y = (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A227;
A229: x in Seg (len (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) by A227, FINSEQ_1:def_3;
then A230: 1 <= i by FINSEQ_1:1;
A231: len (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = len Tm by INTEGRA1:def_6;
then A232: i <= len Tm by A229, FINSEQ_1:1;
dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = dom Tm by A231, FINSEQ_3:29;
then A233: y = (upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((T . m),i))))) * (vol (divset ((T . m),i))) by A227, A228, INTEGRA1:def_6;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A234: S1 = T1 . m and
A235: S2 = T2 . m and
A236: T . m = S1 ^ S2 by A93;
A237: len Tm = (len S1) + (len S2) by A236, FINSEQ_1:22;
percases ( i <= len S1 or i > len S1 ) ;
suppose i <= len S1 ; ::_thesis: y < e
then A238: i in Seg (len S1) by A230;
then A239: i in dom S1 by FINSEQ_1:def_3;
len (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) = len S1 by A234, INTEGRA1:def_6;
then A240: i in dom (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A238, FINSEQ_1:def_3;
A241: divset ((T1 . m),i) = divset ((T . m),i) by A95, A234, A238;
A242: divset ((T1 . m),i) c= ['a,c'] by A139, A234, A238;
then divset ((T1 . m),i) c= ['a,b'] by A137, XBOOLE_1:1;
then (chi (['a,c'],['a,c'])) | (divset ((T1 . m),i)) = (chi (['a,b'],['a,b'])) | (divset ((T . m),i)) by A241, A242, Th4;
then y = (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) . i by A233, A234, A239, A241, INTEGRA1:def_6;
then y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by A240, FUNCT_1:def_3;
then y <= max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) by XXREAL_2:def_8;
hence y < e by A225, XXREAL_0:2; ::_thesis: verum
end;
suppose i > len S1 ; ::_thesis: y < e
then A243: (len S1) + 1 <= i by NAT_1:13;
then consider k being Nat such that
A244: ((len S1) + 1) + k = i by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
set i1 = 1 + k;
A245: i - (len S1) <= len S2 by A237, A232, XREAL_1:20;
1 + k = i - (len S1) by A244;
then 1 <= 1 + k by A243, XREAL_1:19;
then A246: 1 + k in Seg (len S2) by A244, A245;
then A247: 1 + k in dom S2 by FINSEQ_1:def_3;
A248: divset ((T2 . m),(1 + k)) = divset ((T . m),((len S1) + (1 + k))) by A112, A234, A235, A246;
A249: divset ((T2 . m),(1 + k)) c= ['c,b'] by A134, A235, A246;
then divset ((T2 . m),(1 + k)) c= ['a,b'] by A17, XBOOLE_1:1;
then y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k)))) by A233, A244, A248, A249, Th4;
then A250: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) . (1 + k) by A235, A247, INTEGRA1:def_6;
len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) = len S2 by A235, INTEGRA1:def_6;
then 1 + k in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A246, FINSEQ_1:def_3;
then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by A250, FUNCT_1:def_3;
then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) by XXREAL_2:def_8;
hence y < e by A223, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A251: 0 <= delta (T . m) by INTEGRA3:9;
max (rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) by XXREAL_2:def_8;
then delta (T . m) < e by A226;
then abs (delta (T . m)) < e by A251, ABSVALUE:def_1;
hence abs (((delta T) . m) - 0) < e by INTEGRA3:def_2; ::_thesis: verum
end;
hence for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0) < e ; ::_thesis: verum
end;
then A252: delta T is convergent by SEQ_2:def_6;
then A253: lim (delta T) = 0 by A217, SEQ_2:def_7;
(f || ['a,b']) | ['a,b'] is bounded by A4;
then A254: upper_integral (f || ['a,b']) = lim (upper_sum ((f || ['a,b']),T)) by A12, A252, A253, INTEGRA4:9;
A255: for i being Element of NAT holds lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i)))
proof
let i be Element of NAT ; ::_thesis: lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i)))
reconsider F = lower_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;
reconsider F1 = lower_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;
reconsider F2 = lower_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;
reconsider S = T . i as Division of ['a,b'] ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A256: S1 = T1 . i and
A257: S2 = T2 . i and
A258: T . i = S1 ^ S2 by A93;
A259: len F = len S by INTEGRA1:def_7
.= (len S1) + (len S2) by A258, FINSEQ_1:22
.= (len F1) + (len S2) by A256, INTEGRA1:def_7 ;
then A260: len F = (len F1) + (len F2) by A257, INTEGRA1:def_7;
A261: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F2_holds_
F_._((len_F1)_+_k)_=_F2_._k
let k be Nat; ::_thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )
assume k in dom F2 ; ::_thesis: F . ((len F1) + k) = F2 . k
then A262: k in Seg (len F2) by FINSEQ_1:def_3;
then 1 <= k by FINSEQ_1:1;
then A263: 1 + (len F1) <= k + (len F1) by XREAL_1:6;
k <= len F2 by A262, FINSEQ_1:1;
then A264: (len F1) + k <= len F by A260, XREAL_1:6;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by A263, XXREAL_0:2;
then k + (len F1) in Seg (len F) by A264;
then (len F1) + k in Seg (len S) by INTEGRA1:def_7;
then (len F1) + k in dom S by FINSEQ_1:def_3;
then A265: F . ((len F1) + k) = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def_7;
A266: k in Seg (len S2) by A257, A262, INTEGRA1:def_7;
then A267: k in dom S2 by FINSEQ_1:def_3;
len F1 = len S1 by A256, INTEGRA1:def_7;
then A268: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A112, A256, A257, A266;
A269: divset ((T2 . i),k) c= ['c,b'] by A134, A257, A266;
then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17, A268, XBOOLE_1:1;
then F . ((len F1) + k) = (lower_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A265, A268, A269, Th3;
hence F . ((len F1) + k) = F2 . k by A257, A267, INTEGRA1:def_7; ::_thesis: verum
end;
A270: now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_
F_._k_=_F1_._k
let k be Nat; ::_thesis: ( k in dom F1 implies F . k = F1 . k )
len (lower_volume ((f || ['a,b']),(T . i))) = len S by INTEGRA1:def_7;
then A271: dom (lower_volume ((f || ['a,b']),(T . i))) = dom S by FINSEQ_3:29;
assume A272: k in dom F1 ; ::_thesis: F . k = F1 . k
then k in Seg (len F1) by FINSEQ_1:def_3;
then A273: k in Seg (len S1) by A256, INTEGRA1:def_7;
then A274: k in dom S1 by FINSEQ_1:def_3;
len F1 <= len F by A259, NAT_1:11;
then dom F1 c= dom F by FINSEQ_3:30;
then A275: F . k = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by A272, A271, INTEGRA1:def_7;
A276: ( divset ((T . i),k) = divset ((T1 . i),k) & divset ((T1 . i),k) c= ['a,c'] ) by A139, A95, A256, A273;
then divset ((T . i),k) c= ['a,b'] by A137, XBOOLE_1:1;
then F . k = (lower_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A275, A276, Th3;
hence F . k = F1 . k by A256, A274, INTEGRA1:def_7; ::_thesis: verum
end;
dom F = Seg ((len F1) + (len F2)) by A260, FINSEQ_1:def_3;
hence lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A270, A261, FINSEQ_1:def_7; ::_thesis: verum
end;
A277: for i being Element of NAT holds Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i))))
proof
let i be Element of NAT ; ::_thesis: Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i))))
lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A255;
hence Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_holds_(lower_sum_((f_||_['a,b']),T))_._i_=_((lower_sum_((f_||_['a,c']),T1))_._i)_+_((lower_sum_((f_||_['c,b']),T2))_._i)
let i be Element of NAT ; ::_thesis: (lower_sum ((f || ['a,b']),T)) . i = ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i)
thus (lower_sum ((f || ['a,b']),T)) . i = lower_sum ((f || ['a,b']),(T . i)) by INTEGRA2:def_3
.= (lower_sum ((f || ['a,c']),(T1 . i))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) by A277
.= ((lower_sum ((f || ['a,c']),T1)) . i) + (lower_sum ((f || ['c,b']),(T2 . i))) by INTEGRA2:def_3
.= ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def_3 ; ::_thesis: verum
end;
then A278: lower_sum ((f || ['a,b']),T) = (lower_sum ((f || ['a,c']),T1)) + (lower_sum ((f || ['c,b']),T2)) by SEQ_1:7;
A279: f || ['a,c'] is Function of ['a,c'],REAL by A2, A137, Lm1, XBOOLE_1:1;
then A280: ( f || ['a,c'] is upper_integrable & f || ['a,c'] is lower_integrable ) by A138, INTEGRA4:10;
A281: ( upper_sum ((f || ['a,c']),T1) is convergent & lim (upper_sum ((f || ['a,c']),T1)) = upper_integral (f || ['a,c']) ) by A279, A138, A53, INTEGRA4:9;
then A282: (upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b']) by A165, A216, A254, SEQ_2:6;
A283: ( lower_sum ((f || ['a,c']),T1) is convergent & lim (lower_sum ((f || ['a,c']),T1)) = lower_integral (f || ['a,c']) ) by A279, A138, A53, INTEGRA4:8;
(f || ['a,b']) | ['a,b'] is bounded by A4;
then A284: lower_integral (f || ['a,b']) = lim (lower_sum ((f || ['a,b']),T)) by A12, A252, A253, INTEGRA4:8;
( lower_sum ((f || ['c,b']),T2) is convergent & lim (lower_sum ((f || ['c,b']),T2)) = lower_integral (f || ['c,b']) ) by A166, A18, A214, A215, INTEGRA4:8;
then A285: (lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b']) by A278, A283, A284, SEQ_2:6;
integral (f,a,b) = integral (f,['a,b']) by A1, INTEGRA5:def_4
.= (integral (f || ['a,c'])) + (integral (f || ['c,b'])) by A165, A281, A216, A254, SEQ_2:6 ;
hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A58, A57; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
f || ['a,b'] is integrable by A3, INTEGRA5:def_1;
then A286: upper_integral (f || ['a,b']) = lower_integral (f || ['a,b']) by INTEGRA1:def_16;
A287: ( f || ['c,b'] is upper_integrable & f || ['c,b'] is lower_integrable ) by A166, A18, INTEGRA4:10;
A288: lower_integral (f || ['a,c']) <= upper_integral (f || ['a,c']) by A279, A138, INTEGRA1:49;
then lower_integral (f || ['c,b']) = upper_integral (f || ['c,b']) by A286, A282, A285, A167, Th1;
then A289: f || ['c,b'] is integrable by A287, INTEGRA1:def_16;
lower_integral (f || ['a,c']) = upper_integral (f || ['a,c']) by A286, A282, A285, A288, A167, Th1;
then f || ['a,c'] is integrable by A280, INTEGRA1:def_16;
hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) by A289, INTEGRA5:def_1; ::_thesis: verum
end;
theorem Th17: :: INTEGRA6:17
for a, b, c being real number
for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
proof
let a, b, c be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] implies ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) )
assume that
A1: a <= b and
A2: f is_integrable_on ['a,b'] and
A3: ( f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) ; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
now__::_thesis:_(_b_=_c_implies_(_f_is_integrable_on_['a,c']_&_f_is_integrable_on_['c,b']_&_integral_(f,a,b)_=_(integral_(f,a,c))_+_(integral_(f,c,b))_)_)
assume A4: b = c ; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
then A5: ['c,b'] = [.c,b.] by INTEGRA5:def_3;
thus f is_integrable_on ['a,c'] by A2, A4; ::_thesis: ( f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
['c,b'] = [.(lower_bound ['c,b']),(upper_bound ['c,b']).] by INTEGRA1:4;
then ( lower_bound ['c,b'] = c & upper_bound ['c,b'] = b ) by A5, INTEGRA1:5;
then A6: vol ['c,b'] = 0 by A4;
then f || ['c,b'] is integrable by INTEGRA4:6;
hence f is_integrable_on ['c,b'] by INTEGRA5:def_1; ::_thesis: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
( c is Real & b is Real ) by XREAL_0:def_1;
then integral (f,c,b) = integral (f,['c,b']) by A5, INTEGRA5:19;
then integral (f,c,b) = 0 by A6, INTEGRA4:6;
hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A4; ::_thesis: verum
end;
hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) by A1, A2, A3, Lm2; ::_thesis: verum
end;
Lm3: for a, b, c being real number st a <= c & c <= b holds
( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
proof
let a, b, c be real number ; ::_thesis: ( a <= c & c <= b implies ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) )
assume that
A1: a <= c and
A2: c <= b ; ::_thesis: ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
A3: c in [.a,b.] by A1, A2, XXREAL_1:1;
hence c in ['a,b'] by A1, A2, INTEGRA5:def_3, XXREAL_0:2; ::_thesis: ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
A4: ['c,b'] = [.c,b.] by A2, INTEGRA5:def_3;
a <= b by A1, A2, XXREAL_0:2;
then A5: ( a in [.a,b.] & b in [.a,b.] ) by XXREAL_1:1;
( ['a,b'] = [.a,b.] & ['a,c'] = [.a,c.] ) by A1, A2, INTEGRA5:def_3, XXREAL_0:2;
hence ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) by A4, A3, A5, XXREAL_2:def_12; ::_thesis: verum
end;
theorem Th18: :: INTEGRA6:18
for a, c, d, b being real number
for f being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f )
proof
let a, c, d, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) )
assume that
A1: a <= c and
A2: c <= d and
A3: d <= b and
A4: f is_integrable_on ['a,b'] and
A5: f | ['a,b'] is bounded and
A6: ['a,b'] c= dom f ; ::_thesis: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f )
a <= d by A1, A2, XXREAL_0:2;
then A7: a <= b by A3, XXREAL_0:2;
A8: c <= b by A2, A3, XXREAL_0:2;
then c in ['a,b'] by A1, Lm3;
then A9: f is_integrable_on ['c,b'] by A4, A5, A6, A7, Th17;
A10: d in ['c,b'] by A2, A3, Lm3;
A11: ['c,b'] c= ['a,b'] by A1, A8, Lm3;
then ( ['c,b'] c= dom f & f | ['c,b'] is bounded ) by A5, A6, RFUNCT_1:74, XBOOLE_1:1;
hence f is_integrable_on ['c,d'] by A8, A10, A9, Th17; ::_thesis: ( f | ['c,d'] is bounded & ['c,d'] c= dom f )
['c,d'] c= ['c,b'] by A2, A3, Lm3;
then A12: ['c,d'] c= ['a,b'] by A11, XBOOLE_1:1;
hence f | ['c,d'] is bounded by A5, RFUNCT_1:74; ::_thesis: ['c,d'] c= dom f
thus ['c,d'] c= dom f by A6, A12, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: INTEGRA6:19
for a, c, d, b being real number
for f, g being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
proof
let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded ) )
assume that
A1: a <= c and
A2: ( c <= d & d <= b ) and
A3: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) and
A4: ['a,b'] c= dom f and
A5: ['a,b'] c= dom g ; ::_thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
A6: ['c,d'] c= ['c,b'] by A2, Lm3;
A7: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A1, A2, A3, A4, A5, Th18;
c <= b by A2, XXREAL_0:2;
then A8: ['c,b'] c= ['a,b'] by A1, Lm3;
then ['c,b'] c= dom f by A4, XBOOLE_1:1;
then A9: ['c,d'] c= dom f by A6, XBOOLE_1:1;
['c,b'] c= dom g by A5, A8, XBOOLE_1:1;
then A10: ['c,d'] c= dom g by A6, XBOOLE_1:1;
( f is_integrable_on ['c,d'] & g is_integrable_on ['c,d'] ) by A1, A2, A3, A4, A5, Th18;
hence f + g is_integrable_on ['c,d'] by A7, A9, A10, Th11; ::_thesis: (f + g) | ['c,d'] is bounded
(f + g) | (['c,d'] /\ ['c,d']) is bounded by A7, RFUNCT_1:83;
hence (f + g) | ['c,d'] is bounded ; ::_thesis: verum
end;
Lm4: for a, b, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
proof
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) and
A4: ['a,b'] c= dom f and
A5: c in ['a,b'] and
A6: d in ['a,b'] ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
A7: f is_integrable_on ['a,d'] by A1, A3, A4, A6, Th17;
A8: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A9: a <= d by A6, XXREAL_1:1;
A10: d <= b by A6, A8, XXREAL_1:1;
then ['a,d'] c= ['a,b'] by A9, Lm3;
then A11: ['a,d'] c= dom f by A4, XBOOLE_1:1;
a <= c by A5, A8, XXREAL_1:1;
then A12: c in ['a,d'] by A2, Lm3;
f | ['a,d'] is bounded by A3, A4, A9, A10, Th18;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A9, A12, A11, A7, Th17; ::_thesis: verum
end;
theorem Th20: :: INTEGRA6:20
for a, b, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
proof
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
now__::_thesis:_(_not_c_<=_d_implies_integral_(f,a,d)_=_(integral_(f,a,c))_+_(integral_(f,c,d))_)
assume A2: not c <= d ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
then integral (f,a,c) = (integral (f,a,d)) + (integral (f,d,c)) by A1, Lm4;
then A3: integral (f,a,d) = (integral (f,a,c)) - (integral (f,d,c)) ;
integral (f,c,d) = - (integral (f,['d,c'])) by A2, INTEGRA5:def_4;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A2, A3, INTEGRA5:def_4; ::_thesis: verum
end;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A1, Lm4; ::_thesis: verum
end;
Lm5: for a, b, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) )
proof
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) and
A4: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) )
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A5: ( a <= c & d <= b ) by A4, XXREAL_1:1;
then A6: f | ['c,d'] is bounded by A2, A3, Th18;
( ['c,d'] c= dom f & f is_integrable_on ['c,d'] ) by A2, A3, A5, Th18;
hence ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) by A2, A6, Th7, Th8, RFUNCT_1:82, VALUED_1:def_11; ::_thesis: verum
end;
theorem Th21: :: INTEGRA6:21
for a, b, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) )
proof
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) )
A2: now__::_thesis:_(_not_c_<=_d_implies_(_['(min_(c,d)),(max_(c,d))']_c=_dom_(abs_f)_&_abs_f_is_integrable_on_['(min_(c,d)),(max_(c,d))']_&_(abs_f)_|_['(min_(c,d)),(max_(c,d))']_is_bounded_&_abs_(integral_(f,c,d))_<=_integral_((abs_f),(min_(c,d)),(max_(c,d)))_)_)
assume A3: not c <= d ; ::_thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) )
then integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def_4;
then integral (f,c,d) = - (integral (f,d,c)) by A3, INTEGRA5:def_4;
then A4: abs (integral (f,c,d)) = abs (integral (f,d,c)) by COMPLEX1:52;
( d = min (c,d) & c = max (c,d) ) by A3, XXREAL_0:def_9, XXREAL_0:def_10;
hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A3, A4, Lm5; ::_thesis: verum
end;
now__::_thesis:_(_c_<=_d_implies_(_['(min_(c,d)),(max_(c,d))']_c=_dom_(abs_f)_&_abs_f_is_integrable_on_['(min_(c,d)),(max_(c,d))']_&_(abs_f)_|_['(min_(c,d)),(max_(c,d))']_is_bounded_&_abs_(integral_(f,c,d))_<=_integral_((abs_f),(min_(c,d)),(max_(c,d)))_)_)
assume A5: c <= d ; ::_thesis: ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) )
then ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10;
hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A1, A5, Lm5; ::_thesis: verum
end;
hence ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) by A2; ::_thesis: verum
end;
Lm6: for a, b, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) )
proof
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) )
( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10;
hence ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) by A1, A3, Th21; ::_thesis: verum
end;
Lm7: for a, b, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
abs (integral (f,d,c)) <= integral ((abs f),c,d)
proof
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
abs (integral (f,d,c)) <= integral ((abs f),c,d)
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies abs (integral (f,d,c)) <= integral ((abs f),c,d) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and
A4: d in ['a,b'] ; ::_thesis: abs (integral (f,d,c)) <= integral ((abs f),c,d)
A5: ( abs (integral (f,c,d)) <= integral ((abs f),c,d) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, Lm6, INTEGRA5:def_4;
percases ( c = d or c <> d ) ;
suppose c = d ; ::_thesis: abs (integral (f,d,c)) <= integral ((abs f),c,d)
hence abs (integral (f,d,c)) <= integral ((abs f),c,d) by A1, A3, Lm6; ::_thesis: verum
end;
suppose c <> d ; ::_thesis: abs (integral (f,d,c)) <= integral ((abs f),c,d)
then c < d by A2, XXREAL_0:1;
then integral (f,d,c) = - (integral (f,['c,d'])) by INTEGRA5:def_4;
hence abs (integral (f,d,c)) <= integral ((abs f),c,d) by A5, COMPLEX1:52; ::_thesis: verum
end;
end;
end;
theorem :: INTEGRA6:22
for a, b, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) & abs (integral (f,d,c)) <= integral ((abs f),c,d) ) by Lm6, Lm7;
Lm8: for a, b, c, d, e being real number
for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) holds
abs (integral (f,c,d)) <= e * (abs (d - c))
proof
let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) holds
abs (integral (f,c,d)) <= e * (abs (d - c))
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) implies abs (integral (f,c,d)) <= e * (abs (d - c)) )
set A = ['(min (c,d)),(max (c,d))'];
assume that
A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) and
A2: for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ; ::_thesis: abs (integral (f,c,d)) <= e * (abs (d - c))
rng (abs f) c= REAL ;
then A3: abs f is Function of (dom (abs f)),REAL by FUNCT_2:2;
['(min (c,d)),(max (c,d))'] c= dom (abs f) by A1, Th21;
then reconsider g = (abs f) || ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32;
A4: vol ['(min (c,d)),(max (c,d))'] = abs (d - c) by Th6;
abs f is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, Th21;
then A5: g is integrable by INTEGRA5:def_1;
reconsider e = e as Real by XREAL_0:def_1;
consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that
A6: rng h = {e} and
A7: h | ['(min (c,d)),(max (c,d))'] is bounded by INTEGRA4:5;
A8: now__::_thesis:_for_x_being_Real_st_x_in_['(min_(c,d)),(max_(c,d))']_holds_
g_._x_<=_h_._x
let x be Real; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x )
assume A9: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: g . x <= h . x
then g . x = (abs f) . x by FUNCT_1:49;
then A10: g . x = abs (f . x) by VALUED_1:18;
h . x in {e} by A6, A9, FUNCT_2:4;
then h . x = e by TARSKI:def_1;
hence g . x <= h . x by A2, A9, A10; ::_thesis: verum
end;
A11: abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) by A1, Th21;
( min (c,d) <= c & c <= max (c,d) ) by XXREAL_0:17, XXREAL_0:25;
then min (c,d) <= max (c,d) by XXREAL_0:2;
then A12: integral ((abs f),(min (c,d)),(max (c,d))) = integral ((abs f),['(min (c,d)),(max (c,d))']) by INTEGRA5:def_4;
(abs f) | ['(min (c,d)),(max (c,d))'] is bounded by A1, Th21;
then A13: g | ['(min (c,d)),(max (c,d))'] is bounded ;
( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) ) by A6, INTEGRA4:4;
then integral ((abs f),(min (c,d)),(max (c,d))) <= e * (abs (d - c)) by A12, A7, A8, A5, A13, A4, INTEGRA2:34;
hence abs (integral (f,c,d)) <= e * (abs (d - c)) by A11, XXREAL_0:2; ::_thesis: verum
end;
Lm9: for a, b, c, d, e being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) holds
abs (integral (f,c,d)) <= e * (d - c)
proof
let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) holds
abs (integral (f,c,d)) <= e * (d - c)
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) implies abs (integral (f,c,d)) <= e * (d - c) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) ) ; ::_thesis: abs (integral (f,c,d)) <= e * (d - c)
0 <= d - c by A2, XREAL_1:48;
then A4: abs (d - c) = d - c by ABSVALUE:def_1;
( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10;
hence abs (integral (f,c,d)) <= e * (d - c) by A1, A3, A4, Lm8; ::_thesis: verum
end;
Lm10: for a, b, c, d, e being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) holds
abs (integral (f,d,c)) <= e * (d - c)
proof
let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) holds
abs (integral (f,d,c)) <= e * (d - c)
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) implies abs (integral (f,d,c)) <= e * (d - c) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and
A4: d in ['a,b'] and
A5: for x being real number st x in ['c,d'] holds
abs (f . x) <= e ; ::_thesis: abs (integral (f,d,c)) <= e * (d - c)
A6: ( abs (integral (f,c,d)) <= e * (d - c) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, A5, Lm9, INTEGRA5:def_4;
percases ( c = d or c <> d ) ;
suppose c = d ; ::_thesis: abs (integral (f,d,c)) <= e * (d - c)
hence abs (integral (f,d,c)) <= e * (d - c) by A1, A3, A5, Lm9; ::_thesis: verum
end;
suppose c <> d ; ::_thesis: abs (integral (f,d,c)) <= e * (d - c)
then c < d by A2, XXREAL_0:1;
then integral (f,d,c) = - (integral (f,['c,d'])) by INTEGRA5:def_4;
hence abs (integral (f,d,c)) <= e * (d - c) by A6, COMPLEX1:52; ::_thesis: verum
end;
end;
end;
theorem :: INTEGRA6:23
for a, b, c, d, e being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being real number st x in ['c,d'] holds
abs (f . x) <= e ) holds
( abs (integral (f,c,d)) <= e * (d - c) & abs (integral (f,d,c)) <= e * (d - c) ) by Lm9, Lm10;
Lm11: for a, b, c, d being real number
for f, g being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
proof
let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) )
assume that
A1: a <= b and
A2: c <= d and
A3: f is_integrable_on ['a,b'] and
A4: g is_integrable_on ['a,b'] and
A5: f | ['a,b'] is bounded and
A6: g | ['a,b'] is bounded and
A7: ['a,b'] c= dom f and
A8: ['a,b'] c= dom g and
A9: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A10: ( a <= c & d <= b ) by A9, XXREAL_1:1;
then A11: ( f is_integrable_on ['c,d'] & ['c,d'] c= dom f ) by A2, A3, A5, A7, Th18;
A12: ( g is_integrable_on ['c,d'] & ['c,d'] c= dom g ) by A2, A4, A6, A8, A10, Th18;
A13: ( f | ['c,d'] is bounded & g | ['c,d'] is bounded ) by A2, A3, A4, A5, A6, A7, A8, A10, Th18;
then (f + g) | (['c,d'] /\ ['c,d']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) by A2, A11, A13, A12, Th11, Th12, RFUNCT_1:84; ::_thesis: verum
end;
theorem Th24: :: INTEGRA6:24
for a, b, c, d being real number
for f, g being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
proof
let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
now__::_thesis:_(_not_c_<=_d_implies_(_integral_((f_+_g),c,d)_=_(integral_(f,c,d))_+_(integral_(g,c,d))_&_integral_((f_-_g),c,d)_=_(integral_(f,c,d))_-_(integral_(g,c,d))_)_)
assume A2: not c <= d ; ::_thesis: ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
then A3: integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def_4;
A4: integral (g,c,d) = - (integral (g,['d,c'])) by A2, INTEGRA5:def_4;
integral ((f + g),c,d) = - (integral ((f + g),['d,c'])) by A2, INTEGRA5:def_4;
hence integral ((f + g),c,d) = - (integral ((f + g),d,c)) by A2, INTEGRA5:def_4
.= - ((integral (f,d,c)) + (integral (g,d,c))) by A1, A2, Lm11
.= (- (integral (f,d,c))) - (integral (g,d,c))
.= (integral (f,c,d)) - (integral (g,d,c)) by A2, A3, INTEGRA5:def_4
.= (integral (f,c,d)) + (integral (g,c,d)) by A2, A4, INTEGRA5:def_4 ;
::_thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
integral ((f - g),c,d) = - (integral ((f - g),['d,c'])) by A2, INTEGRA5:def_4;
hence integral ((f - g),c,d) = - (integral ((f - g),d,c)) by A2, INTEGRA5:def_4
.= - ((integral (f,d,c)) - (integral (g,d,c))) by A1, A2, Lm11
.= - ((integral (f,d,c)) + (integral (g,c,d))) by A2, A4, INTEGRA5:def_4
.= (- (integral (f,d,c))) - (integral (g,c,d))
.= (integral (f,c,d)) - (integral (g,c,d)) by A2, A3, INTEGRA5:def_4 ;
::_thesis: verum
end;
hence ( integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) by A1, Lm11; ::_thesis: verum
end;
Lm12: for a, b, c, d, e being real number
for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((e (#) f),c,d) = e * (integral (f,c,d))
proof
let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((e (#) f),c,d) = e * (integral (f,c,d))
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & c <= d & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((e (#) f),c,d) = e * (integral (f,c,d)) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) and
A4: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((e (#) f),c,d) = e * (integral (f,c,d))
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A5: ( a <= c & d <= b ) by A4, XXREAL_1:1;
then A6: ['c,d'] c= dom f by A2, A3, Th18;
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) by A2, A3, A5, Th18;
hence integral ((e (#) f),c,d) = e * (integral (f,c,d)) by A2, A6, Th10; ::_thesis: verum
end;
theorem :: INTEGRA6:25
for a, b, c, d, e being real number
for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((e (#) f),c,d) = e * (integral (f,c,d))
proof
let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((e (#) f),c,d) = e * (integral (f,c,d))
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((e (#) f),c,d) = e * (integral (f,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((e (#) f),c,d) = e * (integral (f,c,d))
now__::_thesis:_(_not_c_<=_d_implies_integral_((e_(#)_f),c,d)_=_e_*_(integral_(f,c,d))_)
assume A2: not c <= d ; ::_thesis: integral ((e (#) f),c,d) = e * (integral (f,c,d))
then A3: integral (f,c,d) = - (integral (f,['d,c'])) by INTEGRA5:def_4;
thus integral ((e (#) f),c,d) = - (integral ((e (#) f),['d,c'])) by A2, INTEGRA5:def_4
.= - (integral ((e (#) f),d,c)) by A2, INTEGRA5:def_4
.= - (e * (integral (f,d,c))) by A1, A2, Lm12
.= e * (- (integral (f,d,c)))
.= e * (integral (f,c,d)) by A2, A3, INTEGRA5:def_4 ; ::_thesis: verum
end;
hence integral ((e (#) f),c,d) = e * (integral (f,c,d)) by A1, Lm12; ::_thesis: verum
end;
theorem Th26: :: INTEGRA6:26
for a, b, e being real number
for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
proof
let a, b, e be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) ) )
assume that
A1: a <= b and
A2: ['a,b'] c= dom f and
A3: for x being real number st x in ['a,b'] holds
f . x = e ; ::_thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
rng f c= REAL ;
then f is Function of (dom f),REAL by FUNCT_2:2;
then reconsider g = f || ['a,b'] as Function of ['a,b'],REAL by A2, FUNCT_2:32;
reconsider e1 = e as Real by XREAL_0:def_1;
consider h being Function of ['a,b'],REAL such that
A4: rng h = {e1} and
A5: h | ['a,b'] is bounded by INTEGRA4:5;
integral h = e1 * (vol ['a,b']) by A4, INTEGRA4:4;
then A6: integral h = e * (b - a) by A1, Th5;
A7: for x being set st x in ['a,b'] holds
g . x = h . x
proof
let x0 be set ; ::_thesis: ( x0 in ['a,b'] implies g . x0 = h . x0 )
assume A8: x0 in ['a,b'] ; ::_thesis: g . x0 = h . x0
then reconsider x = x0 as real number ;
g . x0 = f . x by A8, FUNCT_1:49;
then A9: g . x0 = e by A3, A8;
h . x in {e1} by A4, A8, FUNCT_2:4;
hence g . x0 = h . x0 by A9, TARSKI:def_1; ::_thesis: verum
end;
then A10: h = g by FUNCT_2:12;
h is integrable by A4, INTEGRA4:4;
hence f is_integrable_on ['a,b'] by A10, INTEGRA5:def_1; ::_thesis: ( f | ['a,b'] is bounded & integral (f,a,b) = e * (b - a) )
thus f | ['a,b'] is bounded ::_thesis: integral (f,a,b) = e * (b - a)
proof
consider r being real number such that
A11: for c being set st c in ['a,b'] /\ (dom g) holds
abs (g . c) <= r by A5, A10, RFUNCT_1:73;
now__::_thesis:_for_c_being_set_st_c_in_['a,b']_/\_(dom_f)_holds_
abs_(f_._c)_<=_r
let c be set ; ::_thesis: ( c in ['a,b'] /\ (dom f) implies abs (f . c) <= r )
['a,b'] /\ (dom g) = ['a,b'] /\ ((dom f) /\ ['a,b']) by RELAT_1:61;
then A12: ['a,b'] /\ (dom g) = (['a,b'] /\ ['a,b']) /\ (dom f) by XBOOLE_1:16;
assume c in ['a,b'] /\ (dom f) ; ::_thesis: abs (f . c) <= r
then ( abs (g . c) <= r & c in dom g ) by A11, A12, XBOOLE_0:def_4;
hence abs (f . c) <= r by FUNCT_1:47; ::_thesis: verum
end;
hence f | ['a,b'] is bounded by RFUNCT_1:73; ::_thesis: verum
end;
integral (f,a,b) = integral (f,['a,b']) by A1, INTEGRA5:def_4;
hence integral (f,a,b) = e * (b - a) by A7, A6, FUNCT_2:12; ::_thesis: verum
end;
theorem Th27: :: INTEGRA6:27
for a, b, e, c, d being real number
for f being PartFunc of REAL,REAL st a <= b & ( for x being real number st x in ['a,b'] holds
f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = e * (d - c)
proof
let a, b, e, c, d be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= b & ( for x being real number st x in ['a,b'] holds
f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = e * (d - c)
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= b & ( for x being real number st x in ['a,b'] holds
f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = e * (d - c) )
assume that
A1: a <= b and
A2: for x being real number st x in ['a,b'] holds
f . x = e and
A3: ['a,b'] c= dom f and
A4: c in ['a,b'] and
A5: d in ['a,b'] ; ::_thesis: integral (f,c,d) = e * (d - c)
A6: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A2, A3, Th26;
A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A8: c <= b by A4, XXREAL_1:1;
A9: a <= c by A4, A7, XXREAL_1:1;
then A10: ['c,b'] c= ['a,b'] by A8, Lm3;
A11: d <= b by A5, A7, XXREAL_1:1;
A12: a <= d by A5, A7, XXREAL_1:1;
A13: ['a,c'] c= ['a,b'] by A9, A8, Lm3;
percases ( c <= d or not c <= d ) ;
supposeA14: c <= d ; ::_thesis: integral (f,c,d) = e * (d - c)
then ['c,d'] c= ['c,b'] by A11, Lm3;
then ['c,d'] c= ['a,b'] by A10, XBOOLE_1:1;
then A15: for x being real number st x in ['c,d'] holds
f . x = e by A2;
['c,d'] c= dom f by A3, A9, A11, A6, A14, Th18;
hence integral (f,c,d) = e * (d - c) by A14, A15, Th26; ::_thesis: verum
end;
supposeA16: not c <= d ; ::_thesis: integral (f,c,d) = e * (d - c)
then ['d,c'] c= ['a,c'] by A12, Lm3;
then ['d,c'] c= ['a,b'] by A13, XBOOLE_1:1;
then A17: for x being real number st x in ['d,c'] holds
f . x = e by A2;
integral (f,c,d) = - (integral (f,['d,c'])) by A16, INTEGRA5:def_4;
then A18: integral (f,c,d) = - (integral (f,d,c)) by A16, INTEGRA5:def_4;
['d,c'] c= dom f by A3, A12, A8, A6, A16, Th18;
then integral (f,d,c) = e * (c - d) by A16, A17, Th26;
hence integral (f,c,d) = e * (d - c) by A18; ::_thesis: verum
end;
end;
end;
begin
theorem Th28: :: INTEGRA6:28
for a, b being real number
for f being PartFunc of REAL,REAL
for x0 being real number
for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f . x0 )
proof
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL
for x0 being real number
for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f . x0 )
let f be PartFunc of REAL,REAL; ::_thesis: for x0 being real number
for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f . x0 )
deffunc H1( set ) -> Element of NAT = 0 ;
let x0 be real number ; ::_thesis: for F being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f . x0 )
let F be PartFunc of REAL,REAL; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 implies ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) )
assume that
A1: a <= b and
A2: f is_integrable_on ['a,b'] and
A3: f | ['a,b'] is bounded and
A4: ['a,b'] c= dom f and
A5: ].a,b.[ c= dom F and
A6: for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) and
A7: x0 in ].a,b.[ and
A8: f is_continuous_in x0 ; ::_thesis: ( F is_differentiable_in x0 & diff (F,x0) = f . x0 )
defpred S1[ set ] means x0 + (R_id $1) in ].a,b.[;
deffunc H2( Element of REAL ) -> Element of REAL = (f . x0) * $1;
consider L being Function of REAL,REAL such that
A9: for h being Real holds L . h = H2(h) from FUNCT_2:sch_4();
reconsider L = L as PartFunc of REAL,REAL ;
deffunc H3( set ) -> Element of REAL = ((F . (x0 + (R_id $1))) - (F . x0)) - (L . (R_id $1));
reconsider L = L as LinearFunc by A9, FDIFF_1:def_3;
consider R being Function such that
A10: ( dom R = REAL & ( for x being set st x in REAL holds
( ( S1[x] implies R . x = H3(x) ) & ( not S1[x] implies R . x = H1(x) ) ) ) ) from PARTFUN1:sch_1();
rng R c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng R or y in REAL )
assume y in rng R ; ::_thesis: y in REAL
then consider x being set such that
A11: x in dom R and
A12: y = R . x by FUNCT_1:def_3;
A13: ( not S1[x] implies R . x = H1(x) ) by A10, A11;
( S1[x] implies R . x = H3(x) ) by A10, A11;
hence y in REAL by A12, A13; ::_thesis: verum
end;
then reconsider R = R as PartFunc of REAL,REAL by A10, RELSET_1:4;
A14: R is total by A10, PARTFUN1:def_2;
A15: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
A16: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )
A17: for e being real number st 0 < e holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h ") (#) (R /* h)) . m) - 0) < e
proof
set g = REAL --> (f . x0);
let e0 be real number ; ::_thesis: ( 0 < e0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h ") (#) (R /* h)) . m) - 0) < e0 )
set e = e0 / 2;
A18: ( h is convergent & lim h = 0 ) ;
assume A19: 0 < e0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h ") (#) (R /* h)) . m) - 0) < e0
then 0 < e0 / 2 by XREAL_1:215;
then consider p being real number such that
A20: 0 < p and
A21: for t being real number st t in dom f & abs (t - x0) < p holds
abs ((f . t) - (f . x0)) < e0 / 2 by A8, FCONT_1:3;
A22: 0 < p / 2 by A20, XREAL_1:215;
A23: p / 2 < p by A20, XREAL_1:216;
consider N being Neighbourhood of x0 such that
A24: N c= ].a,b.[ by A7, RCOMP_1:18;
consider q being real number such that
A25: 0 < q and
A26: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def_6;
A27: q / 2 < q by A25, XREAL_1:216;
set r = min ((p / 2),(q / 2));
0 < q / 2 by A25, XREAL_1:215;
then 0 < min ((p / 2),(q / 2)) by A22, XXREAL_0:15;
then consider n being Element of NAT such that
A28: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A18, SEQ_2:def_7;
take n ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((((h ") (#) (R /* h)) . m) - 0) < e0
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((((h ") (#) (R /* h)) . m) - 0) < e0 )
min ((p / 2),(q / 2)) <= q / 2 by XXREAL_0:17;
then A29: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A27, Th2, XXREAL_0:2;
assume n <= m ; ::_thesis: abs ((((h ") (#) (R /* h)) . m) - 0) < e0
then A30: abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A28;
then abs ((x0 + (h . m)) - x0) < min ((p / 2),(q / 2)) ;
then x0 + (h . m) in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1;
then A31: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A29;
then A32: x0 + (h . m) in ].a,b.[ by A24, A26;
then x0 + (R_id (h . m)) in ].a,b.[ by RSSPACE:def_3;
then R . (h . m) = ((F . (x0 + (R_id (h . m)))) - (F . x0)) - (L . (R_id (h . m))) by A10;
then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (R_id (h . m))) by RSSPACE:def_3;
then R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - (L . (h . m)) by RSSPACE:def_3;
then A33: R . (h . m) = ((F . (x0 + (h . m))) - (F . x0)) - ((f . x0) * (h . m)) by A9;
F . (x0 + (h . m)) = integral (f,a,(x0 + (h . m))) by A6, A24, A26, A31;
then A34: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((f . x0) * (h . m)) by A6, A7, A33;
A35: dom (REAL --> (f . x0)) = REAL by FUNCT_2:def_1;
then ['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> (f . x0))) by A4, XBOOLE_1:27;
then A36: ['a,b'] c= dom (f - (REAL --> (f . x0))) by VALUED_1:12;
A37: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A38: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A15, A32, Th20;
A39: min ((p / 2),(q / 2)) <= p / 2 by XXREAL_0:17;
A40: for x being real number st x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] holds
abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2
proof
let x be real number ; ::_thesis: ( x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] implies abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 )
reconsider x1 = x as Real by XREAL_0:def_1;
A41: ( min (x0,(x0 + (h . m))) <= x0 & x0 <= max (x0,(x0 + (h . m))) ) by XXREAL_0:17, XXREAL_0:25;
assume x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] ; ::_thesis: abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2
then A42: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A41, INTEGRA5:def_3, XXREAL_0:2;
abs (x - x0) <= abs (h . m)
proof
percases ( x0 <= x0 + (h . m) or not x0 <= x0 + (h . m) ) ;
suppose x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m)
then ( x0 = min (x0,(x0 + (h . m))) & x0 + (h . m) = max (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10;
then x in { z where z is Real : ( x0 <= z & z <= x0 + (h . m) ) } by A42, RCOMP_1:def_1;
then A43: ex z being Real st
( x = z & x0 <= z & z <= x0 + (h . m) ) ;
then 0 <= x - x0 by XREAL_1:48;
then A44: abs (x - x0) = x - x0 by ABSVALUE:def_1;
A45: x - x0 <= (x0 + (h . m)) - x0 by A43, XREAL_1:9;
then 0 <= h . m by A43, XREAL_1:48;
hence abs (x - x0) <= abs (h . m) by A45, A44, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA46: not x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m)
then ( x0 = max (x0,(x0 + (h . m))) & x0 + (h . m) = min (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10;
then x in { z where z is Real : ( x0 + (h . m) <= z & z <= x0 ) } by A42, RCOMP_1:def_1;
then A47: ex z being Real st
( x = z & x0 + (h . m) <= z & z <= x0 ) ;
then A48: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:9;
percases ( x - x0 <> 0 or x - x0 = 0 ) ;
supposeA49: x - x0 <> 0 ; ::_thesis: abs (x - x0) <= abs (h . m)
(x0 + (h . m)) - x0 < x0 - x0 by A46, XREAL_1:14;
then A50: abs (h . m) = - (h . m) by ABSVALUE:def_1;
x - x0 < 0 by A47, A49, XREAL_1:47;
then abs (x - x0) = - (x - x0) by ABSVALUE:def_1;
hence abs (x - x0) <= abs (h . m) by A48, A50, XREAL_1:24; ::_thesis: verum
end;
suppose x - x0 = 0 ; ::_thesis: abs (x - x0) <= abs (h . m)
then abs (x - x0) = 0 by ABSVALUE:def_1;
hence abs (x - x0) <= abs (h . m) by COMPLEX1:46; ::_thesis: verum
end;
end;
end;
end;
end;
then A51: abs (x - x0) < min ((p / 2),(q / 2)) by A30, XXREAL_0:2;
then x in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1;
then x in ].(x0 - q),(x0 + q).[ by A29;
then x in ].a,b.[ by A24, A26;
then A52: x in [.a,b.] by A37;
abs (x - x0) < p / 2 by A39, A51, XXREAL_0:2;
then abs (x - x0) < p by A23, XXREAL_0:2;
then abs ((f . x) - (f . x0)) <= e0 / 2 by A4, A15, A21, A52;
then abs ((f . x1) - ((REAL --> (f . x0)) . x1)) <= e0 / 2 by FUNCOP_1:7;
hence abs ((f - (REAL --> (f . x0))) . x) <= e0 / 2 by A15, A36, A52, VALUED_1:13; ::_thesis: verum
end;
A53: for x being real number st x in ['a,b'] holds
(REAL --> (f . x0)) . x = f . x0 by FUNCOP_1:7;
then A54: (REAL --> (f . x0)) | ['a,b'] is bounded by A1, A35, Th26;
then A55: (f - (REAL --> (f . x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, RFUNCT_1:84;
rng h c= dom R by A10;
then (R . (h . m)) / (h . m) = ((R /* h) . m) / (h . m) by FUNCT_2:108;
then (R . (h . m)) / (h . m) = ((R /* h) . m) * ((h ") . m) by VALUED_1:10;
then A56: (R . (h . m)) / (h . m) = ((h ") (#) (R /* h)) . m by SEQ_1:8;
h . m <> 0 by SEQ_1:4;
then A57: 0 < abs (h . m) by COMPLEX1:47;
A58: REAL --> (f . x0) is_integrable_on ['a,b'] by A1, A35, A53, Th26;
then f - (REAL --> (f . x0)) is_integrable_on ['a,b'] by A2, A3, A4, A35, A54, Th11;
then A59: abs (integral ((f - (REAL --> (f . x0))),x0,(x0 + (h . m)))) <= (e0 / 2) * (abs ((x0 + (h . m)) - x0)) by A1, A7, A15, A37, A32, A55, A36, A40, Lm8;
integral ((REAL --> (f . x0)),x0,(x0 + (h . m))) = (f . x0) * ((x0 + (h . m)) - x0) by A1, A7, A15, A37, A32, A35, A53, Th27;
then R . (h . m) = integral ((f - (REAL --> (f . x0))),x0,(x0 + (h . m))) by A1, A2, A3, A4, A7, A15, A37, A32, A34, A35, A58, A54, A38, Th24;
then ( abs ((R . (h . m)) / (h . m)) = (abs (R . (h . m))) / (abs (h . m)) & (abs (R . (h . m))) / (abs (h . m)) <= ((e0 / 2) * (abs (h . m))) / (abs (h . m)) ) by A59, A57, COMPLEX1:67, XREAL_1:72;
then A60: abs ((R . (h . m)) / (h . m)) <= e0 / 2 by A57, XCMPLX_1:89;
e0 / 2 < e0 by A19, XREAL_1:216;
hence abs ((((h ") (#) (R /* h)) . m) - 0) < e0 by A60, A56, XXREAL_0:2; ::_thesis: verum
end;
hence (h ") (#) (R /* h) is convergent by SEQ_2:def_6; ::_thesis: lim ((h ") (#) (R /* h)) = 0
hence lim ((h ") (#) (R /* h)) = 0 by A17, SEQ_2:def_7; ::_thesis: verum
end;
consider N being Neighbourhood of x0 such that
A61: N c= ].a,b.[ by A7, RCOMP_1:18;
reconsider R = R as RestFunc by A14, A16, FDIFF_1:def_2;
A62: for x being Real st x in N holds
(F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume x in N ; ::_thesis: (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0))
then x0 + (x - x0) in N ;
then x0 + (R_id (x - x0)) in N by RSSPACE:def_3;
then ( x0 + (R_id (x - x0)) = x0 + (x - x0) & R . (x - x0) = H3(x - x0) ) by A10, A61, RSSPACE:def_3;
hence (F . x) - (F . x0) = (L . (x - x0)) + (R . (x - x0)) ; ::_thesis: verum
end;
A63: N c= dom F by A5, A61, XBOOLE_1:1;
hence A64: F is_differentiable_in x0 by A62, FDIFF_1:def_4; ::_thesis: diff (F,x0) = f . x0
L . 1 = (f . x0) * 1 by A9;
hence diff (F,x0) = f . x0 by A63, A62, A64, FDIFF_1:def_5; ::_thesis: verum
end;
Lm13: for a, b being real number
for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
proof
deffunc H1( real number ) -> Element of NAT = 0 ;
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
defpred S1[ set ] means $1 in ].a,b.[;
deffunc H2( real number ) -> Element of REAL = integral (f,a,$1);
consider F being Function such that
A1: ( dom F = REAL & ( for x being Element of REAL holds
( ( S1[x] implies F . x = H2(x) ) & ( not S1[x] implies F . x = H1(x) ) ) ) ) from PARTFUN1:sch_4();
now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_
y_in_REAL
let y be set ; ::_thesis: ( y in rng F implies y in REAL )
assume y in rng F ; ::_thesis: y in REAL
then consider x being set such that
A2: x in dom F and
A3: y = F . x by FUNCT_1:def_3;
reconsider x = x as Element of REAL by A1, A2;
A4: now__::_thesis:_(_not_x_in_].a,b.[_implies_y_in_REAL_)
assume not x in ].a,b.[ ; ::_thesis: y in REAL
then F . x = 0 by A1;
hence y in REAL by A3; ::_thesis: verum
end;
now__::_thesis:_(_x_in_].a,b.[_implies_y_in_REAL_)
assume x in ].a,b.[ ; ::_thesis: y in REAL
then F . x = integral (f,a,x) by A1;
hence y in REAL by A3; ::_thesis: verum
end;
hence y in REAL by A4; ::_thesis: verum
end;
then rng F c= REAL by TARSKI:def_3;
then reconsider F = F as PartFunc of REAL,REAL by A1, RELSET_1:4;
take F ; ::_thesis: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
thus ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) ) by A1; ::_thesis: verum
end;
theorem :: INTEGRA6:29
for a, b being real number
for f being PartFunc of REAL,REAL
for x0 being real number st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds
ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 )
proof
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,REAL
for x0 being real number st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds
ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 )
let f be PartFunc of REAL,REAL; ::_thesis: for x0 being real number st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds
ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 )
let x0 be real number ; ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 implies ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) )
consider F being PartFunc of REAL,REAL such that
A1: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) ) by Lm13;
assume ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 ) ; ::_thesis: ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 )
then ( F is_differentiable_in x0 & diff (F,x0) = f . x0 ) by A1, Th28;
hence ex F being PartFunc of REAL,REAL st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 ) by A1; ::_thesis: verum
end;