let a, b, c be Real; 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; ( 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
; ( 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 ) )
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]
consider S2 being sequence of (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 );
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 ;
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']
;
( 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;
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 ;
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
;
( 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;
hence
(
D = T2 . n & ( for
i being
Element of
NAT st
i in dom D holds
c < D . i ) )
;
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 )
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 ;
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 for i, j being Nat st i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j holds
(S1 ^ S2) . i < (S1 ^ S2) . jlet i,
j be
Nat;
( 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
;
(S1 ^ S2) . i < (S1 ^ S2) . jA67:
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 ( 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
;
(S1 ^ S2) . i < (S1 ^ S2) . jthen 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 ( 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
;
(S1 ^ S2) . i < (S1 ^ S2) . jthen 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;
verum end; hence
(S1 ^ S2) . i < (S1 ^ S2) . j
by A77;
verum end; A86:
1
<= j
by A65, FINSEQ_3:25;
hence
(S1 ^ S2) . i < (S1 ^ S2) . j
by A70;
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]
;
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 ;
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'];
( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) )
assume A96:
S0 = T1 . i
;
( 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)
;
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 ( 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
;
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
;
verum
now ( k = 1 implies divset ((T . i),k) = divset ((T1 . i),k) )assume A110:
k = 1
;
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
;
verum end;
hence
divset (
(T . i),
k)
= divset (
(T1 . i),
k)
by A104;
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 ;
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'];
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'];
( 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
;
( 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)
;
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 ( 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
;
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
;
verum
now ( 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
;
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
;
verum end;
hence
divset (
(T . i),
((len S01) + k))
= divset (
(T2 . i),
k)
by A113, A115, A123;
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 ;
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'];
( 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)
;
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;
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 ;
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'];
( 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)
;
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;
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 ;
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 for k being Nat st k in dom F2 holds
F . ((len F1) + k) = F2 . klet k be
Nat;
( k in dom F2 implies F . ((len F1) + k) = F2 . k )assume A148:
k in dom F2
;
F . ((len F1) + k) = F2 . kthen 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;
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;
verum end;
A157:
now for k being Nat st k in dom F1 holds
F . k = F1 . klet k be
Nat;
( k in dom F1 implies F . k = F1 . k )assume
k in dom F1
;
F . k = F1 . kthen 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;
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;
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;
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 ;
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;
verum
end;
now for i being 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
Nat;
(upper_sum ((f || ['a,b']),T)) . i = ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i)reconsider ii =
i as
Element of
NAT by ORDINAL1:def 12;
thus (upper_sum ((f || ['a,b']),T)) . i =
upper_sum (
(f || ['a,b']),
(T . ii))
by INTEGRA2:def 2
.=
(upper_sum ((f || ['a,c']),(T1 . ii))) + (Sum (upper_volume ((f || ['c,b']),(T2 . ii))))
by A164
.=
((upper_sum ((f || ['a,c']),T1)) . i) + (upper_sum ((f || ['c,b']),(T2 . ii)))
by INTEGRA2:def 2
.=
((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i)
by INTEGRA2:def 2
;
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;
A172:
now for e being Real st e > 0 holds
ex m being Nat st
for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < elet e be
Real;
( e > 0 implies ex m being Nat st
for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < e )assume A173:
e > 0
;
ex m being Nat st
for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < ethen consider m being
Nat such that A174:
for
n being
Nat st
m <= n holds
|.(((delta S2) . n) - 0).| < e / 2
by A168, XREAL_1:215;
take m =
m;
for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < eA175:
e / 2
< e
by A173, XREAL_1:216;
let nn be
Nat;
( m <= nn implies |.(((delta T2) . nn) - 0).| < e )assume A176:
m <= nn
;
|.(((delta T2) . nn) - 0).| < ereconsider n =
nn as
Element of
NAT by ORDINAL1:def 12;
|.(((delta S2) . n) - 0).| < e / 2
by A174, A176;
then
(
0 <= delta (S2 . n) &
|.(delta (S2 . n)).| < e / 2 )
by INTEGRA3:9, INTEGRA3:def 2;
then A177:
max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) < e / 2
by ABSVALUE:def 1;
A178:
for
y being
Real 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;
( 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)))
;
y < e
then consider x being
object such that A179:
x in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))
and A180:
y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) . x
by FUNCT_1:def 3;
reconsider i =
x as
Element of
NAT by A179;
A181:
x in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))))
by A179, FINSEQ_1:def 3;
consider E1 being
Division of
['c,b'] such that A182:
E1 = S2 . n
and A183:
2
<= len E1
by A30;
set i1 =
i + 1;
consider E being
Division of
['c,b'] such that A184:
E = S2 . n
and A185:
T2 . n = E /^ 1
by A38;
A186:
1
<= len E1
by A183, XXREAL_0:2;
then A187:
len D = (len E) - 1
by A184, A185, A182, RFINSEQ:def 1;
A188:
len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = len D
by INTEGRA1:def 6;
then A189:
dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = dom D
by FINSEQ_3:29;
A190:
now ( i = 1 implies y < e )
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E
by A184, INTEGRA1:def 6;
then
2
in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))))
by A184, A182, A183;
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 A191:
(upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2
< e / 2
by A177, XXREAL_0:2;
assume A192:
i = 1
;
y < ethen A193:
1
in dom D
by A181, A188, FINSEQ_1:def 3;
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1
by A184, A187, 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 A181, A192, 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 A194:
(upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1
< e / 2
by A177, XXREAL_0:2;
A195:
2
in dom E
by A184, A182, A183, FINSEQ_3:25;
1
in Seg (len E)
by A184, A182, A186;
then A196:
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 A197:
divset (
(S2 . n),1)
= [.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),1))).]
by A184, A196, INTEGRA1:def 4;
then A198:
[.(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;
A199:
divset (
(T2 . n),
i) =
[.(lower_bound (divset ((T2 . n),1))),(upper_bound (divset ((T2 . n),1))).]
by A192, INTEGRA1:4
.=
[.(lower_bound ['c,b']),(upper_bound (divset ((T2 . n),1))).]
by A193, INTEGRA1:def 4
.=
[.(lower_bound ['c,b']),(D . 1).]
by A193, INTEGRA1:def 4
.=
[.(lower_bound ['c,b']),(E . (1 + 1)).]
by A184, A185, A182, A186, A193, RFINSEQ:def 1
.=
[.(lower_bound ['c,b']),(upper_bound (divset ((S2 . n),2))).]
by A184, A195, 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 A200:
(
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 A199, INTEGRA1:5;
y = vol (divset ((T2 . n),1))
by A179, A180, A189, A192, 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 A192, A199, A200, A197;
then A201:
y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + (vol (divset ((S2 . n),1)))
by A197, A198, 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 A184, A195, INTEGRA1:def 4;
then A202:
divset (
(S2 . n),2)
= [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]
by A184, A196, 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 A202, A201, INTEGRA1:5;
then
y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + (vol (divset ((S2 . n),1)))
by A184, A195, 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 A184, A196, INTEGRA1:20;
then
y < (e / 2) + (e / 2)
by A191, A194, XREAL_1:8;
hence
y < e
;
verum end;
A203:
y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . n),i))))) * (vol (divset ((T2 . n),i)))
by A179, A180, A189, INTEGRA1:def 6;
now ( i <> 1 implies y < e )
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1
by A184, A187, 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 A204:
i + 1
in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))))
by A181, FINSEQ_1:60;
then A205:
i + 1
in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))
by FINSEQ_1:def 3;
A206:
i + 1
in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))
by A204, FINSEQ_1:def 3;
A207:
i in dom D
by A181, A188, FINSEQ_1:def 3;
Seg ((len D) + 1) = Seg (len E)
by A187;
then
i + 1
in Seg (len E)
by A181, A188, FINSEQ_1:60;
then A208:
i + 1
in dom E
by FINSEQ_1:def 3;
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E
by A184, INTEGRA1:def 6;
then A209:
dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = dom E
by FINSEQ_3:29;
assume A210:
i <> 1
;
y < e
i in Seg (len D)
by A179, A188, FINSEQ_1:def 3;
then
1
<= i
by FINSEQ_1:1;
then A211:
1
< i
by A210, XXREAL_0:1;
then A212:
i - 1
in Seg (len D)
by A181, A188, FINSEQ_3:12;
then A213:
i - 1
in dom D
by FINSEQ_1:def 3;
reconsider i9 =
i - 1 as
Element of
NAT by A212;
1
+ 1
< i + 1
by A211, XREAL_1:8;
then A214:
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 A210, A207, INTEGRA1:def 4
.=
[.(D . (i - 1)),(D . i).]
by A210, A207, INTEGRA1:def 4
.=
[.(E . (i9 + 1)),(D . i).]
by A184, A185, A182, A186, A213, RFINSEQ:def 1
.=
[.(E . ((i - 1) + 1)),(E . (i + 1)).]
by A184, A185, A182, A186, A207, RFINSEQ:def 1
.=
[.(E . ((i + 1) - 1)),(upper_bound (divset ((S2 . n),(i + 1)))).]
by A184, A214, A208, INTEGRA1:def 4
.=
[.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).]
by A184, A214, A208, 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 A203, A184, A205, A209, INTEGRA1:def 6;
then
y in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))
by A206, 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 A177, XXREAL_0:2;
hence
y < e
by A175, XXREAL_0:2;
verum end;
hence
y < e
by A190;
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 A178, INTEGRA3:9;
then
|.(delta (T2 . n)).| < e
by ABSVALUE:def 1;
hence
|.(((delta T2) . nn) - 0).| < e
by INTEGRA3:def 2;
verum end;
then A215:
delta T2 is convergent
by SEQ_2:def 6;
then A216:
lim (delta T2) = 0
by A172, SEQ_2:def 7;
then A217:
( upper_sum ((f || ['c,b']),T2) is convergent & lim (upper_sum ((f || ['c,b']),T2)) = upper_integral (f || ['c,b']) )
by A166, A18, A215, INTEGRA4:9;
A218:
now for e being Real st 0 < e holds
ex n being Nat st
for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < elet e be
Real;
( 0 < e implies ex n being Nat st
for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < e )assume A219:
0 < e
;
ex n being Nat st
for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < ethen consider n1 being
Nat such that A220:
for
m being
Nat st
n1 <= m holds
|.(((delta T1) . m) - 0).| < e
by A53, SEQ_2:def 7;
consider n2 being
Nat such that A221:
for
m being
Nat st
n2 <= m holds
|.(((delta T2) . m) - 0).| < e
by A172, A219;
reconsider n =
max (
n1,
n2) as
Nat by TARSKI:1;
take n =
n;
for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < elet mm be
Nat;
( n <= mm implies |.(((delta T) . mm) - 0).| < e )assume A222:
n <= mm
;
|.(((delta T) . mm) - 0).| < ereconsider m =
mm as
Element of
NAT by ORDINAL1:def 12;
n2 <= n
by XXREAL_0:25;
then
n2 <= m
by A222, XXREAL_0:2;
then
|.(((delta T2) . m) - 0).| < e
by A221;
then A223:
|.(delta (T2 . m)).| < e
by INTEGRA3:def 2;
0 <= delta (T2 . m)
by INTEGRA3:9;
then A224:
max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) < e
by A223, ABSVALUE:def 1;
n1 <= n
by XXREAL_0:25;
then
n1 <= m
by A222, XXREAL_0:2;
then
|.(((delta T1) . m) - 0).| < e
by A220;
then A225:
|.(delta (T1 . m)).| < e
by INTEGRA3:def 2;
0 <= delta (T1 . m)
by INTEGRA3:9;
then A226:
max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) < e
by A225, ABSVALUE:def 1;
A227:
for
r being
Real 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;
( 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)))
;
y < e
then consider x being
object such that A228:
x in dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))
and A229:
y = (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) . x
by FUNCT_1:def 3;
reconsider i =
x as
Element of
NAT by A228;
A230:
x in Seg (len (upper_volume ((chi (['a,b'],['a,b'])),(T . m))))
by A228, FINSEQ_1:def 3;
then A231:
1
<= i
by FINSEQ_1:1;
A232:
len (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = len Tm
by INTEGRA1:def 6;
then A233:
i <= len Tm
by A230, FINSEQ_1:1;
dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = dom Tm
by A232, FINSEQ_3:29;
then A234:
y = (upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((T . m),i))))) * (vol (divset ((T . m),i)))
by A228, A229, INTEGRA1:def 6;
consider S1 being
Division of
['a,c'],
S2 being
Division of
['c,b'] such that A235:
S1 = T1 . m
and A236:
S2 = T2 . m
and A237:
T . m = S1 ^ S2
by A93;
A238:
len Tm = (len S1) + (len S2)
by A237, FINSEQ_1:22;
per cases
( i <= len S1 or i > len S1 )
;
suppose
i <= len S1
;
y < ethen A239:
i in Seg (len S1)
by A231;
then A240:
i in dom S1
by FINSEQ_1:def 3;
len (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) = len S1
by A235, INTEGRA1:def 6;
then A241:
i in dom (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))
by A239, FINSEQ_1:def 3;
A242:
divset (
(T1 . m),
i)
= divset (
(T . m),
i)
by A95, A235, A239;
A243:
divset (
(T1 . m),
i)
c= ['a,c']
by A139, A235, A239;
then
divset (
(T1 . m),
i)
c= ['a,b']
by A137;
then
(chi (['a,c'],['a,c'])) | (divset ((T1 . m),i)) = (chi (['a,b'],['a,b'])) | (divset ((T . m),i))
by A242, A243, Th4;
then
y = (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) . i
by A234, A235, A240, A242, INTEGRA1:def 6;
then
y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))
by A241, 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 A226, XXREAL_0:2;
verum end; suppose
i > len S1
;
y < ethen A244:
(len S1) + 1
<= i
by NAT_1:13;
then consider k being
Nat such that A245:
((len S1) + 1) + k = i
by NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
set i1 = 1
+ k;
A246:
i - (len S1) <= len S2
by A238, A233, XREAL_1:20;
1
+ k = i - (len S1)
by A245;
then
1
<= 1
+ k
by A244, XREAL_1:19;
then A247:
1
+ k in Seg (len S2)
by A245, A246;
then A248:
1
+ k in dom S2
by FINSEQ_1:def 3;
A249:
divset (
(T2 . m),
(1 + k))
= divset (
(T . m),
((len S1) + (1 + k)))
by A112, A235, A236, A247;
A250:
divset (
(T2 . m),
(1 + k))
c= ['c,b']
by A134, A236, A247;
then
divset (
(T2 . m),
(1 + k))
c= ['a,b']
by A17;
then
y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k))))
by A234, A245, A249, A250, Th4;
then A251:
y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) . (1 + k)
by A236, A248, INTEGRA1:def 6;
len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) = len S2
by A236, INTEGRA1:def 6;
then
1
+ k in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))
by A247, FINSEQ_1:def 3;
then
y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))
by A251, 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 A224, XXREAL_0:2;
verum end;
end; A252:
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 A227;
then
|.(delta (T . m)).| < e
by A252, ABSVALUE:def 1;
hence
|.(((delta T) . mm) - 0).| < e
by INTEGRA3:def 2;
verum end;
then A253:
delta T is convergent
by SEQ_2:def 6;
then A254:
lim (delta T) = 0
by A218, SEQ_2:def 7;
(f || ['a,b']) | ['a,b'] is bounded
by A4;
then A255:
upper_integral (f || ['a,b']) = lim (upper_sum ((f || ['a,b']),T))
by A12, A253, A254, INTEGRA4:9;
A256:
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 ;
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 A257:
S1 = T1 . i
and A258:
S2 = T2 . i
and A259:
T . i = S1 ^ S2
by A93;
A260:
len F =
len S
by INTEGRA1:def 7
.=
(len S1) + (len S2)
by A259, FINSEQ_1:22
.=
(len F1) + (len S2)
by A257, INTEGRA1:def 7
;
then A261:
len F = (len F1) + (len F2)
by A258, INTEGRA1:def 7;
A262:
now for k being Nat st k in dom F2 holds
F . ((len F1) + k) = F2 . klet k be
Nat;
( k in dom F2 implies F . ((len F1) + k) = F2 . k )assume
k in dom F2
;
F . ((len F1) + k) = F2 . kthen A263:
k in Seg (len F2)
by FINSEQ_1:def 3;
then
1
<= k
by FINSEQ_1:1;
then A264:
1
+ (len F1) <= k + (len F1)
by XREAL_1:6;
k <= len F2
by A263, FINSEQ_1:1;
then A265:
(len F1) + k <= len F
by A261, XREAL_1:6;
1
<= 1
+ (len F1)
by NAT_1:11;
then
1
<= k + (len F1)
by A264, XXREAL_0:2;
then
k + (len F1) in Seg (len F)
by A265;
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 A266:
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;
A267:
k in Seg (len S2)
by A258, A263, INTEGRA1:def 7;
then A268:
k in dom S2
by FINSEQ_1:def 3;
len F1 = len S1
by A257, INTEGRA1:def 7;
then A269:
divset (
(T . i),
((len F1) + k))
= divset (
(T2 . i),
k)
by A112, A257, A258, A267;
A270:
divset (
(T2 . i),
k)
c= ['c,b']
by A134, A258, A267;
then
divset (
(T . i),
((len F1) + k))
c= ['a,b']
by A17, A269;
then
F . ((len F1) + k) = (lower_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k)))
by A266, A269, A270, Th3;
hence
F . ((len F1) + k) = F2 . k
by A258, A268, INTEGRA1:def 7;
verum end;
A271:
now for k being Nat st k in dom F1 holds
F . k = F1 . klet k be
Nat;
( k in dom F1 implies F . k = F1 . k )
len (lower_volume ((f || ['a,b']),(T . i))) = len S
by INTEGRA1:def 7;
then A272:
dom (lower_volume ((f || ['a,b']),(T . i))) = dom S
by FINSEQ_3:29;
assume A273:
k in dom F1
;
F . k = F1 . kthen
k in Seg (len F1)
by FINSEQ_1:def 3;
then A274:
k in Seg (len S1)
by A257, INTEGRA1:def 7;
then A275:
k in dom S1
by FINSEQ_1:def 3;
len F1 <= len F
by A260, NAT_1:11;
then
dom F1 c= dom F
by FINSEQ_3:30;
then A276:
F . k = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k)))
by A273, A272, INTEGRA1:def 7;
A277:
(
divset (
(T . i),
k)
= divset (
(T1 . i),
k) &
divset (
(T1 . i),
k)
c= ['a,c'] )
by A139, A95, A257, A274;
then
divset (
(T . i),
k)
c= ['a,b']
by A137;
then
F . k = (lower_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k)))
by A276, A277, Th3;
hence
F . k = F1 . k
by A257, A275, INTEGRA1:def 7;
verum end;
dom F = Seg ((len F1) + (len F2))
by A261, 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 A271, A262, FINSEQ_1:def 7;
verum
end;
A278:
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 ;
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 A256;
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;
verum
end;
now for i being 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
Nat;
(lower_sum ((f || ['a,b']),T)) . i = ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i)reconsider ii =
i as
Element of
NAT by ORDINAL1:def 12;
thus (lower_sum ((f || ['a,b']),T)) . i =
lower_sum (
(f || ['a,b']),
(T . ii))
by INTEGRA2:def 3
.=
(lower_sum ((f || ['a,c']),(T1 . ii))) + (Sum (lower_volume ((f || ['c,b']),(T2 . ii))))
by A278
.=
((lower_sum ((f || ['a,c']),T1)) . i) + (lower_sum ((f || ['c,b']),(T2 . ii)))
by INTEGRA2:def 3
.=
((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i)
by INTEGRA2:def 3
;
verum end;
then A279:
lower_sum ((f || ['a,b']),T) = (lower_sum ((f || ['a,c']),T1)) + (lower_sum ((f || ['c,b']),T2))
by SEQ_1:7;
A280:
f || ['a,c'] is Function of ['a,c'],REAL
by A2, A137, Lm1, XBOOLE_1:1;
then A281:
( f || ['a,c'] is upper_integrable & f || ['a,c'] is lower_integrable )
by A138, INTEGRA4:10;
A282:
( upper_sum ((f || ['a,c']),T1) is convergent & lim (upper_sum ((f || ['a,c']),T1)) = upper_integral (f || ['a,c']) )
by A280, A138, A53, INTEGRA4:9;
then A283:
(upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b'])
by A165, A217, A255, SEQ_2:6;
A284:
( lower_sum ((f || ['a,c']),T1) is convergent & lim (lower_sum ((f || ['a,c']),T1)) = lower_integral (f || ['a,c']) )
by A280, A138, A53, INTEGRA4:8;
(f || ['a,b']) | ['a,b'] is bounded
by A4;
then A285:
lower_integral (f || ['a,b']) = lim (lower_sum ((f || ['a,b']),T))
by A12, A253, A254, 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, A215, A216, INTEGRA4:8;
then A286:
(lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b'])
by A279, A284, A285, 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, A282, A217, A255, SEQ_2:6
;
hence
integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
by A58, A57; ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
f || ['a,b'] is integrable
by A3;
then A287:
upper_integral (f || ['a,b']) = lower_integral (f || ['a,b'])
;
A288:
( f || ['c,b'] is upper_integrable & f || ['c,b'] is lower_integrable )
by A166, A18, INTEGRA4:10;
A289:
lower_integral (f || ['a,c']) <= upper_integral (f || ['a,c'])
by A280, A138, INTEGRA1:49;
then
lower_integral (f || ['c,b']) = upper_integral (f || ['c,b'])
by A287, A283, A286, A167, Th1;
then A290:
f || ['c,b'] is integrable
by A288;
lower_integral (f || ['a,c']) = upper_integral (f || ['a,c'])
by A287, A283, A286, A289, A167, Th1;
then
f || ['a,c'] is integrable
by A281;
hence
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
by A290; verum