let x be Real; for A being closed-interval Subset of REAL
for D1, D2 being Division of A
for g being Function of A,REAL st x in divset D1,(len D1) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds
(Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
let A be closed-interval Subset of REAL ; for D1, D2 being Division of A
for g being Function of A,REAL st x in divset D1,(len D1) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds
(Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
let D1, D2 be Division of A; for g being Function of A,REAL st x in divset D1,(len D1) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds
(Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
let g be Function of A,REAL ; ( x in divset D1,(len D1) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded implies (Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )
assume that
A1:
x in divset D1,(len D1)
and
A2:
len D1 >= 2
; ( not D1 <= D2 or not rng D2 = (rng D1) \/ {x} or not g | A is bounded or (Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )
set j = len D1;
assume that
A3:
D1 <= D2
and
A4:
rng D2 = (rng D1) \/ {x}
; ( not g | A is bounded or (Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )
A5:
len D1 in dom D1
by FINSEQ_5:6;
then A6:
indx D2,D1,(len D1) in dom D2
by A3, INTEGRA1:def 21;
A7:
len D1 <> 1
by A2;
then reconsider j1 = (len D1) - 1 as Element of NAT by A5, INTEGRA1:9;
A8:
j1 in dom D1
by A5, A7, INTEGRA1:9;
then A9:
j1 <= len D1
by FINSEQ_3:27;
A10:
1 <= j1
by A8, FINSEQ_3:27;
then
mid D1,1,j1 is increasing
by A5, A7, INTEGRA1:9, INTEGRA1:37;
then A11:
D1 | j1 is increasing
by A10, JORDAN3:25;
A12:
(len D1) - 1 in dom D1
by A5, A7, INTEGRA1:9;
then A13:
indx D2,D1,j1 in dom D2
by A3, INTEGRA1:def 21;
then A14:
1 <= indx D2,D1,j1
by FINSEQ_3:27;
then
mid D2,1,(indx D2,D1,j1) is increasing
by A13, INTEGRA1:37;
then A15:
D2 | (indx D2,D1,j1) is increasing
by A14, JORDAN3:25;
A16:
indx D2,D1,j1 <= len D2
by A13, FINSEQ_3:27;
then A17:
len (D2 | (indx D2,D1,j1)) = indx D2,D1,j1
by FINSEQ_1:80;
A18:
rng (D2 | (indx D2,D1,j1)) = rng (D1 | j1)
by A1, A2, A3, A4, Lm6;
then A19:
D2 | (indx D2,D1,j1) = D1 | j1
by A15, A11, Th5;
A20:
for k being Element of NAT st 1 <= k & k <= j1 holds
k = indx D2,D1,k
proof
let k be
Element of
NAT ;
( 1 <= k & k <= j1 implies k = indx D2,D1,k )
assume that A21:
1
<= k
and A22:
k <= j1
;
k = indx D2,D1,k
assume A23:
k <> indx D2,
D1,
k
;
contradiction
per cases
( k > indx D2,D1,k or k < indx D2,D1,k )
by A23, XXREAL_0:1;
suppose A24:
k > indx D2,
D1,
k
;
contradiction
k <= len D1
by A9, A22, XXREAL_0:2;
then A25:
k in dom D1
by A21, FINSEQ_3:27;
then
indx D2,
D1,
k in dom D2
by A3, INTEGRA1:def 21;
then
indx D2,
D1,
k in Seg (len D2)
by FINSEQ_1:def 3;
then A26:
1
<= indx D2,
D1,
k
by FINSEQ_1:3;
A27:
indx D2,
D1,
k < j1
by A22, A24, XXREAL_0:2;
then A28:
indx D2,
D1,
k in Seg j1
by A26, FINSEQ_1:3;
indx D2,
D1,
k <= indx D2,
D1,
j1
by A3, A8, A22, A25, Th6;
then
indx D2,
D1,
k in Seg (indx D2,D1,j1)
by A26, FINSEQ_1:3;
then A29:
(D2 | (indx D2,D1,j1)) . (indx D2,D1,k) = D2 . (indx D2,D1,k)
by A13, RFINSEQ:19;
indx D2,
D1,
k <= len D1
by A9, A27, XXREAL_0:2;
then
indx D2,
D1,
k in dom D1
by A26, FINSEQ_3:27;
then A30:
D1 . k > D1 . (indx D2,D1,k)
by A24, A25, SEQM_3:def 1;
D1 . k = D2 . (indx D2,D1,k)
by A3, A25, INTEGRA1:def 21;
hence
contradiction
by A8, A19, A29, A30, A28, RFINSEQ:19;
verum end; suppose A31:
k < indx D2,
D1,
k
;
contradiction
k <= len D1
by A9, A22, XXREAL_0:2;
then A32:
k in dom D1
by A21, FINSEQ_3:27;
then
indx D2,
D1,
k <= indx D2,
D1,
j1
by A3, A8, A22, Th6;
then A33:
k <= indx D2,
D1,
j1
by A31, XXREAL_0:2;
then
k <= len D2
by A16, XXREAL_0:2;
then A34:
k in dom D2
by A21, FINSEQ_3:27;
k in Seg j1
by A21, A22, FINSEQ_1:3;
then A35:
D1 . k = (D1 | j1) . k
by A12, RFINSEQ:19;
indx D2,
D1,
k in dom D2
by A3, A32, INTEGRA1:def 21;
then A36:
D2 . k < D2 . (indx D2,D1,k)
by A31, A34, SEQM_3:def 1;
A37:
k in Seg (indx D2,D1,j1)
by A21, A33, FINSEQ_1:3;
D1 . k = D2 . (indx D2,D1,k)
by A3, A32, INTEGRA1:def 21;
hence
contradiction
by A13, A19, A35, A36, A37, RFINSEQ:19;
verum end;
end;
A38:
for k being Nat st 1 <= k & k <= len ((lower_volume g,D1) | j1) holds
((lower_volume g,D1) | j1) . k = ((lower_volume g,D2) | (indx D2,D1,j1)) . k
proof
indx D2,
D1,
j1 in Seg (len D2)
by A13, FINSEQ_1:def 3;
then
indx D2,
D1,
j1 in Seg (len (lower_volume g,D2))
by INTEGRA1:def 8;
then A39:
indx D2,
D1,
j1 in dom (lower_volume g,D2)
by FINSEQ_1:def 3;
let k be
Nat;
( 1 <= k & k <= len ((lower_volume g,D1) | j1) implies ((lower_volume g,D1) | j1) . k = ((lower_volume g,D2) | (indx D2,D1,j1)) . k )
assume that A40:
1
<= k
and A41:
k <= len ((lower_volume g,D1) | j1)
;
((lower_volume g,D1) | j1) . k = ((lower_volume g,D2) | (indx D2,D1,j1)) . k
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
A42:
len (lower_volume g,D1) = len D1
by INTEGRA1:def 8;
then A43:
k <= j1
by A9, A41, FINSEQ_1:80;
then
k <= len D1
by A9, XXREAL_0:2;
then
k in Seg (len D1)
by A40, FINSEQ_1:3;
then A44:
k in dom D1
by FINSEQ_1:def 3;
then A45:
indx D2,
D1,
k in dom D2
by A3, INTEGRA1:def 21;
A46:
k in Seg j1
by A40, A43, FINSEQ_1:3;
then
indx D2,
D1,
k in Seg j1
by A20, A40, A43;
then A47:
indx D2,
D1,
k in Seg (indx D2,D1,j1)
by A10, A20;
then
indx D2,
D1,
k <= indx D2,
D1,
j1
by FINSEQ_1:3;
then A48:
indx D2,
D1,
k <= len D2
by A16, XXREAL_0:2;
A49:
D1 . k = D2 . (indx D2,D1,k)
by A3, A44, INTEGRA1:def 21;
A50:
(
lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) &
upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) )
proof
per cases
( k = 1 or k <> 1 )
;
suppose A51:
k = 1
;
( lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) & upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) )then A52:
upper_bound (divset D1,k) = D1 . k
by A44, INTEGRA1:def 5;
A53:
lower_bound (divset D1,k) = lower_bound A
by A44, A51, INTEGRA1:def 5;
indx D2,
D1,
k = 1
by A10, A20, A51;
hence
(
lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) &
upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) )
by A45, A49, A53, A52, INTEGRA1:def 5;
verum end; suppose A54:
k <> 1
;
( lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) & upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) )then reconsider k1 =
k - 1 as
Element of
NAT by A44, INTEGRA1:9;
A55:
k - 1
in dom D1
by A44, A54, INTEGRA1:9;
then A56:
1
<= k1
by FINSEQ_3:27;
k <= k + 1
by NAT_1:11;
then
k1 <= k
by XREAL_1:22;
then A57:
k1 <= j1
by A43, XXREAL_0:2;
A58:
indx D2,
D1,
k <> 1
by A20, A40, A43, A54;
then A59:
lower_bound (divset D2,(indx D2,D1,k)) = D2 . ((indx D2,D1,k) - 1)
by A45, INTEGRA1:def 5;
A60:
upper_bound (divset D1,k) = D1 . k
by A44, A54, INTEGRA1:def 5;
A61:
lower_bound (divset D1,k) = D1 . (k - 1)
by A44, A54, INTEGRA1:def 5;
A62:
upper_bound (divset D2,(indx D2,D1,k)) = D2 . (indx D2,D1,k)
by A45, A58, INTEGRA1:def 5;
D2 . ((indx D2,D1,k) - 1) =
D2 . (k - 1)
by A20, A40, A43
.=
D2 . (indx D2,D1,k1)
by A20, A57, A56
;
hence
(
lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) &
upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) )
by A3, A44, A61, A60, A55, A59, A62, INTEGRA1:def 21;
verum end;
end;
divset D1,
k = [.(lower_bound (divset D1,k)),(upper_bound (divset D1,k)).]
by INTEGRA1:5;
then A63:
divset D1,
k = divset D2,
(indx D2,D1,k)
by A50, INTEGRA1:5;
j1 in Seg (len (lower_volume g,D1))
by A8, A42, FINSEQ_1:def 3;
then
j1 in dom (lower_volume g,D1)
by FINSEQ_1:def 3;
then A64:
((lower_volume g,D1) | j1) . k =
(lower_volume g,D1) . k
by A46, RFINSEQ:19
.=
(lower_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k)))
by A44, A63, INTEGRA1:def 8
;
1
<= indx D2,
D1,
k
by A20, A40, A43;
then A65:
indx D2,
D1,
k in dom D2
by A48, FINSEQ_3:27;
((lower_volume g,D2) | (indx D2,D1,j1)) . k =
((lower_volume g,D2) | (indx D2,D1,j1)) . (indx D2,D1,k)
by A20, A40, A43
.=
(lower_volume g,D2) . (indx D2,D1,k)
by A47, A39, RFINSEQ:19
.=
(lower_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k)))
by A65, INTEGRA1:def 8
;
hence
((lower_volume g,D1) | j1) . k = ((lower_volume g,D2) | (indx D2,D1,j1)) . k
by A64;
verum
end;
A66:
len D2 in dom D2
by FINSEQ_5:6;
deffunc H1( Division of A) -> FinSequence of REAL = lower_volume g,$1;
deffunc H2( Division of A, Nat) -> Element of REAL = (PartSums (lower_volume g,$1)) . $2;
A67:
len D1 >= len (lower_volume g,D1)
by INTEGRA1:def 8;
A68:
len D1 <= len H1(D1)
by INTEGRA1:def 8;
A69:
len D1 in Seg (len D1)
by FINSEQ_1:5;
then A70:
1 <= len D1
by FINSEQ_1:3;
then A71:
len D1 in dom H1(D1)
by A68, FINSEQ_3:27;
assume A72:
g | A is bounded
; (Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
len D1 < (len D1) + 1
by NAT_1:13;
then A73:
j1 < len D1
by XREAL_1:21;
then
j1 < len H1(D1)
by INTEGRA1:def 8;
then
j1 in dom H1(D1)
by A10, FINSEQ_3:27;
then
H2(D1,j1) = Sum (H1(D1) | j1)
by INTEGRA1:def 22;
then H2(D1,j1) + (Sum (mid H1(D1),(len D1),(len D1))) =
Sum ((H1(D1) | j1) ^ (mid H1(D1),(len D1),(len D1)))
by RVSUM_1:105
.=
Sum ((mid H1(D1),1,j1) ^ (mid H1(D1),(j1 + 1),(len D1)))
by A10, JORDAN3:25
.=
Sum (mid H1(D1),1,(len D1))
by A10, A68, A73, INTEGRA2:4
.=
Sum (H1(D1) | (len D1))
by A70, JORDAN3:25
;
then A74:
H2(D1,j1) + (Sum (mid (lower_volume g,D1),(len D1),(len D1))) = H2(D1, len D1)
by A71, INTEGRA1:def 22;
A75:
indx D2,D1,(len D1) in dom D2
by A3, A5, INTEGRA1:def 21;
then A76:
indx D2,D1,(len D1) in Seg (len D2)
by FINSEQ_1:def 3;
then A77:
1 <= indx D2,D1,(len D1)
by FINSEQ_1:3;
len D1 < (len D1) + 1
by NAT_1:13;
then
j1 < len D1
by XREAL_1:21;
then A78:
indx D2,D1,j1 < indx D2,D1,(len D1)
by A3, A5, A8, Th7;
then A79:
(indx D2,D1,j1) + 1 <= indx D2,D1,(len D1)
by NAT_1:13;
A80:
j1 in dom D1
by A5, A7, INTEGRA1:9;
A81:
(Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid (lower_volume g,D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
proof
A82:
(indx D2,D1,(len D1)) - (indx D2,D1,j1) <= 2
proof
set ID1 =
(indx D2,D1,j1) + 1;
set ID2 =
((indx D2,D1,j1) + 1) + 1;
assume
(indx D2,D1,(len D1)) - (indx D2,D1,j1) > 2
;
contradiction
then A83:
(indx D2,D1,j1) + (1 + 1) < indx D2,
D1,
(len D1)
by XREAL_1:22;
A84:
(indx D2,D1,j1) + 1
< ((indx D2,D1,j1) + 1) + 1
by NAT_1:13;
then
indx D2,
D1,
j1 <= ((indx D2,D1,j1) + 1) + 1
by NAT_1:13;
then A85:
1
<= ((indx D2,D1,j1) + 1) + 1
by A14, XXREAL_0:2;
A86:
indx D2,
D1,
(len D1) in dom D2
by A3, A5, INTEGRA1:def 21;
then A87:
indx D2,
D1,
(len D1) <= len D2
by FINSEQ_3:27;
then
((indx D2,D1,j1) + 1) + 1
<= len D2
by A83, XXREAL_0:2;
then A88:
((indx D2,D1,j1) + 1) + 1
in dom D2
by A85, FINSEQ_3:27;
then A89:
D2 . (((indx D2,D1,j1) + 1) + 1) < D2 . (indx D2,D1,(len D1))
by A83, A86, SEQM_3:def 1;
A90:
1
<= (indx D2,D1,j1) + 1
by A14, NAT_1:13;
A91:
D1 . j1 = D2 . (indx D2,D1,j1)
by A3, A8, INTEGRA1:def 21;
(indx D2,D1,j1) + 1
<= indx D2,
D1,
(len D1)
by A83, A84, XXREAL_0:2;
then
(indx D2,D1,j1) + 1
<= len D2
by A87, XXREAL_0:2;
then A92:
(indx D2,D1,j1) + 1
in dom D2
by A90, FINSEQ_3:27;
A93:
D1 . (len D1) = D2 . (indx D2,D1,(len D1))
by A3, A5, INTEGRA1:def 21;
indx D2,
D1,
j1 < (indx D2,D1,j1) + 1
by NAT_1:13;
then A94:
D2 . (indx D2,D1,j1) < D2 . ((indx D2,D1,j1) + 1)
by A13, A92, SEQM_3:def 1;
A95:
D2 . ((indx D2,D1,j1) + 1) < D2 . (((indx D2,D1,j1) + 1) + 1)
by A84, A92, A88, SEQM_3:def 1;
A96:
( not
D2 . ((indx D2,D1,j1) + 1) in rng D1 & not
D2 . (((indx D2,D1,j1) + 1) + 1) in rng D1 )
proof
assume A97:
(
D2 . ((indx D2,D1,j1) + 1) in rng D1 or
D2 . (((indx D2,D1,j1) + 1) + 1) in rng D1 )
;
contradiction
per cases
( D2 . ((indx D2,D1,j1) + 1) in rng D1 or D2 . (((indx D2,D1,j1) + 1) + 1) in rng D1 )
by A97;
suppose
D2 . ((indx D2,D1,j1) + 1) in rng D1
;
contradictionthen consider n being
Element of
NAT such that A98:
n in dom D1
and A99:
D1 . n = D2 . ((indx D2,D1,j1) + 1)
by PARTFUN1:26;
j1 < n
by A80, A94, A91, A98, A99, GOBOARD2:18;
then A100:
len D1 < n + 1
by XREAL_1:21;
D2 . ((indx D2,D1,j1) + 1) < D2 . (indx D2,D1,(len D1))
by A95, A89, XXREAL_0:2;
then
n < len D1
by A5, A93, A98, A99, GOBOARD2:18;
hence
contradiction
by A100, NAT_1:13;
verum end; suppose
D2 . (((indx D2,D1,j1) + 1) + 1) in rng D1
;
contradictionthen consider n being
Element of
NAT such that A101:
n in dom D1
and A102:
D1 . n = D2 . (((indx D2,D1,j1) + 1) + 1)
by PARTFUN1:26;
D2 . (indx D2,D1,j1) < D2 . (((indx D2,D1,j1) + 1) + 1)
by A94, A95, XXREAL_0:2;
then
j1 < n
by A8, A91, A101, A102, GOBOARD2:18;
then A103:
len D1 < n + 1
by XREAL_1:21;
n < len D1
by A5, A89, A93, A101, A102, GOBOARD2:18;
hence
contradiction
by A103, NAT_1:13;
verum end;
end;
D2 . ((indx D2,D1,j1) + 1) in rng D2
by A92, FUNCT_1:def 5;
then
D2 . ((indx D2,D1,j1) + 1) in {x}
by A4, A96, XBOOLE_0:def 3;
then A104:
D2 . ((indx D2,D1,j1) + 1) = x
by TARSKI:def 1;
D2 . (((indx D2,D1,j1) + 1) + 1) in rng D2
by A88, FUNCT_1:def 5;
then
D2 . (((indx D2,D1,j1) + 1) + 1) in {x}
by A4, A96, XBOOLE_0:def 3;
then
D2 . ((indx D2,D1,j1) + 1) = D2 . (((indx D2,D1,j1) + 1) + 1)
by A104, TARSKI:def 1;
hence
contradiction
by A84, A92, A88, GOBOARD2:19;
verum
end;
A105:
len D1 <= len (lower_volume g,D1)
by INTEGRA1:def 8;
A106:
1
<= len D1
by A69, FINSEQ_1:3;
then A107:
(mid (lower_volume g,D1),(len D1),(len D1)) . 1
= (lower_volume g,D1) . (len D1)
by A105, JORDAN3:27;
((len D1) -' (len D1)) + 1
= 1
by Lm1;
then
len (mid (lower_volume g,D1),(len D1),(len D1)) = 1
by A106, A105, JORDAN3:27;
then A108:
mid (lower_volume g,D1),
(len D1),
(len D1) = <*((lower_volume g,D1) . (len D1))*>
by A107, FINSEQ_1:57;
A109:
1
<= (indx D2,D1,j1) + 1
by A14, NAT_1:13;
indx D2,
D1,
(len D1) in dom D2
by A3, A5, INTEGRA1:def 21;
then A110:
indx D2,
D1,
(len D1) in Seg (len D2)
by FINSEQ_1:def 3;
then A111:
1
<= indx D2,
D1,
(len D1)
by FINSEQ_1:3;
indx D2,
D1,
(len D1) in Seg (len (lower_volume g,D2))
by A110, INTEGRA1:def 8;
then A112:
indx D2,
D1,
(len D1) <= len (lower_volume g,D2)
by FINSEQ_1:3;
then A113:
(indx D2,D1,j1) + 1
<= len (lower_volume g,D2)
by A79, XXREAL_0:2;
then
(indx D2,D1,j1) + 1
in Seg (len (lower_volume g,D2))
by A109, FINSEQ_1:3;
then A114:
(indx D2,D1,j1) + 1
in Seg (len D2)
by INTEGRA1:def 8;
(indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1) = (indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)
by A79, XREAL_1:235;
then
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1
<= 2
by A82;
then A115:
len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) <= 2
by A79, A111, A112, A109, A113, JORDAN3:27;
len (lower_volume g,D2) = len D2
by INTEGRA1:def 8;
then A116:
(indx D2,D1,j1) + 1
in dom D2
by A109, A113, FINSEQ_3:27;
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1
>= 0 + 1
by XREAL_1:8;
then A117:
1
<= len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))
by A79, A111, A112, A109, A113, JORDAN3:27;
now per cases
( len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) = 1 or len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) = 2 )
by A117, A115, Lm2;
suppose A118:
len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) = 1
;
(Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid (lower_volume g,D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
upper_bound (divset D1,(len D1)) = D1 . (len D1)
by A5, A7, INTEGRA1:def 5;
then A119:
upper_bound (divset D1,(len D1)) = D2 . (indx D2,D1,(len D1))
by A3, A5, INTEGRA1:def 21;
lower_bound (divset D1,(len D1)) = D1 . j1
by A5, A7, INTEGRA1:def 5;
then
lower_bound (divset D1,(len D1)) = D2 . (indx D2,D1,j1)
by A3, A8, INTEGRA1:def 21;
then A120:
divset D1,
(len D1) = [.(D2 . (indx D2,D1,j1)),(D2 . (indx D2,D1,(len D1))).]
by A119, INTEGRA1:5;
A121:
delta D1 >= 0
by Th8;
A122:
(upper_bound (rng g)) - (lower_bound (rng g)) >= 0
by A72, Lm3, XREAL_1:50;
A123:
indx D2,
D1,
(len D1) in dom D2
by A3, A5, INTEGRA1:def 21;
len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) = ((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1
by A79, A111, A112, A109, A113, JORDAN3:27;
then A124:
(indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1) = 0
by A79, A118, XREAL_1:235;
then
indx D2,
D1,
(len D1) <> 1
by A13, FINSEQ_3:27;
then A125:
upper_bound (divset D2,(indx D2,D1,(len D1))) = D2 . (indx D2,D1,(len D1))
by A123, INTEGRA1:def 5;
lower_bound (divset D2,(indx D2,D1,(len D1))) = D2 . ((indx D2,D1,(len D1)) - 1)
by A14, A124, A123, INTEGRA1:def 5;
then A126:
divset D2,
(indx D2,D1,(len D1)) = divset D1,
(len D1)
by A124, A120, A125, INTEGRA1:5;
(mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) . 1
= (lower_volume g,D2) . ((indx D2,D1,j1) + 1)
by A111, A112, A109, A113, JORDAN3:27;
then
mid (lower_volume g,D2),
((indx D2,D1,j1) + 1),
(indx D2,D1,(len D1)) = <*((lower_volume g,D2) . ((indx D2,D1,j1) + 1))*>
by A118, FINSEQ_1:57;
then Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) =
(lower_volume g,D2) . ((indx D2,D1,j1) + 1)
by FINSOP_1:12
.=
(lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))
by A116, INTEGRA1:def 8
.=
(lower_volume g,D1) . (len D1)
by A5, A124, A126, INTEGRA1:def 8
.=
Sum (mid (lower_volume g,D1),(len D1),(len D1))
by A108, FINSOP_1:12
;
hence
(Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid (lower_volume g,D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A121, A122;
verum end; suppose A127:
len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) = 2
;
(Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid (lower_volume g,D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)A128:
(mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) . 1
= (lower_volume g,D2) . ((indx D2,D1,j1) + 1)
by A111, A112, A109, A113, JORDAN3:27;
A129:
2
+ ((indx D2,D1,j1) + 1) >= 0 + 1
by XREAL_1:9;
(mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) . 2 =
H1(
D2)
. ((2 + ((indx D2,D1,j1) + 1)) -' 1)
by A79, A111, A112, A109, A113, A127, JORDAN3:27
.=
H1(
D2)
. ((2 + ((indx D2,D1,j1) + 1)) - 1)
by A129, XREAL_1:235
.=
H1(
D2)
. ((indx D2,D1,j1) + (1 + 1))
;
then
mid (lower_volume g,D2),
((indx D2,D1,j1) + 1),
(indx D2,D1,(len D1)) = <*((lower_volume g,D2) . ((indx D2,D1,j1) + 1)),((lower_volume g,D2) . ((indx D2,D1,j1) + 2))*>
by A127, A128, FINSEQ_1:61;
then A130:
Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) = ((lower_volume g,D2) . ((indx D2,D1,j1) + 1)) + ((lower_volume g,D2) . ((indx D2,D1,j1) + 2))
by RVSUM_1:107;
A131:
vol (divset D2,((indx D2,D1,j1) + 1)) >= 0
by INTEGRA1:11;
upper_bound (divset D1,(len D1)) = D1 . (len D1)
by A5, A7, INTEGRA1:def 5;
then A132:
upper_bound (divset D1,(len D1)) = D2 . (indx D2,D1,(len D1))
by A3, A5, INTEGRA1:def 21;
A133:
vol (divset D2,((indx D2,D1,j1) + 2)) >= 0
by INTEGRA1:11;
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1
= 2
by A79, A111, A112, A109, A113, A127, JORDAN3:27;
then A134:
((indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)) + 1
= 2
by A79, XREAL_1:235;
then A135:
(indx D2,D1,j1) + 2
in dom D2
by A3, A5, INTEGRA1:def 21;
lower_bound (divset D1,(len D1)) = D1 . j1
by A5, A7, INTEGRA1:def 5;
then
lower_bound (divset D1,(len D1)) = D2 . (indx D2,D1,j1)
by A3, A8, INTEGRA1:def 21;
then A136:
vol (divset D1,(len D1)) = (((D2 . ((indx D2,D1,j1) + 2)) - (D2 . ((indx D2,D1,j1) + 1))) + (D2 . ((indx D2,D1,j1) + 1))) - (D2 . (indx D2,D1,j1))
by A132, A134, INTEGRA1:def 6;
(indx D2,D1,j1) + 1
in Seg (len (lower_volume g,D2))
by A109, A113, FINSEQ_1:3;
then
(indx D2,D1,j1) + 1
in Seg (len D2)
by INTEGRA1:def 8;
then A137:
(indx D2,D1,j1) + 1
in dom D2
by FINSEQ_1:def 3;
A138:
(indx D2,D1,j1) + 1
<> 1
by A14, NAT_1:13;
then A139:
upper_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . ((indx D2,D1,j1) + 1)
by A137, INTEGRA1:def 5;
((indx D2,D1,j1) + 1) - 1
= (indx D2,D1,j1) + 0
;
then A140:
lower_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . (indx D2,D1,j1)
by A137, A138, INTEGRA1:def 5;
A141:
((indx D2,D1,j1) + 1) + 1
> 1
by A109, NAT_1:13;
((indx D2,D1,j1) + 2) - 1
= (indx D2,D1,j1) + 1
;
then A142:
lower_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 1)
by A135, A141, INTEGRA1:def 5;
upper_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 2)
by A135, A141, INTEGRA1:def 5;
then vol (divset D1,(len D1)) =
((vol (divset D2,((indx D2,D1,j1) + 2))) + (D2 . ((indx D2,D1,j1) + 1))) - (D2 . (indx D2,D1,j1))
by A142, A136, INTEGRA1:def 6
.=
(vol (divset D2,((indx D2,D1,j1) + 2))) + ((upper_bound (divset D2,((indx D2,D1,j1) + 1))) - (lower_bound (divset D2,((indx D2,D1,j1) + 1))))
by A140, A139
;
then A143:
vol (divset D1,(len D1)) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2)))
by INTEGRA1:def 6;
then A144:
(lower_volume g,D1) . (len D1) = (lower_bound (rng (g | (divset D1,(len D1))))) * ((vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2))))
by A5, INTEGRA1:def 8;
A145:
(Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid H1(D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * ((vol (divset D2,((indx D2,D1,j1) + 2))) + (vol (divset D2,((indx D2,D1,j1) + 1))))
proof
set ID1 =
(indx D2,D1,j1) + 1;
set ID2 =
(indx D2,D1,j1) + 2;
set IR =
(lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)));
divset D1,
(len D1) c= A
by A5, INTEGRA1:10;
then A146:
lower_bound (rng (g | (divset D1,(len D1)))) >= lower_bound (rng g)
by A72, Lm4;
Sum (mid H1(D1),(len D1),(len D1)) = ((lower_bound (rng (g | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((lower_bound (rng (g | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))))
by A108, A144, FINSOP_1:12;
then
(Sum (mid H1(D1),(len D1),(len D1))) - ((lower_bound (rng (g | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) >= (lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))
by A133, A146, XREAL_1:66;
then
Sum (mid H1(D1),(len D1),(len D1)) >= ((lower_bound (rng (g | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) + ((lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2))))
by XREAL_1:21;
then A147:
(Sum (mid H1(D1),(len D1),(len D1))) - ((lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) >= (lower_bound (rng (g | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))
by XREAL_1:21;
(lower_bound (rng (g | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) >= (lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1)))
by A131, A146, XREAL_1:66;
then
(Sum (mid H1(D1),(len D1),(len D1))) - ((lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) >= (lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1)))
by A147, XXREAL_0:2;
then A148:
Sum (mid H1(D1),(len D1),(len D1)) >= ((lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1))))
by XREAL_1:21;
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1
= 2
by A79, A111, A112, A109, A113, A127, JORDAN3:27;
then A149:
((indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)) + 1
= 2
by A79, XREAL_1:235;
(indx D2,D1,j1) + 1
in dom D2
by A114, FINSEQ_1:def 3;
then
divset D2,
((indx D2,D1,j1) + 1) c= A
by INTEGRA1:10;
then
lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1)))) <= upper_bound (rng g)
by A72, Lm4;
then A150:
(lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) <= (upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1)))
by A131, XREAL_1:66;
A151:
indx D2,
D1,
(len D1) in dom D2
by A3, A5, INTEGRA1:def 21;
then
divset D2,
((indx D2,D1,j1) + 2) c= A
by A149, INTEGRA1:10;
then A152:
lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 2)))) <= upper_bound (rng g)
by A72, Lm4;
Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) =
((lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 2))))) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + (H1(D2) . ((indx D2,D1,j1) + 1))
by A130, A151, A149, INTEGRA1:def 8
.=
((lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 2))))) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))))
by A116, INTEGRA1:def 8
;
then
(Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - ((lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) <= (upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))
by A133, A152, XREAL_1:66;
then
Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) <= ((upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))))
by XREAL_1:22;
then
(Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - ((upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) <= (lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))
by XREAL_1:22;
then
(Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - ((upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) <= (upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1)))
by A150, XXREAL_0:2;
then
Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) <= ((upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1))))
by XREAL_1:22;
then
(Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid H1(D1),(len D1),(len D1))) <= (((upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1))))) - (((lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1)))))
by A148, XREAL_1:15;
hence
(Sum (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid H1(D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * ((vol (divset D2,((indx D2,D1,j1) + 2))) + (vol (divset D2,((indx D2,D1,j1) + 1))))
;
verum
end;
(upper_bound (rng g)) - (lower_bound (rng g)) >= 0
by A72, Lm3, XREAL_1:50;
then
((upper_bound (rng g)) - (lower_bound (rng g))) * (vol (divset D1,(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A5, Lm5, XREAL_1:66;
hence
(Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid (lower_volume g,D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A143, A145, XXREAL_0:2;
verum end;
hence
(Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) - (Sum (mid (lower_volume g,D1),(len D1),(len D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
;
verum
end;
indx D2,D1,j1 in dom D2
by A3, A12, INTEGRA1:def 21;
then
indx D2,D1,j1 <= len D2
by FINSEQ_3:27;
then A153:
indx D2,D1,j1 <= len (lower_volume g,D2)
by INTEGRA1:def 8;
j1 <= len D1
by A12, FINSEQ_3:27;
then A154:
j1 <= len (lower_volume g,D1)
by INTEGRA1:def 8;
A155:
D2 . (indx D2,D1,(len D1)) = D1 . (len D1)
by A3, A5, INTEGRA1:def 21;
A156:
indx D2,D1,(len D1) >= len (lower_volume g,D2)
proof
assume
indx D2,
D1,
(len D1) < len (lower_volume g,D2)
;
contradiction
then
indx D2,
D1,
(len D1) < len D2
by INTEGRA1:def 8;
then A157:
D1 . (len D1) < D2 . (len D2)
by A66, A6, A155, SEQM_3:def 1;
A158:
not
D2 . (len D2) in rng D1
D2 . (len D2) in rng D2
by A66, FUNCT_1:def 5;
then
(
D2 . (len D2) in rng D1 or
D2 . (len D2) in {x} )
by A4, XBOOLE_0:def 3;
then
D2 . (len D2) = x
by A158, TARSKI:def 1;
then
D2 . (len D2) <= upper_bound (divset D1,(len D1))
by A1, INTEGRA2:1;
hence
contradiction
by A5, A7, A157, INTEGRA1:def 5;
verum
end;
indx D2,D1,(len D1) in Seg (len D2)
by A6, FINSEQ_1:def 3;
then
indx D2,D1,(len D1) in Seg (len (lower_volume g,D2))
by INTEGRA1:def 8;
then
indx D2,D1,(len D1) in dom (lower_volume g,D2)
by FINSEQ_1:def 3;
then A159: H2(D2, indx D2,D1,(len D1)) =
Sum ((lower_volume g,D2) | (indx D2,D1,(len D1)))
by INTEGRA1:def 22
.=
Sum (lower_volume g,D2)
by A156, FINSEQ_1:79
;
len D1 in Seg (len (lower_volume g,D1))
by A69, INTEGRA1:def 8;
then
len D1 in dom (lower_volume g,D1)
by FINSEQ_1:def 3;
then A160: H2(D1, len D1) =
Sum ((lower_volume g,D1) | (len D1))
by INTEGRA1:def 22
.=
Sum (lower_volume g,D1)
by A67, FINSEQ_1:79
;
len D1 = len (lower_volume g,D1)
by INTEGRA1:def 8;
then A161:
j1 in dom (lower_volume g,D1)
by A8, FINSEQ_3:31;
len (D2 | (indx D2,D1,j1)) = len (D1 | j1)
by A15, A11, A18, Th5;
then
indx D2,D1,j1 = j1
by A9, A17, FINSEQ_1:80;
then
len ((lower_volume g,D1) | j1) = indx D2,D1,j1
by A154, FINSEQ_1:80;
then
len ((lower_volume g,D1) | j1) = len ((lower_volume g,D2) | (indx D2,D1,j1))
by A153, FINSEQ_1:80;
then A162:
(lower_volume g,D2) | (indx D2,D1,j1) = (lower_volume g,D1) | j1
by A38, FINSEQ_1:18;
len D2 = len (lower_volume g,D2)
by INTEGRA1:def 8;
then
indx D2,D1,j1 in dom (lower_volume g,D2)
by A13, FINSEQ_3:31;
then A163: H2(D2, indx D2,D1,j1) =
Sum ((lower_volume g,D2) | (indx D2,D1,j1))
by INTEGRA1:def 22
.=
H2(D1,j1)
by A162, A161, INTEGRA1:def 22
;
indx D2,D1,(len D1) <= len D2
by A76, FINSEQ_1:3;
then A164:
indx D2,D1,(len D1) <= len H1(D2)
by INTEGRA1:def 8;
A165:
len D2 = len H1(D2)
by INTEGRA1:def 8;
then A166:
indx D2,D1,(len D1) in dom H1(D2)
by A75, FINSEQ_3:31;
indx D2,D1,j1 in dom H1(D2)
by A13, A165, FINSEQ_3:31;
then
H2(D2, indx D2,D1,j1) = Sum (H1(D2) | (indx D2,D1,j1))
by INTEGRA1:def 22;
then H2(D2, indx D2,D1,j1) + (Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) =
Sum ((H1(D2) | (indx D2,D1,j1)) ^ (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))))
by RVSUM_1:105
.=
Sum ((mid H1(D2),1,(indx D2,D1,j1)) ^ (mid H1(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))))
by A14, JORDAN3:25
.=
Sum (mid H1(D2),1,(indx D2,D1,(len D1)))
by A14, A78, A164, INTEGRA2:4
.=
Sum (H1(D2) | (indx D2,D1,(len D1)))
by A77, JORDAN3:25
;
then
H2(D2, indx D2,D1,j1) + (Sum (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) = H2(D2, indx D2,D1,(len D1))
by A166, INTEGRA1:def 22;
hence
(Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A163, A81, A74, A159, A160; verum