| 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 |
|
ffvelcdm |
|- ( ( 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
|
sselid |
|- ( ( 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
|
eqtrid |
|- ( 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
|
ffvelcdmd |
|- ( ph -> ( T ` M ) e. ( 0 [,) +oo ) ) |
| 125 |
120 124
|
sselid |
|- ( 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
|
ffvelcdmda |
|- ( ( 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
|
eqtr3id |
|- ( 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
|
eqtrid |
|- ( ( 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
|
ffvelcdmda |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( z e. NN |-> ( G ` ( z + M ) ) ) ) ) ` n ) e. ( 0 [,) +oo ) ) |
| 294 |
120 293
|
sselid |
|- ( ( 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 ) ) ) |