let A be non empty closed_interval Subset of REAL; for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds
for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
let D1, D2 be Division of A; for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds
for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
let f be Function of A,REAL; ( D1 <= D2 & f | A is bounded_above implies for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i))) )
assume that
A1:
D1 <= D2
and
A2:
f | A is bounded_above
; for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
for i being non zero Nat st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
proof
defpred S1[
Nat]
means ( $1
in dom D1 implies
Sum ((upper_volume (f,D1)) | $1) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,$1))) );
A3:
S1[1]
proof
reconsider g =
f | (divset (D1,1)) as
PartFunc of
(divset (D1,1)),
REAL by PARTFUN1:10;
set B =
divset (
D1,1);
set DD1 =
mid (
D1,1,1);
A4:
dom g = (dom f) /\ (divset (D1,1))
by RELAT_1:61;
assume A5:
1
in dom D1
;
Sum ((upper_volume (f,D1)) | 1) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,1)))
then A6:
D1 . 1
= upper_bound (divset (D1,1))
by Def3;
then A7:
D2 . (indx (D2,D1,1)) = upper_bound (divset (D1,1))
by A1, A5, Def18;
D1 . 1
>= lower_bound (divset (D1,1))
by A6, SEQ_4:11;
then reconsider DD1 =
mid (
D1,1,1) as
Division of
divset (
D1,1)
by A5, A6, Th35;
1
in Seg (len D1)
by A5, FINSEQ_1:def 3;
then A8:
1
<= len D1
by FINSEQ_1:1;
then A9:
len (mid (D1,1,1)) = (1 -' 1) + 1
by FINSEQ_6:118;
A10:
len (upper_volume (g,DD1)) =
len DD1
by Def5
.=
1
by A9, XREAL_1:235
;
A11:
len (mid (D1,1,1)) = 1
by A9, XREAL_1:235;
then A12:
len (mid (D1,1,1)) = len (D1 | 1)
;
for
k being
Nat st 1
<= k &
k <= len (mid (D1,1,1)) holds
(mid (D1,1,1)) . k = (D1 | 1) . k
proof
let k be
Nat;
( 1 <= k & k <= len (mid (D1,1,1)) implies (mid (D1,1,1)) . k = (D1 | 1) . k )
assume that A13:
1
<= k
and A14:
k <= len (mid (D1,1,1))
;
(mid (D1,1,1)) . k = (D1 | 1) . k
k in Seg (len (D1 | 1))
by A12, A13, A14, FINSEQ_1:1;
then
k in dom (D1 | 1)
by FINSEQ_1:def 3;
then
k in dom (D1 | (Seg 1))
by FINSEQ_1:def 15;
then A15:
(D1 | (Seg 1)) . k = D1 . k
by FUNCT_1:47;
A16:
k = 1
by A11, A13, A14, XXREAL_0:1;
then
(mid (D1,1,1)) . k = D1 . ((1 + 1) - 1)
by A8, FINSEQ_6:118;
hence
(mid (D1,1,1)) . k = (D1 | 1) . k
by A16, A15, FINSEQ_1:def 15;
verum
end;
then A17:
mid (
D1,1,1)
= D1 | 1
by A12, FINSEQ_1:14;
A18:
for
i being
Nat st 1
<= i &
i <= len (upper_volume (g,DD1)) holds
(upper_volume (g,DD1)) . i = ((upper_volume (f,D1)) | 1) . i
proof
let i be
Nat;
( 1 <= i & i <= len (upper_volume (g,DD1)) implies (upper_volume (g,DD1)) . i = ((upper_volume (f,D1)) | 1) . i )
assume that A19:
1
<= i
and A20:
i <= len (upper_volume (g,DD1))
;
(upper_volume (g,DD1)) . i = ((upper_volume (f,D1)) | 1) . i
A21:
1
in Seg 1
by FINSEQ_1:3;
dom (D1 | (Seg 1)) = (dom D1) /\ (Seg 1)
by RELAT_1:61;
then A22:
1
in dom (D1 | (Seg 1))
by A5, A21, XBOOLE_0:def 4;
dom (upper_volume (f,D1)) =
Seg (len (upper_volume (f,D1)))
by FINSEQ_1:def 3
.=
Seg (len D1)
by Def5
;
then A23:
dom ((upper_volume (f,D1)) | (Seg 1)) =
(Seg (len D1)) /\ (Seg 1)
by RELAT_1:61
.=
Seg 1
by A8, FINSEQ_1:7
;
len DD1 = 1
by A9, XREAL_1:235;
then A24:
1
in dom DD1
by A21, FINSEQ_1:def 3;
A25:
((upper_volume (f,D1)) | 1) . i =
((upper_volume (f,D1)) | (Seg 1)) . i
by FINSEQ_1:def 15
.=
((upper_volume (f,D1)) | (Seg 1)) . 1
by A10, A19, A20, XXREAL_0:1
.=
(upper_volume (f,D1)) . 1
by A23, FINSEQ_1:3, FUNCT_1:47
.=
(upper_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1)))
by A5, Def5
;
A26:
divset (
D1,1) =
[.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
by Th2
.=
[.(lower_bound A),(upper_bound (divset (D1,1))).]
by A5, Def3
.=
[.(lower_bound A),(D1 . 1).]
by A5, Def3
;
A27:
(upper_volume (g,DD1)) . i =
(upper_volume (g,DD1)) . 1
by A10, A19, A20, XXREAL_0:1
.=
(upper_bound (rng (g | (divset (DD1,1))))) * (vol (divset (DD1,1)))
by A24, Def5
;
divset (
DD1,1) =
[.(lower_bound (divset (DD1,1))),(upper_bound (divset (DD1,1))).]
by Th2
.=
[.(lower_bound (divset (D1,1))),(upper_bound (divset (DD1,1))).]
by A24, Def3
.=
[.(lower_bound (divset (D1,1))),(DD1 . 1).]
by A24, Def3
.=
[.(lower_bound A),((D1 | 1) . 1).]
by A5, A17, Def3
.=
[.(lower_bound A),((D1 | (Seg 1)) . 1).]
by FINSEQ_1:def 15
.=
[.(lower_bound A),(D1 . 1).]
by A22, FUNCT_1:47
;
hence
(upper_volume (g,DD1)) . i = ((upper_volume (f,D1)) | 1) . i
by A27, A26, A25;
verum
end;
A28:
g | (divset (D1,1)) is
bounded_above
A33:
rng D2 c= A
by Def1;
A34:
indx (
D2,
D1,1)
in dom D2
by A1, A5, Def18;
then A35:
indx (
D2,
D1,1)
in Seg (len D2)
by FINSEQ_1:def 3;
then A36:
1
<= indx (
D2,
D1,1)
by FINSEQ_1:1;
A37:
indx (
D2,
D1,1)
<= len D2
by A35, FINSEQ_1:1;
then
1
<= len D2
by A36, XXREAL_0:2;
then
1
in Seg (len D2)
by FINSEQ_1:1;
then A38:
1
in dom D2
by FINSEQ_1:def 3;
then
D2 . 1
in rng D2
by FUNCT_1:def 3;
then
D2 . 1
in A
by A33;
then
D2 . 1
in [.(lower_bound A),(upper_bound A).]
by Th2;
then
D2 . 1
in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) }
by RCOMP_1:def 1;
then
ex
a being
Real st
(
D2 . 1
= a &
lower_bound A <= a &
a <= upper_bound A )
;
then
D2 . 1
>= lower_bound (divset (D1,1))
by A5, Def3;
then reconsider DD2 =
mid (
D2,1,
(indx (D2,D1,1))) as
Division of
divset (
D1,1)
by A34, A36, A38, A7, Th35;
indx (
D2,
D1,1)
in dom D2
by A1, A5, Def18;
then A39:
indx (
D2,
D1,1)
in Seg (len D2)
by FINSEQ_1:def 3;
then A40:
1
<= indx (
D2,
D1,1)
by FINSEQ_1:1;
A41:
indx (
D2,
D1,1)
<= len D2
by A39, FINSEQ_1:1;
then A42:
1
<= len D2
by A40, XXREAL_0:2;
then
len (mid (D2,1,(indx (D2,D1,1)))) = ((indx (D2,D1,1)) -' 1) + 1
by A40, A41, FINSEQ_6:118;
then A43:
len (mid (D2,1,(indx (D2,D1,1)))) = ((indx (D2,D1,1)) - 1) + 1
by A40, XREAL_1:233;
then A44:
len (mid (D2,1,(indx (D2,D1,1)))) = len (D2 | (indx (D2,D1,1)))
by A41, FINSEQ_1:59;
A45:
for
k being
Nat st 1
<= k &
k <= len (mid (D2,1,(indx (D2,D1,1)))) holds
(mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k
proof
let k be
Nat;
( 1 <= k & k <= len (mid (D2,1,(indx (D2,D1,1)))) implies (mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k )
assume that A46:
1
<= k
and A47:
k <= len (mid (D2,1,(indx (D2,D1,1))))
;
(mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k
k in Seg (len (D2 | (indx (D2,D1,1))))
by A44, A46, A47, FINSEQ_1:1;
then
k in dom (D2 | (indx (D2,D1,1)))
by FINSEQ_1:def 3;
then
k in dom (D2 | (Seg (indx (D2,D1,1))))
by FINSEQ_1:def 15;
then A48:
(D2 | (Seg (indx (D2,D1,1)))) . k = D2 . k
by FUNCT_1:47;
(mid (D2,1,(indx (D2,D1,1)))) . k = D2 . ((k + 1) -' 1)
by A40, A41, A42, A46, A47, FINSEQ_6:118;
then
(mid (D2,1,(indx (D2,D1,1)))) . k = D2 . ((k + 1) - 1)
by NAT_1:11, XREAL_1:233;
hence
(mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k
by A48, FINSEQ_1:def 15;
verum
end;
then A49:
mid (
D2,1,
(indx (D2,D1,1)))
= D2 | (indx (D2,D1,1))
by A44, FINSEQ_1:14;
A50:
for
i being
Nat st 1
<= i &
i <= len (upper_volume (g,DD2)) holds
(upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i
proof
let i be
Nat;
( 1 <= i & i <= len (upper_volume (g,DD2)) implies (upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i )
assume that A51:
1
<= i
and A52:
i <= len (upper_volume (g,DD2))
;
(upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i
A53:
i <= len DD2
by A52, Def5;
then A54:
i in Seg (len DD2)
by A51, FINSEQ_1:1;
then A55:
i in dom DD2
by FINSEQ_1:def 3;
divset (
DD2,
i)
= divset (
D2,
i)
proof
Seg (indx (D2,D1,1)) c= Seg (len D2)
by A41, FINSEQ_1:5;
then
i in Seg (len D2)
by A43, A54;
then A56:
i in dom D2
by FINSEQ_1:def 3;
now divset (DD2,i) = divset (D2,i)per cases
( i = 1 or i <> 1 )
;
suppose A57:
i = 1
;
divset (DD2,i) = divset (D2,i)then A58:
1
in dom (D2 | (Seg (indx (D2,D1,1))))
by A49, A55, FINSEQ_1:def 15;
then
1
in (dom D2) /\ (Seg (indx (D2,D1,1)))
by RELAT_1:61;
then A59:
1
in dom D2
by XBOOLE_0:def 4;
A60:
divset (
D2,
i) =
[.(lower_bound (divset (D2,1))),(upper_bound (divset (D2,1))).]
by A57, Th2
.=
[.(lower_bound A),(upper_bound (divset (D2,1))).]
by A59, Def3
.=
[.(lower_bound A),(D2 . 1).]
by A59, Def3
;
divset (
DD2,
i) =
[.(lower_bound (divset (DD2,1))),(upper_bound (divset (DD2,1))).]
by A57, Th2
.=
[.(lower_bound (divset (D1,1))),(upper_bound (divset (DD2,1))).]
by A55, A57, Def3
.=
[.(lower_bound (divset (D1,1))),(DD2 . 1).]
by A55, A57, Def3
.=
[.(lower_bound (divset (D1,1))),((D2 | (indx (D2,D1,1))) . 1).]
by A45, A53, A57
.=
[.(lower_bound (divset (D1,1))),((D2 | (Seg (indx (D2,D1,1)))) . 1).]
by FINSEQ_1:def 15
.=
[.(lower_bound (divset (D1,1))),(D2 . 1).]
by A58, FUNCT_1:47
.=
[.(lower_bound A),(D2 . 1).]
by A5, Def3
;
hence
divset (
DD2,
i)
= divset (
D2,
i)
by A60;
verum end; suppose A61:
i <> 1
;
divset (DD2,i) = divset (D2,i)A62:
i - 1
in dom (D2 | (Seg (indx (D2,D1,1))))
proof
not
i is
trivial
by A51, A61, NAT_2:def 1;
then A63:
i >= 1
+ 1
by NAT_2:29;
then A64:
1
<= i - 1
by XREAL_1:19;
A65:
ex
j being
Nat st
i = 1
+ j
by A51, NAT_1:10;
A66:
i - 1
<= (indx (D2,D1,1)) - 0
by A43, A53, XREAL_1:13;
then
i - 1
<= len D2
by A37, XXREAL_0:2;
then
i - 1
in Seg (len D2)
by A65, A64, FINSEQ_1:1;
then A67:
i - 1
in dom D2
by FINSEQ_1:def 3;
i - 1
>= 1
by A63, XREAL_1:19;
then
i - 1
in Seg (indx (D2,D1,1))
by A65, A66, FINSEQ_1:1;
then
i - 1
in (dom D2) /\ (Seg (indx (D2,D1,1)))
by A67, XBOOLE_0:def 4;
hence
i - 1
in dom (D2 | (Seg (indx (D2,D1,1))))
by RELAT_1:61;
verum
end; DD2 . (i - 1) =
(D2 | (indx (D2,D1,1))) . (i - 1)
by A44, A45, FINSEQ_1:14
.=
(D2 | (Seg (indx (D2,D1,1)))) . (i - 1)
by FINSEQ_1:def 15
;
then A68:
DD2 . (i - 1) = D2 . (i - 1)
by A62, FUNCT_1:47;
i <= len D2
by A43, A37, A53, XXREAL_0:2;
then
i in Seg (len D2)
by A51, FINSEQ_1:1;
then
i in dom D2
by FINSEQ_1:def 3;
then
i in (dom D2) /\ (Seg (indx (D2,D1,1)))
by A43, A54, XBOOLE_0:def 4;
then A69:
i in dom (D2 | (Seg (indx (D2,D1,1))))
by RELAT_1:61;
DD2 . i =
(D2 | (indx (D2,D1,1))) . i
by A44, A45, FINSEQ_1:14
.=
(D2 | (Seg (indx (D2,D1,1)))) . i
by FINSEQ_1:def 15
;
then A70:
DD2 . i = D2 . i
by A69, FUNCT_1:47;
A71:
divset (
D2,
i) =
[.(lower_bound (divset (D2,i))),(upper_bound (divset (D2,i))).]
by Th2
.=
[.(D2 . (i - 1)),(upper_bound (divset (D2,i))).]
by A56, A61, Def3
.=
[.(D2 . (i - 1)),(D2 . i).]
by A56, A61, Def3
;
divset (
DD2,
i) =
[.(lower_bound (divset (DD2,i))),(upper_bound (divset (DD2,i))).]
by Th2
.=
[.(DD2 . (i - 1)),(upper_bound (divset (DD2,i))).]
by A55, A61, Def3
.=
[.(D2 . (i - 1)),(D2 . i).]
by A55, A61, A68, A70, Def3
;
hence
divset (
DD2,
i)
= divset (
D2,
i)
by A71;
verum end; end; end;
hence
divset (
DD2,
i)
= divset (
D2,
i)
;
verum
end;
then A72:
(upper_volume (g,DD2)) . i = (upper_bound (rng (g | (divset (D2,i))))) * (vol (divset (D2,i)))
by A55, Def5;
Seg (indx (D2,D1,1)) c= Seg (len D2)
by A41, FINSEQ_1:5;
then
i in Seg (len D2)
by A43, A54;
then A73:
i in dom D2
by FINSEQ_1:def 3;
A74:
i in dom DD2
by A54, FINSEQ_1:def 3;
A75:
now ( lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] & upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] )per cases
( i = 1 or i <> 1 )
;
suppose A76:
i = 1
;
( lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] & upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] )then
1
in dom (D2 | (Seg (indx (D2,D1,1))))
by A49, A74, FINSEQ_1:def 15;
then
1
in (dom D2) /\ (Seg (indx (D2,D1,1)))
by RELAT_1:61;
then A77:
1
in dom D2
by XBOOLE_0:def 4;
then A78:
D2 . 1
<= D2 . (indx (D2,D1,1))
by A34, A36, SEQ_4:137;
lower_bound (divset (D2,i)) = lower_bound A
by A76, A77, Def3;
then A79:
lower_bound (divset (D2,i)) = lower_bound (divset (D1,1))
by A5, Def3;
upper_bound (divset (D2,i)) = D2 . 1
by A76, A77, Def3;
then
upper_bound (divset (D2,i)) <= D1 . 1
by A1, A5, A78, Def18;
then A80:
upper_bound (divset (D2,i)) <= upper_bound (divset (D1,1))
by A5, Def3;
lower_bound (divset (D1,1)) <= upper_bound (divset (D1,1))
by SEQ_4:11;
hence
lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
by A79, XXREAL_1:1;
upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
lower_bound (divset (D2,i)) <= upper_bound (divset (D2,i))
by SEQ_4:11;
then
upper_bound (divset (D2,i)) in { r where r is Real : ( lower_bound (divset (D1,1)) <= r & r <= upper_bound (divset (D1,1)) ) }
by A79, A80;
hence
upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
by RCOMP_1:def 1;
verum end; suppose A81:
i <> 1
;
( lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] & upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] )then
not
i is
trivial
by A51, NAT_2:def 1;
then
i >= 1
+ 1
by NAT_2:29;
then A82:
1
<= i - 1
by XREAL_1:19;
A83:
ex
j being
Nat st
i = 1
+ j
by A51, NAT_1:10;
A84:
rng D2 c= A
by Def1;
A85:
lower_bound (divset (D2,i)) = D2 . (i - 1)
by A73, A81, Def3;
A86:
lower_bound (divset (D1,1)) = lower_bound A
by A5, Def3;
A87:
i - 1
<= (indx (D2,D1,1)) - 0
by A43, A53, XREAL_1:13;
then
i - 1
<= len D2
by A37, XXREAL_0:2;
then
i - 1
in Seg (len D2)
by A83, A82, FINSEQ_1:1;
then A88:
i - 1
in dom D2
by FINSEQ_1:def 3;
then
D2 . (i - 1) in rng D2
by FUNCT_1:def 3;
then A89:
lower_bound (divset (D2,i)) >= lower_bound (divset (D1,1))
by A85, A86, A84, SEQ_4:def 2;
A90:
upper_bound (divset (D1,1)) = D1 . 1
by A5, Def3;
D2 . (i - 1) <= D2 . (indx (D2,D1,1))
by A34, A87, A88, SEQ_4:137;
then
lower_bound (divset (D2,i)) <= upper_bound (divset (D1,1))
by A1, A5, A85, A90, Def18;
then
lower_bound (divset (D2,i)) in { r where r is Real : ( lower_bound (divset (D1,1)) <= r & r <= upper_bound (divset (D1,1)) ) }
by A89;
hence
lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
by RCOMP_1:def 1;
upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]A91:
upper_bound (divset (D2,i)) = D2 . i
by A73, A81, Def3;
D2 . i in rng D2
by A73, FUNCT_1:def 3;
then A92:
upper_bound (divset (D2,i)) >= lower_bound (divset (D1,1))
by A91, A86, A84, SEQ_4:def 2;
D2 . i <= D2 . (indx (D2,D1,1))
by A43, A34, A53, A73, SEQ_4:137;
then
upper_bound (divset (D2,i)) <= upper_bound (divset (D1,1))
by A1, A5, A91, A90, Def18;
then
upper_bound (divset (D2,i)) in { r where r is Real : ( lower_bound (divset (D1,1)) <= r & r <= upper_bound (divset (D1,1)) ) }
by A92;
hence
upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
by RCOMP_1:def 1;
verum end; end; end;
A93:
divset (
D1,1)
= [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
by Th2;
A94:
Seg (indx (D2,D1,1)) c= Seg (len D2)
by A41, FINSEQ_1:5;
then
i in Seg (len D2)
by A43, A54;
then A95:
i in dom D2
by FINSEQ_1:def 3;
divset (
D2,
i)
= [.(lower_bound (divset (D2,i))),(upper_bound (divset (D2,i))).]
by Th2;
then A96:
divset (
D2,
i)
c= divset (
D1,1)
by A93, A75, XXREAL_2:def 12;
A97:
dom ((upper_volume (f,D2)) | (Seg (indx (D2,D1,1)))) =
(dom (upper_volume (f,D2))) /\ (Seg (indx (D2,D1,1)))
by RELAT_1:61
.=
(Seg (len (upper_volume (f,D2)))) /\ (Seg (indx (D2,D1,1)))
by FINSEQ_1:def 3
.=
(Seg (len D2)) /\ (Seg (indx (D2,D1,1)))
by Def5
.=
Seg (indx (D2,D1,1))
by A94, XBOOLE_1:28
;
((upper_volume (f,D2)) | (indx (D2,D1,1))) . i =
((upper_volume (f,D2)) | (Seg (indx (D2,D1,1)))) . i
by FINSEQ_1:def 15
.=
(upper_volume (f,D2)) . i
by A43, A54, A97, FUNCT_1:47
.=
(upper_bound (rng (f | (divset (D2,i))))) * (vol (divset (D2,i)))
by A95, Def5
;
hence
(upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i
by A72, A96, FUNCT_1:51;
verum
end;
len (upper_volume (g,DD1)) = len ((upper_volume (f,D1)) | 1)
by A10;
then A98:
upper_volume (
g,
DD1)
= (upper_volume (f,D1)) | 1
by A18, FINSEQ_1:14;
A99:
indx (
D2,
D1,1)
<= len (upper_volume (f,D2))
by A41, Def5;
len (upper_volume (g,DD2)) = indx (
D2,
D1,1)
by A43, Def5;
then A100:
len (upper_volume (g,DD2)) = len ((upper_volume (f,D2)) | (indx (D2,D1,1)))
by A99, FINSEQ_1:59;
dom g = A /\ (divset (D1,1))
by A4, FUNCT_2:def 1;
then
dom g = divset (
D1,1)
by A5, Th6, XBOOLE_1:28;
then
g is
total
by PARTFUN1:def 2;
then
upper_sum (
g,
DD1)
>= upper_sum (
g,
DD2)
by A11, A28, Th28;
hence
Sum ((upper_volume (f,D1)) | 1) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,1)))
by A98, A100, A50, FINSEQ_1:14;
verum
end;
A101:
for
k being non
zero Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume A102:
(
k in dom D1 implies
Sum ((upper_volume (f,D1)) | k) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,k))) )
;
S1[k + 1]
assume A103:
k + 1
in dom D1
;
Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
then A104:
k + 1
in Seg (len D1)
by FINSEQ_1:def 3;
then A105:
1
<= k + 1
by FINSEQ_1:1;
A106:
k + 1
<= len D1
by A104, FINSEQ_1:1;
now Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))per cases
( 1 = k + 1 or 1 <> k + 1 )
;
suppose A107:
1
<> k + 1
;
Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))set IDK =
indx (
D2,
D1,
k);
set IDK1 =
indx (
D2,
D1,
(k + 1));
set K1D2 =
(upper_volume (f,D2)) | (indx (D2,D1,(k + 1)));
set KD1 =
(upper_volume (f,D1)) | k;
set K1D1 =
(upper_volume (f,D1)) | (k + 1);
set n =
k + 1;
A108:
k + 1
<= len (upper_volume (f,D1))
by A106, Def5;
then A109:
len ((upper_volume (f,D1)) | (k + 1)) = k + 1
by FINSEQ_1:59;
then consider p1,
q1 being
FinSequence of
REAL such that A110:
len p1 = k
and A111:
len q1 = 1
and A112:
(upper_volume (f,D1)) | (k + 1) = p1 ^ q1
by FINSEQ_2:23;
A113:
k <= k + 1
by NAT_1:11;
then A114:
k <= len D1
by A106, XXREAL_0:2;
then A115:
k <= len (upper_volume (f,D1))
by Def5;
then A116:
len p1 = len ((upper_volume (f,D1)) | k)
by A110, FINSEQ_1:59;
for
i being
Nat st 1
<= i &
i <= len p1 holds
p1 . i = ((upper_volume (f,D1)) | k) . i
proof
let i be
Nat;
( 1 <= i & i <= len p1 implies p1 . i = ((upper_volume (f,D1)) | k) . i )
assume that A117:
1
<= i
and A118:
i <= len p1
;
p1 . i = ((upper_volume (f,D1)) | k) . i
A119:
i in Seg (len p1)
by A117, A118, FINSEQ_1:1;
then A120:
i in dom ((upper_volume (f,D1)) | k)
by A116, FINSEQ_1:def 3;
then A121:
i in dom ((upper_volume (f,D1)) | (Seg k))
by FINSEQ_1:def 15;
k <= k + 1
by NAT_1:11;
then A122:
Seg k c= Seg (k + 1)
by FINSEQ_1:5;
A123:
dom ((upper_volume (f,D1)) | (k + 1)) =
Seg (len ((upper_volume (f,D1)) | (k + 1)))
by FINSEQ_1:def 3
.=
Seg (k + 1)
by A108, FINSEQ_1:59
;
dom ((upper_volume (f,D1)) | k) =
Seg (len ((upper_volume (f,D1)) | k))
by FINSEQ_1:def 3
.=
Seg k
by A115, FINSEQ_1:59
;
then
i in dom ((upper_volume (f,D1)) | (k + 1))
by A120, A122, A123;
then A124:
i in dom ((upper_volume (f,D1)) | (Seg (k + 1)))
by FINSEQ_1:def 15;
A125:
((upper_volume (f,D1)) | (k + 1)) . i =
((upper_volume (f,D1)) | (Seg (k + 1))) . i
by FINSEQ_1:def 15
.=
(upper_volume (f,D1)) . i
by A124, FUNCT_1:47
;
A126:
((upper_volume (f,D1)) | k) . i =
((upper_volume (f,D1)) | (Seg k)) . i
by FINSEQ_1:def 15
.=
(upper_volume (f,D1)) . i
by A121, FUNCT_1:47
;
i in dom p1
by A119, FINSEQ_1:def 3;
hence
p1 . i = ((upper_volume (f,D1)) | k) . i
by A112, A126, A125, FINSEQ_1:def 7;
verum
end; then A127:
p1 = (upper_volume (f,D1)) | k
by A116, FINSEQ_1:14;
A128:
indx (
D2,
D1,
(k + 1))
in dom D2
by A1, A103, Def18;
then A129:
indx (
D2,
D1,
(k + 1))
in Seg (len D2)
by FINSEQ_1:def 3;
then A130:
1
<= indx (
D2,
D1,
(k + 1))
by FINSEQ_1:1;
not
k + 1 is
trivial
by A107, NAT_2:def 1;
then
k + 1
>= 2
by NAT_2:29;
then
k >= (1 + 1) - 1
by XREAL_1:20;
then A131:
k in Seg (len D1)
by A114, FINSEQ_1:1;
then A132:
k in dom D1
by FINSEQ_1:def 3;
then A133:
indx (
D2,
D1,
k)
in dom D2
by A1, Def18;
A134:
indx (
D2,
D1,
k)
< indx (
D2,
D1,
(k + 1))
proof
k < k + 1
by NAT_1:13;
then A135:
D1 . k < D1 . (k + 1)
by A103, A132, SEQM_3:def 1;
assume
indx (
D2,
D1,
k)
>= indx (
D2,
D1,
(k + 1))
;
contradiction
then A136:
D2 . (indx (D2,D1,k)) >= D2 . (indx (D2,D1,(k + 1)))
by A133, A128, SEQ_4:137;
D1 . k = D2 . (indx (D2,D1,k))
by A1, A132, Def18;
hence
contradiction
by A1, A103, A136, A135, Def18;
verum
end; A137:
indx (
D2,
D1,
(k + 1))
>= indx (
D2,
D1,
k)
proof
assume
indx (
D2,
D1,
(k + 1))
< indx (
D2,
D1,
k)
;
contradiction
then A138:
D2 . (indx (D2,D1,(k + 1))) < D2 . (indx (D2,D1,k))
by A133, A128, SEQM_3:def 1;
D1 . (k + 1) = D2 . (indx (D2,D1,(k + 1)))
by A1, A103, Def18;
then
D1 . (k + 1) < D1 . k
by A1, A132, A138, Def18;
hence
contradiction
by A103, A132, NAT_1:11, SEQ_4:137;
verum
end; then consider ID being
Nat such that A139:
indx (
D2,
D1,
(k + 1))
= (indx (D2,D1,k)) + ID
by NAT_1:10;
reconsider ID =
ID as
Element of
NAT by ORDINAL1:def 12;
A140:
len (upper_volume (f,D2)) = len D2
by Def5;
then A141:
indx (
D2,
D1,
(k + 1))
<= len (upper_volume (f,D2))
by A129, FINSEQ_1:1;
then
len ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = (indx (D2,D1,k)) + ((indx (D2,D1,(k + 1))) - (indx (D2,D1,k)))
by FINSEQ_1:59;
then consider p2,
q2 being
FinSequence of
REAL such that A142:
len p2 = indx (
D2,
D1,
k)
and A143:
len q2 = (indx (D2,D1,(k + 1))) - (indx (D2,D1,k))
and A144:
(upper_volume (f,D2)) | (indx (D2,D1,(k + 1))) = p2 ^ q2
by A139, FINSEQ_2:23;
indx (
D2,
D1,
k)
in dom D2
by A1, A132, Def18;
then A145:
indx (
D2,
D1,
k)
in Seg (len (upper_volume (f,D2)))
by A140, FINSEQ_1:def 3;
then A146:
1
<= indx (
D2,
D1,
k)
by FINSEQ_1:1;
set KD2 =
(upper_volume (f,D2)) | (indx (D2,D1,k));
A147:
Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = (Sum p2) + (Sum q2)
by A144, RVSUM_1:75;
A148:
indx (
D2,
D1,
k)
<= len (upper_volume (f,D2))
by A145, FINSEQ_1:1;
then A149:
len p2 = len ((upper_volume (f,D2)) | (indx (D2,D1,k)))
by A142, FINSEQ_1:59;
for
i being
Nat st 1
<= i &
i <= len p2 holds
p2 . i = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i
proof
let i be
Nat;
( 1 <= i & i <= len p2 implies p2 . i = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i )
assume that A150:
1
<= i
and A151:
i <= len p2
;
p2 . i = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i
A152:
i in Seg (len p2)
by A150, A151, FINSEQ_1:1;
then A153:
i in dom ((upper_volume (f,D2)) | (indx (D2,D1,k)))
by A149, FINSEQ_1:def 3;
then A154:
i in dom ((upper_volume (f,D2)) | (Seg (indx (D2,D1,k))))
by FINSEQ_1:def 15;
A155:
dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) =
Seg (len ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))))
by FINSEQ_1:def 3
.=
Seg (indx (D2,D1,(k + 1)))
by A141, FINSEQ_1:59
;
A156:
Seg (indx (D2,D1,k)) c= Seg (indx (D2,D1,(k + 1)))
by A137, FINSEQ_1:5;
dom ((upper_volume (f,D2)) | (indx (D2,D1,k))) =
Seg (len ((upper_volume (f,D2)) | (indx (D2,D1,k))))
by FINSEQ_1:def 3
.=
Seg (indx (D2,D1,k))
by A148, FINSEQ_1:59
;
then
i in dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
by A153, A156, A155;
then A157:
i in dom ((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1)))))
by FINSEQ_1:def 15;
A158:
((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) . i =
((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) . i
by FINSEQ_1:def 15
.=
(upper_volume (f,D2)) . i
by A157, FUNCT_1:47
;
A159:
((upper_volume (f,D2)) | (indx (D2,D1,k))) . i =
((upper_volume (f,D2)) | (Seg (indx (D2,D1,k)))) . i
by FINSEQ_1:def 15
.=
(upper_volume (f,D2)) . i
by A154, FUNCT_1:47
;
i in dom p2
by A152, FINSEQ_1:def 3;
hence
p2 . i = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i
by A144, A159, A158, FINSEQ_1:def 7;
verum
end; then A160:
p2 = (upper_volume (f,D2)) | (indx (D2,D1,k))
by A149, FINSEQ_1:14;
A161:
indx (
D2,
D1,
(k + 1))
<= len D2
by A129, FINSEQ_1:1;
A162:
ID = (indx (D2,D1,(k + 1))) - (indx (D2,D1,k))
by A139;
A163:
Sum q1 >= Sum q2
proof
set MD2 =
mid (
D2,
((indx (D2,D1,k)) + 1),
(indx (D2,D1,(k + 1))));
set MD1 =
mid (
D1,
(k + 1),
(k + 1));
set DD1 =
divset (
D1,
(k + 1));
set g =
f | (divset (D1,(k + 1)));
A164:
1
<= (indx (D2,D1,k)) + 1
by NAT_1:11;
reconsider g =
f | (divset (D1,(k + 1))) as
PartFunc of
(divset (D1,(k + 1))),
REAL by PARTFUN1:10;
(k + 1) - 1
= k
;
then A165:
lower_bound (divset (D1,(k + 1))) = D1 . k
by A103, A107, Def3;
D2 . (indx (D2,D1,(k + 1))) = D1 . (k + 1)
by A1, A103, Def18;
then A166:
D2 . (indx (D2,D1,(k + 1))) = upper_bound (divset (D1,(k + 1)))
by A103, A107, Def3;
A167:
(indx (D2,D1,k)) + 1
<= indx (
D2,
D1,
(k + 1))
by A134, NAT_1:13;
then A168:
(indx (D2,D1,k)) + 1
<= len D2
by A161, XXREAL_0:2;
then
(indx (D2,D1,k)) + 1
in Seg (len D2)
by A164, FINSEQ_1:1;
then A169:
(indx (D2,D1,k)) + 1
in dom D2
by FINSEQ_1:def 3;
then
D2 . ((indx (D2,D1,k)) + 1) >= D2 . (indx (D2,D1,k))
by A133, NAT_1:11, SEQ_4:137;
then
D2 . ((indx (D2,D1,k)) + 1) >= lower_bound (divset (D1,(k + 1)))
by A1, A132, A165, Def18;
then reconsider MD2 =
mid (
D2,
((indx (D2,D1,k)) + 1),
(indx (D2,D1,(k + 1)))) as
Division of
divset (
D1,
(k + 1))
by A128, A167, A169, A166, Th35;
A170:
((indx (D2,D1,(k + 1))) -' ((indx (D2,D1,k)) + 1)) + 1 =
((indx (D2,D1,(k + 1))) - ((indx (D2,D1,k)) + 1)) + 1
by A167, XREAL_1:233
.=
(indx (D2,D1,(k + 1))) - (indx (D2,D1,k))
;
A171:
for
n being
Nat st 1
<= n &
n <= len q2 holds
q2 . n = (upper_volume (g,MD2)) . n
proof
A172:
dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) =
Seg (len ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))))
by FINSEQ_1:def 3
.=
Seg (indx (D2,D1,(k + 1)))
by A141, FINSEQ_1:59
;
then A173:
dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) c= Seg (len D2)
by A161, FINSEQ_1:5;
then A174:
dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) c= dom D2
by FINSEQ_1:def 3;
A175:
len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) = ID
by A130, A161, A139, A167, A168, A164, A170, FINSEQ_6:118;
let n be
Nat;
( 1 <= n & n <= len q2 implies q2 . n = (upper_volume (g,MD2)) . n )
assume that A176:
1
<= n
and A177:
n <= len q2
;
q2 . n = (upper_volume (g,MD2)) . n
n in Seg (len q2)
by A176, A177, FINSEQ_1:1;
then A178:
n in dom q2
by FINSEQ_1:def 3;
then A179:
(indx (D2,D1,k)) + n in dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
by A142, A144, FINSEQ_1:28;
then A180:
(indx (D2,D1,k)) + n in dom ((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1)))))
by FINSEQ_1:def 15;
A181:
q2 . n =
((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) . ((indx (D2,D1,k)) + n)
by A142, A144, A178, FINSEQ_1:def 7
.=
((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) . ((indx (D2,D1,k)) + n)
by FINSEQ_1:def 15
.=
(upper_volume (f,D2)) . ((indx (D2,D1,k)) + n)
by A180, FUNCT_1:47
.=
(upper_bound (rng (f | (divset (D2,((indx (D2,D1,k)) + n)))))) * (vol (divset (D2,((indx (D2,D1,k)) + n))))
by A179, A174, Def5
;
(indx (D2,D1,k)) + n in Seg (len D2)
by A179, A173;
then A182:
(indx (D2,D1,k)) + n in dom D2
by FINSEQ_1:def 3;
(indx (D2,D1,k)) + n <= indx (
D2,
D1,
(k + 1))
by A172, A179, FINSEQ_1:1;
then A183:
n <= ID
by A162, XREAL_1:19;
then
n in Seg ID
by A176, FINSEQ_1:1;
then A184:
n in dom MD2
by A175, FINSEQ_1:def 3;
n in Seg (len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))))
by A176, A183, A175, FINSEQ_1:1;
then A185:
n in dom (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1)))))
by FINSEQ_1:def 3;
A186:
1
<= (indx (D2,D1,k)) + n
by A172, A179, FINSEQ_1:1;
A187:
(
divset (
MD2,
n)
= divset (
D2,
((indx (D2,D1,k)) + n)) &
divset (
D2,
((indx (D2,D1,k)) + n))
c= divset (
D1,
(k + 1)) )
proof
now ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )per cases
( n = 1 or n <> 1 )
;
suppose A188:
n = 1
;
( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )then A189:
(indx (D2,D1,k)) + 1
<= len D2
by A179, A173, FINSEQ_1:1;
A190:
1
<= (indx (D2,D1,k)) + 1
by A172, A179, A188, FINSEQ_1:1;
A191:
upper_bound (divset (MD2,1)) =
(mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) . 1
by A184, A188, Def3
.=
D2 . (1 + (indx (D2,D1,k)))
by A130, A161, A190, A189, FINSEQ_6:118
;
A192:
(indx (D2,D1,k)) + 1
<> 1
by A146, NAT_1:13;
A193:
(k + 1) - 1
= k
;
A194:
lower_bound (divset (MD2,1)) =
lower_bound (divset (D1,(k + 1)))
by A184, A188, Def3
.=
D1 . k
by A103, A107, A193, Def3
;
A195:
divset (
D2,
((indx (D2,D1,k)) + n)) =
[.(lower_bound (divset (D2,((indx (D2,D1,k)) + 1)))),(upper_bound (divset (D2,((indx (D2,D1,k)) + 1)))).]
by A188, Th2
.=
[.(D2 . (((indx (D2,D1,k)) + 1) - 1)),(upper_bound (divset (D2,((indx (D2,D1,k)) + 1)))).]
by A169, A192, Def3
.=
[.(D2 . (indx (D2,D1,k))),(D2 . ((indx (D2,D1,k)) + 1)).]
by A169, A192, Def3
.=
[.(D1 . k),(D2 . ((indx (D2,D1,k)) + 1)).]
by A1, A132, Def18
;
hence
divset (
MD2,
n)
= divset (
D2,
((indx (D2,D1,k)) + n))
by A188, A194, A191, Th2;
( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
divset (
MD2,
n)
= [.(D1 . k),(D2 . ((indx (D2,D1,k)) + 1)).]
by A188, A194, A191, Th2;
hence
(
divset (
MD2,
n)
= divset (
D2,
((indx (D2,D1,k)) + n)) &
divset (
D2,
((indx (D2,D1,k)) + n))
c= divset (
D1,
(k + 1)) )
by A184, A195, Th6;
verum end; suppose A196:
n <> 1
;
( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )A197:
(indx (D2,D1,k)) + n <> 1
A198:
divset (
D2,
((indx (D2,D1,k)) + n)) =
[.(lower_bound (divset (D2,((indx (D2,D1,k)) + n)))),(upper_bound (divset (D2,((indx (D2,D1,k)) + n)))).]
by Th2
.=
[.(D2 . (((indx (D2,D1,k)) + n) - 1)),(upper_bound (divset (D2,((indx (D2,D1,k)) + n)))).]
by A182, A197, Def3
.=
[.(D2 . (((indx (D2,D1,k)) + n) - 1)),(D2 . ((indx (D2,D1,k)) + n)).]
by A182, A197, Def3
;
n <= n + 1
by NAT_1:12;
then
n - 1
<= n
by XREAL_1:20;
then A199:
n - 1
<= len MD2
by A183, A175, XXREAL_0:2;
consider n1 being
Nat such that A200:
n = 1
+ n1
by A176, NAT_1:10;
not
n is
trivial
by A176, A196, NAT_2:def 1;
then
n >= 1
+ 1
by NAT_2:29;
then A201:
1
<= n - 1
by XREAL_1:19;
A202:
(indx (D2,D1,k)) + 1
<= indx (
D2,
D1,
(k + 1))
by A134, NAT_1:13;
reconsider n1 =
n1 as
Element of
NAT by ORDINAL1:def 12;
A203:
(n1 + ((indx (D2,D1,k)) + 1)) -' 1
= ((indx (D2,D1,k)) + n) - 1
by A186, A200, XREAL_1:233;
A204:
(n + ((indx (D2,D1,k)) + 1)) -' 1 =
((n + (indx (D2,D1,k))) + 1) - 1
by NAT_1:11, XREAL_1:233
.=
(indx (D2,D1,k)) + n
;
A205:
lower_bound (divset (MD2,n)) =
MD2 . (n - 1)
by A184, A196, Def3
.=
D2 . (((indx (D2,D1,k)) + n) - 1)
by A130, A161, A168, A164, A202, A200, A203, A201, A199, FINSEQ_6:118
;
A206:
upper_bound (divset (MD2,n)) =
MD2 . n
by A184, A196, Def3
.=
D2 . ((indx (D2,D1,k)) + n)
by A130, A161, A168, A164, A176, A183, A175, A202, A204, FINSEQ_6:118
;
hence
divset (
MD2,
n)
= divset (
D2,
((indx (D2,D1,k)) + n))
by A205, A198, Th2;
( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
divset (
MD2,
n)
= [.(D2 . (((indx (D2,D1,k)) + n) - 1)),(D2 . ((indx (D2,D1,k)) + n)).]
by A205, A206, Th2;
hence
(
divset (
MD2,
n)
= divset (
D2,
((indx (D2,D1,k)) + n)) &
divset (
D2,
((indx (D2,D1,k)) + n))
c= divset (
D1,
(k + 1)) )
by A184, A198, Th6;
verum end; end; end;
hence
(
divset (
MD2,
n)
= divset (
D2,
((indx (D2,D1,k)) + n)) &
divset (
D2,
((indx (D2,D1,k)) + n))
c= divset (
D1,
(k + 1)) )
;
verum
end;
then
g | (divset (MD2,n)) = f | (divset (D2,((indx (D2,D1,k)) + n)))
by FUNCT_1:51;
hence
q2 . n = (upper_volume (g,MD2)) . n
by A185, A181, A187, Def5;
verum
end;
(k + 1) - 1
= k
;
then A207:
lower_bound (divset (D1,(k + 1))) = D1 . k
by A103, A107, Def3;
D1 . (k + 1) = upper_bound (divset (D1,(k + 1)))
by A103, A107, Def3;
then reconsider MD1 =
mid (
D1,
(k + 1),
(k + 1)) as
Division of
divset (
D1,
(k + 1))
by A103, A113, A132, A207, Th35, SEQ_4:137;
A208:
g | (divset (D1,(k + 1))) is
bounded_above
len MD1 = ((k + 1) -' (k + 1)) + 1
by A105, A106, FINSEQ_6:118;
then A213:
len MD1 = ((k + 1) - (k + 1)) + 1
by XREAL_1:233;
then A214:
dom q1 = dom MD1
by A111, FINSEQ_3:29;
A215:
for
n being
Nat st 1
<= n &
n <= len q1 holds
q1 . n = (upper_volume (g,MD1)) . n
proof
k + 1
in Seg (len ((upper_volume (f,D1)) | (k + 1)))
by A109, FINSEQ_1:4;
then
k + 1
in dom ((upper_volume (f,D1)) | (k + 1))
by FINSEQ_1:def 3;
then A216:
k + 1
in dom ((upper_volume (f,D1)) | (Seg (k + 1)))
by FINSEQ_1:def 15;
A217:
MD1 . 1
= D1 . (k + 1)
by A105, A106, FINSEQ_6:118;
1
in Seg (len MD1)
by A213, FINSEQ_1:3;
then A218:
1
in dom MD1
by FINSEQ_1:def 3;
divset (
MD1,1)
= [.(lower_bound (divset (MD1,1))),(upper_bound (divset (MD1,1))).]
by Th2;
then A219:
divset (
MD1,1) =
[.(lower_bound (divset (D1,(k + 1)))),(upper_bound (divset (MD1,1))).]
by A218, Def3
.=
[.(lower_bound (divset (D1,(k + 1)))),(D1 . (k + 1)).]
by A218, A217, Def3
;
(k + 1) - 1
= k
;
then A220:
lower_bound (divset (D1,(k + 1))) = D1 . k
by A103, A107, Def3;
let n be
Nat;
( 1 <= n & n <= len q1 implies q1 . n = (upper_volume (g,MD1)) . n )
assume that A221:
1
<= n
and A222:
n <= len q1
;
q1 . n = (upper_volume (g,MD1)) . n
A223:
n = 1
by A111, A221, A222, XXREAL_0:1;
n in Seg (len q1)
by A221, A222, FINSEQ_1:1;
then A224:
n in dom q1
by FINSEQ_1:def 3;
upper_bound (divset (D1,(k + 1))) = D1 . (k + 1)
by A103, A107, Def3;
then
divset (
D1,
(k + 1))
= [.(D1 . k),(D1 . (k + 1)).]
by A220, Th2;
then A225:
(upper_volume (g,MD1)) . n = (upper_bound (rng (g | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1))))
by A214, A223, A224, A219, A220, Def5;
((upper_volume (f,D1)) | (k + 1)) . (k + 1) =
((upper_volume (f,D1)) | (Seg (k + 1))) . (k + 1)
by FINSEQ_1:def 15
.=
(upper_volume (f,D1)) . (k + 1)
by A216, FUNCT_1:47
;
then q1 . n =
(upper_volume (f,D1)) . (k + 1)
by A110, A112, A223, A224, FINSEQ_1:def 7
.=
(upper_bound (rng (f | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1))))
by A103, Def5
;
hence
q1 . n = (upper_volume (g,MD1)) . n
by A225;
verum
end;
len q1 = len (upper_volume (g,MD1))
by A111, A213, Def5;
then A226:
q1 = upper_volume (
g,
MD1)
by A215, FINSEQ_1:14;
dom g = (dom f) /\ (divset (D1,(k + 1)))
by RELAT_1:61;
then
dom g = A /\ (divset (D1,(k + 1)))
by FUNCT_2:def 1;
then
dom g = divset (
D1,
(k + 1))
by A103, Th6, XBOOLE_1:28;
then A227:
g is
total
by PARTFUN1:def 2;
len MD1 = ((k + 1) -' (k + 1)) + 1
by A105, A106, FINSEQ_6:118;
then
len MD1 = ((k + 1) - (k + 1)) + 1
by XREAL_1:233;
then A228:
upper_sum (
g,
MD1)
>= upper_sum (
g,
MD2)
by A208, A227, Th28;
len (upper_volume (g,MD2)) =
len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1)))))
by Def5
.=
(indx (D2,D1,(k + 1))) - (indx (D2,D1,k))
by A130, A161, A167, A168, A164, A170, FINSEQ_6:118
;
hence
Sum q1 >= Sum q2
by A143, A226, A171, A228, FINSEQ_1:14;
verum
end;
Sum ((upper_volume (f,D1)) | (k + 1)) = (Sum p1) + (Sum q1)
by A112, RVSUM_1:75;
then
Sum q1 = (Sum ((upper_volume (f,D1)) | (k + 1))) - (Sum p1)
;
then
Sum ((upper_volume (f,D1)) | (k + 1)) >= (Sum q2) + (Sum p1)
by A163, XREAL_1:19;
then
(Sum ((upper_volume (f,D1)) | (k + 1))) - (Sum q2) >= Sum p1
by XREAL_1:19;
then
(Sum ((upper_volume (f,D1)) | (k + 1))) - (Sum q2) >= Sum p2
by A102, A131, A127, A160, FINSEQ_1:def 3, XXREAL_0:2;
hence
Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
by A147, XREAL_1:19;
verum end; end; end;
hence
Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
;
verum
end;
thus
for
k being non
zero Nat holds
S1[
k]
from NAT_1:sch 10(A3, A101); verum
end;
hence
for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
; verum