Metamath Proof Explorer

Theorem uniioombllem3

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2 
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
uniioombl.a 
|- A = U. ran ( (,) o. F )
uniioombl.e 
|- ( ph -> ( vol* ` E ) e. RR )
uniioombl.c 
|- ( ph -> C e. RR+ )
uniioombl.g 
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.s 
|- ( ph -> E C_ U. ran ( (,) o. G ) )
uniioombl.t 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
uniioombl.v 
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
uniioombl.m 
|- ( ph -> M e. NN )
uniioombl.m2 
|- ( ph -> ( abs ` ( ( T ` M ) - sup ( ran T , RR* , < ) ) ) < C )
uniioombl.k 
|- K = U. ( ( (,) o. G ) " ( 1 ... M ) )
Assertion uniioombllem3 
|- ( ph -> ( ( vol* ` ( E i^i A ) ) + ( vol* ` ( E \ A ) ) ) < ( ( ( vol* ` ( K i^i A ) ) + ( vol* ` ( K \ A ) ) ) + ( C + C ) ) )

Proof

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 ) ) )