Step |
Hyp |
Ref |
Expression |
1 |
|
uniioombl.1 |
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
2 |
|
uniioombl.2 |
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) ) |
3 |
|
uniioombl.3 |
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) ) |
4 |
|
uniioombl.a |
|- A = U. ran ( (,) o. F ) |
5 |
|
uniioombl.e |
|- ( ph -> ( vol* ` E ) e. RR ) |
6 |
|
uniioombl.c |
|- ( ph -> C e. RR+ ) |
7 |
|
uniioombl.g |
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
8 |
|
uniioombl.s |
|- ( ph -> E C_ U. ran ( (,) o. G ) ) |
9 |
|
uniioombl.t |
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) ) |
10 |
|
uniioombl.v |
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) ) |
11 |
|
uniioombl.m |
|- ( ph -> M e. NN ) |
12 |
|
uniioombl.m2 |
|- ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C ) |
13 |
|
uniioombl.k |
|- K = U. ( ( (,) o. G ) " ( 1 ... M ) ) |
14 |
|
inss1 |
|- ( E i^i A ) C_ E |
15 |
14
|
a1i |
|- ( ph -> ( E i^i A ) C_ E ) |
16 |
7
|
uniiccdif |
|- ( ph -> ( U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) /\ ( vol* ` ( U. ran ( [,] o. G ) \ U. ran ( (,) o. G ) ) ) = 0 ) ) |
17 |
16
|
simpld |
|- ( ph -> U. ran ( (,) o. G ) C_ U. ran ( [,] o. G ) ) |
18 |
|
ovolficcss |
|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. G ) C_ RR ) |
19 |
7 18
|
syl |
|- ( ph -> U. ran ( [,] o. G ) C_ RR ) |
20 |
17 19
|
sstrd |
|- ( ph -> U. ran ( (,) o. G ) C_ RR ) |
21 |
8 20
|
sstrd |
|- ( ph -> E C_ RR ) |
22 |
|
ovolsscl |
|- ( ( ( E i^i A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i A ) ) e. RR ) |
23 |
15 21 5 22
|
syl3anc |
|- ( ph -> ( vol* ` ( E i^i A ) ) e. RR ) |
24 |
|
difssd |
|- ( ph -> ( E \ A ) C_ E ) |
25 |
|
ovolsscl |
|- ( ( ( E \ A ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ A ) ) e. RR ) |
26 |
24 21 5 25
|
syl3anc |
|- ( ph -> ( vol* ` ( E \ A ) ) e. RR ) |
27 |
|
inss1 |
|- ( K i^i A ) C_ K |
28 |
27
|
a1i |
|- ( ph -> ( K i^i A ) C_ K ) |
29 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
uniioombllem3a |
|- ( ph -> ( K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) /\ ( vol* ` K ) e. RR ) ) |
30 |
29
|
simpld |
|- ( ph -> K = U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) ) |
31 |
|
inss2 |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) |
32 |
|
elfznn |
|- ( j e. ( 1 ... M ) -> j e. NN ) |
33 |
|
ffvelrn |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) ) |
34 |
7 32 33
|
syl2an |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( <_ i^i ( RR X. RR ) ) ) |
35 |
31 34
|
sseldi |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) e. ( RR X. RR ) ) |
36 |
|
1st2nd2 |
|- ( ( G ` j ) e. ( RR X. RR ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) |
37 |
35 36
|
syl |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( G ` j ) = <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) |
38 |
37
|
fveq2d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) ) |
39 |
|
df-ov |
|- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) = ( (,) ` <. ( 1st ` ( G ` j ) ) , ( 2nd ` ( G ` j ) ) >. ) |
40 |
38 39
|
eqtr4di |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) = ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) ) |
41 |
|
ioossre |
|- ( ( 1st ` ( G ` j ) ) (,) ( 2nd ` ( G ` j ) ) ) C_ RR |
42 |
40 41
|
eqsstrdi |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( (,) ` ( G ` j ) ) C_ RR ) |
43 |
42
|
ralrimiva |
|- ( ph -> A. j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR ) |
44 |
|
iunss |
|- ( U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR <-> A. j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR ) |
45 |
43 44
|
sylibr |
|- ( ph -> U_ j e. ( 1 ... M ) ( (,) ` ( G ` j ) ) C_ RR ) |
46 |
30 45
|
eqsstrd |
|- ( ph -> K C_ RR ) |
47 |
29
|
simprd |
|- ( ph -> ( vol* ` K ) e. RR ) |
48 |
|
ovolsscl |
|- ( ( ( K i^i A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K i^i A ) ) e. RR ) |
49 |
28 46 47 48
|
syl3anc |
|- ( ph -> ( vol* ` ( K i^i A ) ) e. RR ) |
50 |
6
|
rpred |
|- ( ph -> C e. RR ) |
51 |
49 50
|
readdcld |
|- ( ph -> ( ( vol* ` ( K i^i A ) ) + C ) e. RR ) |
52 |
|
difssd |
|- ( ph -> ( K \ A ) C_ K ) |
53 |
|
ovolsscl |
|- ( ( ( K \ A ) C_ K /\ K C_ RR /\ ( vol* ` K ) e. RR ) -> ( vol* ` ( K \ A ) ) e. RR ) |
54 |
52 46 47 53
|
syl3anc |
|- ( ph -> ( vol* ` ( K \ A ) ) e. RR ) |
55 |
54 50
|
readdcld |
|- ( ph -> ( ( vol* ` ( K \ A ) ) + C ) e. RR ) |
56 |
|
ssun2 |
|- U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
57 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
58 |
|
rexpssxrxp |
|- ( RR X. RR ) C_ ( RR* X. RR* ) |
59 |
31 58
|
sstri |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) |
60 |
|
fss |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> G : NN --> ( RR* X. RR* ) ) |
61 |
7 59 60
|
sylancl |
|- ( ph -> G : NN --> ( RR* X. RR* ) ) |
62 |
|
fco |
|- ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ G : NN --> ( RR* X. RR* ) ) -> ( (,) o. G ) : NN --> ~P RR ) |
63 |
57 61 62
|
sylancr |
|- ( ph -> ( (,) o. G ) : NN --> ~P RR ) |
64 |
63
|
ffnd |
|- ( ph -> ( (,) o. G ) Fn NN ) |
65 |
|
fnima |
|- ( ( (,) o. G ) Fn NN -> ( ( (,) o. G ) " NN ) = ran ( (,) o. G ) ) |
66 |
64 65
|
syl |
|- ( ph -> ( ( (,) o. G ) " NN ) = ran ( (,) o. G ) ) |
67 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
68 |
11
|
peano2nnd |
|- ( ph -> ( M + 1 ) e. NN ) |
69 |
68 67
|
eleqtrdi |
|- ( ph -> ( M + 1 ) e. ( ZZ>= ` 1 ) ) |
70 |
|
uzsplit |
|- ( ( M + 1 ) e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) ) |
71 |
69 70
|
syl |
|- ( ph -> ( ZZ>= ` 1 ) = ( ( 1 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) ) |
72 |
67 71
|
syl5eq |
|- ( ph -> NN = ( ( 1 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) ) |
73 |
11
|
nncnd |
|- ( ph -> M e. CC ) |
74 |
|
ax-1cn |
|- 1 e. CC |
75 |
|
pncan |
|- ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M ) |
76 |
73 74 75
|
sylancl |
|- ( ph -> ( ( M + 1 ) - 1 ) = M ) |
77 |
76
|
oveq2d |
|- ( ph -> ( 1 ... ( ( M + 1 ) - 1 ) ) = ( 1 ... M ) ) |
78 |
77
|
uneq1d |
|- ( ph -> ( ( 1 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) ) |
79 |
72 78
|
eqtrd |
|- ( ph -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) ) |
80 |
79
|
imaeq2d |
|- ( ph -> ( ( (,) o. G ) " NN ) = ( ( (,) o. G ) " ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) ) ) |
81 |
66 80
|
eqtr3d |
|- ( ph -> ran ( (,) o. G ) = ( ( (,) o. G ) " ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) ) ) |
82 |
|
imaundi |
|- ( ( (,) o. G ) " ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) ) = ( ( ( (,) o. G ) " ( 1 ... M ) ) u. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
83 |
81 82
|
eqtrdi |
|- ( ph -> ran ( (,) o. G ) = ( ( ( (,) o. G ) " ( 1 ... M ) ) u. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
84 |
83
|
unieqd |
|- ( ph -> U. ran ( (,) o. G ) = U. ( ( ( (,) o. G ) " ( 1 ... M ) ) u. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
85 |
|
uniun |
|- U. ( ( ( (,) o. G ) " ( 1 ... M ) ) u. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) = ( U. ( ( (,) o. G ) " ( 1 ... M ) ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
86 |
84 85
|
eqtrdi |
|- ( ph -> U. ran ( (,) o. G ) = ( U. ( ( (,) o. G ) " ( 1 ... M ) ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
87 |
13
|
uneq1i |
|- ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) = ( U. ( ( (,) o. G ) " ( 1 ... M ) ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
88 |
86 87
|
eqtr4di |
|- ( ph -> U. ran ( (,) o. G ) = ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
89 |
56 88
|
sseqtrrid |
|- ( ph -> U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ U. ran ( (,) o. G ) ) |
90 |
1 2 3 4 5 6 7 8 9 10
|
uniioombllem1 |
|- ( ph -> sup ( ran T , RR* , < ) e. RR ) |
91 |
|
ssid |
|- U. ran ( (,) o. G ) C_ U. ran ( (,) o. G ) |
92 |
9
|
ovollb |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. G ) C_ U. ran ( (,) o. G ) ) -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) |
93 |
7 91 92
|
sylancl |
|- ( ph -> ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) |
94 |
|
ovollecl |
|- ( ( U. ran ( (,) o. G ) C_ RR /\ sup ( ran T , RR* , < ) e. RR /\ ( vol* ` U. ran ( (,) o. G ) ) <_ sup ( ran T , RR* , < ) ) -> ( vol* ` U. ran ( (,) o. G ) ) e. RR ) |
95 |
20 90 93 94
|
syl3anc |
|- ( ph -> ( vol* ` U. ran ( (,) o. G ) ) e. RR ) |
96 |
|
ovolsscl |
|- ( ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol* ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) e. RR ) |
97 |
89 20 95 96
|
syl3anc |
|- ( ph -> ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) e. RR ) |
98 |
49 97
|
readdcld |
|- ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) e. RR ) |
99 |
|
unss1 |
|- ( ( K i^i A ) C_ K -> ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
100 |
27 99
|
ax-mp |
|- ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
101 |
100 88
|
sseqtrrid |
|- ( ph -> ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ U. ran ( (,) o. G ) ) |
102 |
|
ovolsscl |
|- ( ( ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol* ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol* ` ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) e. RR ) |
103 |
101 20 95 102
|
syl3anc |
|- ( ph -> ( vol* ` ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) e. RR ) |
104 |
8 88
|
sseqtrd |
|- ( ph -> E C_ ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
105 |
104
|
ssrind |
|- ( ph -> ( E i^i A ) C_ ( ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) i^i A ) ) |
106 |
|
indir |
|- ( ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) i^i A ) = ( ( K i^i A ) u. ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) i^i A ) ) |
107 |
|
inss1 |
|- ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) i^i A ) C_ U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) |
108 |
|
unss2 |
|- ( ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) i^i A ) C_ U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) -> ( ( K i^i A ) u. ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) i^i A ) ) C_ ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
109 |
107 108
|
ax-mp |
|- ( ( K i^i A ) u. ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) i^i A ) ) C_ ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
110 |
106 109
|
eqsstri |
|- ( ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) i^i A ) C_ ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
111 |
105 110
|
sstrdi |
|- ( ph -> ( E i^i A ) C_ ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
112 |
101 20
|
sstrd |
|- ( ph -> ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ RR ) |
113 |
|
ovolss |
|- ( ( ( E i^i A ) C_ ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) /\ ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ RR ) -> ( vol* ` ( E i^i A ) ) <_ ( vol* ` ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
114 |
111 112 113
|
syl2anc |
|- ( ph -> ( vol* ` ( E i^i A ) ) <_ ( vol* ` ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
115 |
28 46
|
sstrd |
|- ( ph -> ( K i^i A ) C_ RR ) |
116 |
89 20
|
sstrd |
|- ( ph -> U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ RR ) |
117 |
|
ovolun |
|- ( ( ( ( K i^i A ) C_ RR /\ ( vol* ` ( K i^i A ) ) e. RR ) /\ ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ RR /\ ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) e. RR ) ) -> ( vol* ` ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) <_ ( ( vol* ` ( K i^i A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
118 |
115 49 116 97 117
|
syl22anc |
|- ( ph -> ( vol* ` ( ( K i^i A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) <_ ( ( vol* ` ( K i^i A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
119 |
23 103 98 114 118
|
letrd |
|- ( ph -> ( vol* ` ( E i^i A ) ) <_ ( ( vol* ` ( K i^i A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
120 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
121 |
|
eqid |
|- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G ) |
122 |
121 9
|
ovolsf |
|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) ) |
123 |
7 122
|
syl |
|- ( ph -> T : NN --> ( 0 [,) +oo ) ) |
124 |
123 11
|
ffvelrnd |
|- ( ph -> ( T ` M ) e. ( 0 [,) +oo ) ) |
125 |
120 124
|
sseldi |
|- ( ph -> ( T ` M ) e. RR ) |
126 |
90 125
|
resubcld |
|- ( ph -> ( sup ( ran T , RR* , < ) - ( T ` M ) ) e. RR ) |
127 |
97
|
rexrd |
|- ( ph -> ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) e. RR* ) |
128 |
|
id |
|- ( z e. NN -> z e. NN ) |
129 |
|
nnaddcl |
|- ( ( z e. NN /\ M e. NN ) -> ( z + M ) e. NN ) |
130 |
128 11 129
|
syl2anr |
|- ( ( ph /\ z e. NN ) -> ( z + M ) e. NN ) |
131 |
7
|
ffvelrnda |
|- ( ( ph /\ ( z + M ) e. NN ) -> ( G ` ( z + M ) ) e. ( <_ i^i ( RR X. RR ) ) ) |
132 |
130 131
|
syldan |
|- ( ( ph /\ z e. NN ) -> ( G ` ( z + M ) ) e. ( <_ i^i ( RR X. RR ) ) ) |
133 |
132
|
fmpttd |
|- ( ph -> ( z e. NN |-> ( G ` ( z + M ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) ) |
134 |
|
eqid |
|- ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) = ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) |
135 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) |
136 |
134 135
|
ovolsf |
|- ( ( z e. NN |-> ( G ` ( z + M ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) : NN --> ( 0 [,) +oo ) ) |
137 |
133 136
|
syl |
|- ( ph -> seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) : NN --> ( 0 [,) +oo ) ) |
138 |
137
|
frnd |
|- ( ph -> ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) C_ ( 0 [,) +oo ) ) |
139 |
|
icossxr |
|- ( 0 [,) +oo ) C_ RR* |
140 |
138 139
|
sstrdi |
|- ( ph -> ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) C_ RR* ) |
141 |
|
supxrcl |
|- ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) , RR* , < ) e. RR* ) |
142 |
140 141
|
syl |
|- ( ph -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) , RR* , < ) e. RR* ) |
143 |
126
|
rexrd |
|- ( ph -> ( sup ( ran T , RR* , < ) - ( T ` M ) ) e. RR* ) |
144 |
|
1zzd |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> 1 e. ZZ ) |
145 |
11
|
nnzd |
|- ( ph -> M e. ZZ ) |
146 |
145
|
adantr |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> M e. ZZ ) |
147 |
|
addcom |
|- ( ( M e. CC /\ 1 e. CC ) -> ( M + 1 ) = ( 1 + M ) ) |
148 |
73 74 147
|
sylancl |
|- ( ph -> ( M + 1 ) = ( 1 + M ) ) |
149 |
148
|
fveq2d |
|- ( ph -> ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` ( 1 + M ) ) ) |
150 |
149
|
eleq2d |
|- ( ph -> ( x e. ( ZZ>= ` ( M + 1 ) ) <-> x e. ( ZZ>= ` ( 1 + M ) ) ) ) |
151 |
150
|
biimpa |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x e. ( ZZ>= ` ( 1 + M ) ) ) |
152 |
|
eluzsub |
|- ( ( 1 e. ZZ /\ M e. ZZ /\ x e. ( ZZ>= ` ( 1 + M ) ) ) -> ( x - M ) e. ( ZZ>= ` 1 ) ) |
153 |
144 146 151 152
|
syl3anc |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( x - M ) e. ( ZZ>= ` 1 ) ) |
154 |
153 67
|
eleqtrrdi |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( x - M ) e. NN ) |
155 |
|
eluzelz |
|- ( x e. ( ZZ>= ` ( M + 1 ) ) -> x e. ZZ ) |
156 |
155
|
adantl |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x e. ZZ ) |
157 |
156
|
zcnd |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x e. CC ) |
158 |
73
|
adantr |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> M e. CC ) |
159 |
157 158
|
npcand |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( x - M ) + M ) = x ) |
160 |
159
|
eqcomd |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x = ( ( x - M ) + M ) ) |
161 |
|
oveq1 |
|- ( z = ( x - M ) -> ( z + M ) = ( ( x - M ) + M ) ) |
162 |
161
|
rspceeqv |
|- ( ( ( x - M ) e. NN /\ x = ( ( x - M ) + M ) ) -> E. z e. NN x = ( z + M ) ) |
163 |
154 160 162
|
syl2anc |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> E. z e. NN x = ( z + M ) ) |
164 |
|
eqid |
|- ( z e. NN |-> ( z + M ) ) = ( z e. NN |-> ( z + M ) ) |
165 |
164
|
elrnmpt |
|- ( x e. _V -> ( x e. ran ( z e. NN |-> ( z + M ) ) <-> E. z e. NN x = ( z + M ) ) ) |
166 |
165
|
elv |
|- ( x e. ran ( z e. NN |-> ( z + M ) ) <-> E. z e. NN x = ( z + M ) ) |
167 |
163 166
|
sylibr |
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> x e. ran ( z e. NN |-> ( z + M ) ) ) |
168 |
167
|
ex |
|- ( ph -> ( x e. ( ZZ>= ` ( M + 1 ) ) -> x e. ran ( z e. NN |-> ( z + M ) ) ) ) |
169 |
168
|
ssrdv |
|- ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ ran ( z e. NN |-> ( z + M ) ) ) |
170 |
|
imass2 |
|- ( ( ZZ>= ` ( M + 1 ) ) C_ ran ( z e. NN |-> ( z + M ) ) -> ( G " ( ZZ>= ` ( M + 1 ) ) ) C_ ( G " ran ( z e. NN |-> ( z + M ) ) ) ) |
171 |
169 170
|
syl |
|- ( ph -> ( G " ( ZZ>= ` ( M + 1 ) ) ) C_ ( G " ran ( z e. NN |-> ( z + M ) ) ) ) |
172 |
|
rnco2 |
|- ran ( G o. ( z e. NN |-> ( z + M ) ) ) = ( G " ran ( z e. NN |-> ( z + M ) ) ) |
173 |
7 130
|
cofmpt |
|- ( ph -> ( G o. ( z e. NN |-> ( z + M ) ) ) = ( z e. NN |-> ( G ` ( z + M ) ) ) ) |
174 |
173
|
rneqd |
|- ( ph -> ran ( G o. ( z e. NN |-> ( z + M ) ) ) = ran ( z e. NN |-> ( G ` ( z + M ) ) ) ) |
175 |
172 174
|
syl5eqr |
|- ( ph -> ( G " ran ( z e. NN |-> ( z + M ) ) ) = ran ( z e. NN |-> ( G ` ( z + M ) ) ) ) |
176 |
171 175
|
sseqtrd |
|- ( ph -> ( G " ( ZZ>= ` ( M + 1 ) ) ) C_ ran ( z e. NN |-> ( G ` ( z + M ) ) ) ) |
177 |
|
imass2 |
|- ( ( G " ( ZZ>= ` ( M + 1 ) ) ) C_ ran ( z e. NN |-> ( G ` ( z + M ) ) ) -> ( (,) " ( G " ( ZZ>= ` ( M + 1 ) ) ) ) C_ ( (,) " ran ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) |
178 |
176 177
|
syl |
|- ( ph -> ( (,) " ( G " ( ZZ>= ` ( M + 1 ) ) ) ) C_ ( (,) " ran ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) |
179 |
|
imaco |
|- ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) = ( (,) " ( G " ( ZZ>= ` ( M + 1 ) ) ) ) |
180 |
|
rnco2 |
|- ran ( (,) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) = ( (,) " ran ( z e. NN |-> ( G ` ( z + M ) ) ) ) |
181 |
178 179 180
|
3sstr4g |
|- ( ph -> ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ ran ( (,) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) |
182 |
181
|
unissd |
|- ( ph -> U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ U. ran ( (,) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) |
183 |
135
|
ovollb |
|- ( ( ( z e. NN |-> ( G ` ( z + M ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ U. ran ( (,) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) -> ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) , RR* , < ) ) |
184 |
133 182 183
|
syl2anc |
|- ( ph -> ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) , RR* , < ) ) |
185 |
123
|
frnd |
|- ( ph -> ran T C_ ( 0 [,) +oo ) ) |
186 |
185 139
|
sstrdi |
|- ( ph -> ran T C_ RR* ) |
187 |
9
|
fveq1i |
|- ( T ` ( M + n ) ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( M + n ) ) |
188 |
11
|
nnred |
|- ( ph -> M e. RR ) |
189 |
188
|
ltp1d |
|- ( ph -> M < ( M + 1 ) ) |
190 |
|
fzdisj |
|- ( M < ( M + 1 ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... ( M + n ) ) ) = (/) ) |
191 |
189 190
|
syl |
|- ( ph -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... ( M + n ) ) ) = (/) ) |
192 |
191
|
adantr |
|- ( ( ph /\ n e. NN ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... ( M + n ) ) ) = (/) ) |
193 |
|
nnnn0 |
|- ( n e. NN -> n e. NN0 ) |
194 |
|
nn0addge1 |
|- ( ( M e. RR /\ n e. NN0 ) -> M <_ ( M + n ) ) |
195 |
188 193 194
|
syl2an |
|- ( ( ph /\ n e. NN ) -> M <_ ( M + n ) ) |
196 |
11
|
adantr |
|- ( ( ph /\ n e. NN ) -> M e. NN ) |
197 |
196 67
|
eleqtrdi |
|- ( ( ph /\ n e. NN ) -> M e. ( ZZ>= ` 1 ) ) |
198 |
|
nnaddcl |
|- ( ( M e. NN /\ n e. NN ) -> ( M + n ) e. NN ) |
199 |
11 198
|
sylan |
|- ( ( ph /\ n e. NN ) -> ( M + n ) e. NN ) |
200 |
199
|
nnzd |
|- ( ( ph /\ n e. NN ) -> ( M + n ) e. ZZ ) |
201 |
|
elfz5 |
|- ( ( M e. ( ZZ>= ` 1 ) /\ ( M + n ) e. ZZ ) -> ( M e. ( 1 ... ( M + n ) ) <-> M <_ ( M + n ) ) ) |
202 |
197 200 201
|
syl2anc |
|- ( ( ph /\ n e. NN ) -> ( M e. ( 1 ... ( M + n ) ) <-> M <_ ( M + n ) ) ) |
203 |
195 202
|
mpbird |
|- ( ( ph /\ n e. NN ) -> M e. ( 1 ... ( M + n ) ) ) |
204 |
|
fzsplit |
|- ( M e. ( 1 ... ( M + n ) ) -> ( 1 ... ( M + n ) ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... ( M + n ) ) ) ) |
205 |
203 204
|
syl |
|- ( ( ph /\ n e. NN ) -> ( 1 ... ( M + n ) ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... ( M + n ) ) ) ) |
206 |
|
fzfid |
|- ( ( ph /\ n e. NN ) -> ( 1 ... ( M + n ) ) e. Fin ) |
207 |
7
|
adantr |
|- ( ( ph /\ n e. NN ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
208 |
|
elfznn |
|- ( j e. ( 1 ... ( M + n ) ) -> j e. NN ) |
209 |
|
ovolfcl |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) ) |
210 |
207 208 209
|
syl2an |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... ( M + n ) ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) ) |
211 |
210
|
simp2d |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... ( M + n ) ) ) -> ( 2nd ` ( G ` j ) ) e. RR ) |
212 |
210
|
simp1d |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... ( M + n ) ) ) -> ( 1st ` ( G ` j ) ) e. RR ) |
213 |
211 212
|
resubcld |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... ( M + n ) ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR ) |
214 |
213
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... ( M + n ) ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. CC ) |
215 |
192 205 206 214
|
fsumsplit |
|- ( ( ph /\ n e. NN ) -> sum_ j e. ( 1 ... ( M + n ) ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) = ( sum_ j e. ( 1 ... M ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) + sum_ j e. ( ( M + 1 ) ... ( M + n ) ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) ) |
216 |
121
|
ovolfsval |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ j e. NN ) -> ( ( ( abs o. - ) o. G ) ` j ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) |
217 |
207 208 216
|
syl2an |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... ( M + n ) ) ) -> ( ( ( abs o. - ) o. G ) ` j ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) |
218 |
199 67
|
eleqtrdi |
|- ( ( ph /\ n e. NN ) -> ( M + n ) e. ( ZZ>= ` 1 ) ) |
219 |
217 218 214
|
fsumser |
|- ( ( ph /\ n e. NN ) -> sum_ j e. ( 1 ... ( M + n ) ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( M + n ) ) ) |
220 |
7
|
ad2antrr |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... M ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
221 |
32
|
adantl |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... M ) ) -> j e. NN ) |
222 |
220 221 216
|
syl2anc |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... M ) ) -> ( ( ( abs o. - ) o. G ) ` j ) = ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) |
223 |
7 32 209
|
syl2an |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) ) |
224 |
223
|
simp2d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 2nd ` ( G ` j ) ) e. RR ) |
225 |
223
|
simp1d |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1st ` ( G ` j ) ) e. RR ) |
226 |
224 225
|
resubcld |
|- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR ) |
227 |
226
|
adantlr |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR ) |
228 |
227
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( 1 ... M ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. CC ) |
229 |
222 197 228
|
fsumser |
|- ( ( ph /\ n e. NN ) -> sum_ j e. ( 1 ... M ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` M ) ) |
230 |
9
|
fveq1i |
|- ( T ` M ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` M ) |
231 |
229 230
|
eqtr4di |
|- ( ( ph /\ n e. NN ) -> sum_ j e. ( 1 ... M ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) = ( T ` M ) ) |
232 |
196
|
nnzd |
|- ( ( ph /\ n e. NN ) -> M e. ZZ ) |
233 |
232
|
peano2zd |
|- ( ( ph /\ n e. NN ) -> ( M + 1 ) e. ZZ ) |
234 |
7
|
ad2antrr |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( ( M + 1 ) ... ( M + n ) ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
235 |
196
|
peano2nnd |
|- ( ( ph /\ n e. NN ) -> ( M + 1 ) e. NN ) |
236 |
|
elfzuz |
|- ( j e. ( ( M + 1 ) ... ( M + n ) ) -> j e. ( ZZ>= ` ( M + 1 ) ) ) |
237 |
|
eluznn |
|- ( ( ( M + 1 ) e. NN /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. NN ) |
238 |
235 236 237
|
syl2an |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( ( M + 1 ) ... ( M + n ) ) ) -> j e. NN ) |
239 |
234 238 209
|
syl2anc |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( ( M + 1 ) ... ( M + n ) ) ) -> ( ( 1st ` ( G ` j ) ) e. RR /\ ( 2nd ` ( G ` j ) ) e. RR /\ ( 1st ` ( G ` j ) ) <_ ( 2nd ` ( G ` j ) ) ) ) |
240 |
239
|
simp2d |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( ( M + 1 ) ... ( M + n ) ) ) -> ( 2nd ` ( G ` j ) ) e. RR ) |
241 |
239
|
simp1d |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( ( M + 1 ) ... ( M + n ) ) ) -> ( 1st ` ( G ` j ) ) e. RR ) |
242 |
240 241
|
resubcld |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( ( M + 1 ) ... ( M + n ) ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. RR ) |
243 |
242
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ j e. ( ( M + 1 ) ... ( M + n ) ) ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) e. CC ) |
244 |
|
2fveq3 |
|- ( j = ( k + M ) -> ( 2nd ` ( G ` j ) ) = ( 2nd ` ( G ` ( k + M ) ) ) ) |
245 |
|
2fveq3 |
|- ( j = ( k + M ) -> ( 1st ` ( G ` j ) ) = ( 1st ` ( G ` ( k + M ) ) ) ) |
246 |
244 245
|
oveq12d |
|- ( j = ( k + M ) -> ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) = ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) ) |
247 |
232 233 200 243 246
|
fsumshftm |
|- ( ( ph /\ n e. NN ) -> sum_ j e. ( ( M + 1 ) ... ( M + n ) ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) = sum_ k e. ( ( ( M + 1 ) - M ) ... ( ( M + n ) - M ) ) ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) ) |
248 |
196
|
nncnd |
|- ( ( ph /\ n e. NN ) -> M e. CC ) |
249 |
|
pncan2 |
|- ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - M ) = 1 ) |
250 |
248 74 249
|
sylancl |
|- ( ( ph /\ n e. NN ) -> ( ( M + 1 ) - M ) = 1 ) |
251 |
|
nncn |
|- ( n e. NN -> n e. CC ) |
252 |
251
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. CC ) |
253 |
248 252
|
pncan2d |
|- ( ( ph /\ n e. NN ) -> ( ( M + n ) - M ) = n ) |
254 |
250 253
|
oveq12d |
|- ( ( ph /\ n e. NN ) -> ( ( ( M + 1 ) - M ) ... ( ( M + n ) - M ) ) = ( 1 ... n ) ) |
255 |
254
|
sumeq1d |
|- ( ( ph /\ n e. NN ) -> sum_ k e. ( ( ( M + 1 ) - M ) ... ( ( M + n ) - M ) ) ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) = sum_ k e. ( 1 ... n ) ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) ) |
256 |
133
|
adantr |
|- ( ( ph /\ n e. NN ) -> ( z e. NN |-> ( G ` ( z + M ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) ) |
257 |
|
elfznn |
|- ( k e. ( 1 ... n ) -> k e. NN ) |
258 |
134
|
ovolfsval |
|- ( ( ( z e. NN |-> ( G ` ( z + M ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) /\ k e. NN ) -> ( ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ` k ) = ( ( 2nd ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) - ( 1st ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) ) ) |
259 |
256 257 258
|
syl2an |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ` k ) = ( ( 2nd ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) - ( 1st ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) ) ) |
260 |
257
|
adantl |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN ) |
261 |
|
fvoveq1 |
|- ( z = k -> ( G ` ( z + M ) ) = ( G ` ( k + M ) ) ) |
262 |
|
eqid |
|- ( z e. NN |-> ( G ` ( z + M ) ) ) = ( z e. NN |-> ( G ` ( z + M ) ) ) |
263 |
|
fvex |
|- ( G ` ( k + M ) ) e. _V |
264 |
261 262 263
|
fvmpt |
|- ( k e. NN -> ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) = ( G ` ( k + M ) ) ) |
265 |
260 264
|
syl |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) = ( G ` ( k + M ) ) ) |
266 |
265
|
fveq2d |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( 2nd ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) = ( 2nd ` ( G ` ( k + M ) ) ) ) |
267 |
265
|
fveq2d |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( 1st ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) = ( 1st ` ( G ` ( k + M ) ) ) ) |
268 |
266 267
|
oveq12d |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( 2nd ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) - ( 1st ` ( ( z e. NN |-> ( G ` ( z + M ) ) ) ` k ) ) ) = ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) ) |
269 |
259 268
|
eqtrd |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ` k ) = ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) ) |
270 |
|
simpr |
|- ( ( ph /\ n e. NN ) -> n e. NN ) |
271 |
270 67
|
eleqtrdi |
|- ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) ) |
272 |
7
|
ad2antrr |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
273 |
|
nnaddcl |
|- ( ( k e. NN /\ M e. NN ) -> ( k + M ) e. NN ) |
274 |
257 196 273
|
syl2anr |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( k + M ) e. NN ) |
275 |
|
ovolfcl |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( k + M ) e. NN ) -> ( ( 1st ` ( G ` ( k + M ) ) ) e. RR /\ ( 2nd ` ( G ` ( k + M ) ) ) e. RR /\ ( 1st ` ( G ` ( k + M ) ) ) <_ ( 2nd ` ( G ` ( k + M ) ) ) ) ) |
276 |
272 274 275
|
syl2anc |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( 1st ` ( G ` ( k + M ) ) ) e. RR /\ ( 2nd ` ( G ` ( k + M ) ) ) e. RR /\ ( 1st ` ( G ` ( k + M ) ) ) <_ ( 2nd ` ( G ` ( k + M ) ) ) ) ) |
277 |
276
|
simp2d |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( 2nd ` ( G ` ( k + M ) ) ) e. RR ) |
278 |
276
|
simp1d |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( 1st ` ( G ` ( k + M ) ) ) e. RR ) |
279 |
277 278
|
resubcld |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) e. RR ) |
280 |
279
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) e. CC ) |
281 |
269 271 280
|
fsumser |
|- ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) ( ( 2nd ` ( G ` ( k + M ) ) ) - ( 1st ` ( G ` ( k + M ) ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) |
282 |
247 255 281
|
3eqtrd |
|- ( ( ph /\ n e. NN ) -> sum_ j e. ( ( M + 1 ) ... ( M + n ) ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) |
283 |
231 282
|
oveq12d |
|- ( ( ph /\ n e. NN ) -> ( sum_ j e. ( 1 ... M ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) + sum_ j e. ( ( M + 1 ) ... ( M + n ) ) ( ( 2nd ` ( G ` j ) ) - ( 1st ` ( G ` j ) ) ) ) = ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) ) |
284 |
215 219 283
|
3eqtr3d |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( M + n ) ) = ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) ) |
285 |
187 284
|
syl5eq |
|- ( ( ph /\ n e. NN ) -> ( T ` ( M + n ) ) = ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) ) |
286 |
123
|
ffnd |
|- ( ph -> T Fn NN ) |
287 |
|
fnfvelrn |
|- ( ( T Fn NN /\ ( M + n ) e. NN ) -> ( T ` ( M + n ) ) e. ran T ) |
288 |
286 199 287
|
syl2an2r |
|- ( ( ph /\ n e. NN ) -> ( T ` ( M + n ) ) e. ran T ) |
289 |
285 288
|
eqeltrrd |
|- ( ( ph /\ n e. NN ) -> ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) e. ran T ) |
290 |
|
supxrub |
|- ( ( ran T C_ RR* /\ ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) e. ran T ) -> ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) <_ sup ( ran T , RR* , < ) ) |
291 |
186 289 290
|
syl2an2r |
|- ( ( ph /\ n e. NN ) -> ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) <_ sup ( ran T , RR* , < ) ) |
292 |
125
|
adantr |
|- ( ( ph /\ n e. NN ) -> ( T ` M ) e. RR ) |
293 |
137
|
ffvelrnda |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) e. ( 0 [,) +oo ) ) |
294 |
120 293
|
sseldi |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) e. RR ) |
295 |
90
|
adantr |
|- ( ( ph /\ n e. NN ) -> sup ( ran T , RR* , < ) e. RR ) |
296 |
292 294 295
|
leaddsub2d |
|- ( ( ph /\ n e. NN ) -> ( ( ( T ` M ) + ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) ) <_ sup ( ran T , RR* , < ) <-> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) ) |
297 |
291 296
|
mpbid |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) |
298 |
297
|
ralrimiva |
|- ( ph -> A. n e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) |
299 |
137
|
ffnd |
|- ( ph -> seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) Fn NN ) |
300 |
|
breq1 |
|- ( x = ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) -> ( x <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) <-> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) ) |
301 |
300
|
ralrn |
|- ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) Fn NN -> ( A. x e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) x <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) <-> A. n e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) ) |
302 |
299 301
|
syl |
|- ( ph -> ( A. x e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) x <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) <-> A. n e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) ) |
303 |
298 302
|
mpbird |
|- ( ph -> A. x e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) x <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) |
304 |
|
supxrleub |
|- ( ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) C_ RR* /\ ( sup ( ran T , RR* , < ) - ( T ` M ) ) e. RR* ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) , RR* , < ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) <-> A. x e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) x <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) ) |
305 |
140 143 304
|
syl2anc |
|- ( ph -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) , RR* , < ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) <-> A. x e. ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) x <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) ) |
306 |
303 305
|
mpbird |
|- ( ph -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) , RR* , < ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) |
307 |
127 142 143 184 306
|
xrletrd |
|- ( ph -> ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) <_ ( sup ( ran T , RR* , < ) - ( T ` M ) ) ) |
308 |
125 90 50
|
absdifltd |
|- ( ph -> ( ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C <-> ( ( sup ( ran T , RR* , < ) - C ) < ( T ` M ) /\ ( T ` M ) < ( sup ( ran T , RR* , < ) + C ) ) ) ) |
309 |
12 308
|
mpbid |
|- ( ph -> ( ( sup ( ran T , RR* , < ) - C ) < ( T ` M ) /\ ( T ` M ) < ( sup ( ran T , RR* , < ) + C ) ) ) |
310 |
309
|
simpld |
|- ( ph -> ( sup ( ran T , RR* , < ) - C ) < ( T ` M ) ) |
311 |
90 50 125 310
|
ltsub23d |
|- ( ph -> ( sup ( ran T , RR* , < ) - ( T ` M ) ) < C ) |
312 |
97 126 50 307 311
|
lelttrd |
|- ( ph -> ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) < C ) |
313 |
97 50 49 312
|
ltadd2dd |
|- ( ph -> ( ( vol* ` ( K i^i A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) < ( ( vol* ` ( K i^i A ) ) + C ) ) |
314 |
23 98 51 119 313
|
lelttrd |
|- ( ph -> ( vol* ` ( E i^i A ) ) < ( ( vol* ` ( K i^i A ) ) + C ) ) |
315 |
54 97
|
readdcld |
|- ( ph -> ( ( vol* ` ( K \ A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) e. RR ) |
316 |
|
difss |
|- ( K \ A ) C_ K |
317 |
|
unss1 |
|- ( ( K \ A ) C_ K -> ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
318 |
316 317
|
ax-mp |
|- ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
319 |
318 88
|
sseqtrrid |
|- ( ph -> ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ U. ran ( (,) o. G ) ) |
320 |
|
ovolsscl |
|- ( ( ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ U. ran ( (,) o. G ) /\ U. ran ( (,) o. G ) C_ RR /\ ( vol* ` U. ran ( (,) o. G ) ) e. RR ) -> ( vol* ` ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) e. RR ) |
321 |
319 20 95 320
|
syl3anc |
|- ( ph -> ( vol* ` ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) e. RR ) |
322 |
104
|
ssdifd |
|- ( ph -> ( E \ A ) C_ ( ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) \ A ) ) |
323 |
|
difundir |
|- ( ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) \ A ) = ( ( K \ A ) u. ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) \ A ) ) |
324 |
|
difss |
|- ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) \ A ) C_ U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) |
325 |
|
unss2 |
|- ( ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) \ A ) C_ U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) -> ( ( K \ A ) u. ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) \ A ) ) C_ ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
326 |
324 325
|
ax-mp |
|- ( ( K \ A ) u. ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) \ A ) ) C_ ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
327 |
323 326
|
eqsstri |
|- ( ( K u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) \ A ) C_ ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) |
328 |
322 327
|
sstrdi |
|- ( ph -> ( E \ A ) C_ ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) |
329 |
319 20
|
sstrd |
|- ( ph -> ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ RR ) |
330 |
|
ovolss |
|- ( ( ( E \ A ) C_ ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) /\ ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) C_ RR ) -> ( vol* ` ( E \ A ) ) <_ ( vol* ` ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
331 |
328 329 330
|
syl2anc |
|- ( ph -> ( vol* ` ( E \ A ) ) <_ ( vol* ` ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
332 |
52 46
|
sstrd |
|- ( ph -> ( K \ A ) C_ RR ) |
333 |
|
ovolun |
|- ( ( ( ( K \ A ) C_ RR /\ ( vol* ` ( K \ A ) ) e. RR ) /\ ( U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) C_ RR /\ ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) e. RR ) ) -> ( vol* ` ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) <_ ( ( vol* ` ( K \ A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
334 |
332 54 116 97 333
|
syl22anc |
|- ( ph -> ( vol* ` ( ( K \ A ) u. U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) <_ ( ( vol* ` ( K \ A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
335 |
26 321 315 331 334
|
letrd |
|- ( ph -> ( vol* ` ( E \ A ) ) <_ ( ( vol* ` ( K \ A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) ) |
336 |
97 50 54 312
|
ltadd2dd |
|- ( ph -> ( ( vol* ` ( K \ A ) ) + ( vol* ` U. ( ( (,) o. G ) " ( ZZ>= ` ( M + 1 ) ) ) ) ) < ( ( vol* ` ( K \ A ) ) + C ) ) |
337 |
26 315 55 335 336
|
lelttrd |
|- ( ph -> ( vol* ` ( E \ A ) ) < ( ( vol* ` ( K \ A ) ) + C ) ) |
338 |
23 26 51 55 314 337
|
lt2addd |
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) < ( ( ( vol* ` ( K i^i A ) ) + C ) + ( ( vol* ` ( K \ A ) ) + C ) ) ) |
339 |
49
|
recnd |
|- ( ph -> ( vol* ` ( K i^i A ) ) e. CC ) |
340 |
50
|
recnd |
|- ( ph -> C e. CC ) |
341 |
54
|
recnd |
|- ( ph -> ( vol* ` ( K \ A ) ) e. CC ) |
342 |
339 340 341 340
|
add4d |
|- ( ph -> ( ( ( vol* ` ( K i^i A ) ) + C ) + ( ( vol* ` ( K \ A ) ) + C ) ) = ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) ) |
343 |
338 342
|
breqtrd |
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) < ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) ) |