Metamath Proof Explorer

Theorem ovoliunlem1

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypotheses ovoliun.t 
|- T = seq 1 ( + , G )
ovoliun.g 
|- G = ( n e. NN |-> ( vol* ` A ) )
ovoliun.a 
|- ( ( ph /\ n e. NN ) -> A C_ RR )
ovoliun.v 
|- ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
ovoliun.r 
|- ( ph -> sup ( ran T , RR* , < ) e. RR )
ovoliun.b 
|- ( ph -> B e. RR+ )
ovoliun.s 
|- S = seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) )
ovoliun.u 
|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ovoliun.h 
|- H = ( k e. NN |-> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) )
ovoliun.j 
|- ( ph -> J : NN -1-1-onto-> ( NN X. NN ) )
ovoliun.f 
|- ( ph -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovoliun.x1 
|- ( ( ph /\ n e. NN ) -> A C_ U. ran ( (,) o. ( F ` n ) ) )
ovoliun.x2 
|- ( ( ph /\ n e. NN ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
ovoliun.k 
|- ( ph -> K e. NN )
ovoliun.l1 
|- ( ph -> L e. ZZ )
ovoliun.l2 
|- ( ph -> A. w e. ( 1 ... K ) ( 1st ` ( J ` w ) ) <_ L )
Assertion ovoliunlem1 
|- ( ph -> ( U ` K ) <_ ( sup ( ran T , RR* , < ) + B ) )

Proof

Step Hyp Ref Expression
1 ovoliun.t 
 |-  T = seq 1 ( + , G )
2 ovoliun.g 
 |-  G = ( n e. NN |-> ( vol* ` A ) )
3 ovoliun.a 
 |-  ( ( ph /\ n e. NN ) -> A C_ RR )
4 ovoliun.v 
 |-  ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
5 ovoliun.r 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR )
6 ovoliun.b 
 |-  ( ph -> B e. RR+ )
7 ovoliun.s 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) )
8 ovoliun.u 
 |-  U = seq 1 ( + , ( ( abs o. - ) o. H ) )
9 ovoliun.h 
 |-  H = ( k e. NN |-> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) )
10 ovoliun.j 
 |-  ( ph -> J : NN -1-1-onto-> ( NN X. NN ) )
11 ovoliun.f 
 |-  ( ph -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
12 ovoliun.x1 
 |-  ( ( ph /\ n e. NN ) -> A C_ U. ran ( (,) o. ( F ` n ) ) )
13 ovoliun.x2 
 |-  ( ( ph /\ n e. NN ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
14 ovoliun.k 
 |-  ( ph -> K e. NN )
15 ovoliun.l1 
 |-  ( ph -> L e. ZZ )
16 ovoliun.l2 
 |-  ( ph -> A. w e. ( 1 ... K ) ( 1st ` ( J ` w ) ) <_ L )
17 2fveq3 
 |-  ( j = ( J ` m ) -> ( F ` ( 1st ` j ) ) = ( F ` ( 1st ` ( J ` m ) ) ) )
18 fveq2 
 |-  ( j = ( J ` m ) -> ( 2nd ` j ) = ( 2nd ` ( J ` m ) ) )
19 17 18 fveq12d 
 |-  ( j = ( J ` m ) -> ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) = ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) )
20 19 fveq2d 
 |-  ( j = ( J ` m ) -> ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) = ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) )
21 19 fveq2d 
 |-  ( j = ( J ` m ) -> ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) = ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) )
22 20 21 oveq12d 
 |-  ( j = ( J ` m ) -> ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) = ( ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) - ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) ) )
23 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
24 f1of1 
 |-  ( J : NN -1-1-onto-> ( NN X. NN ) -> J : NN -1-1-> ( NN X. NN ) )
25 10 24 syl 
 |-  ( ph -> J : NN -1-1-> ( NN X. NN ) )
26 fz1ssnn 
 |-  ( 1 ... K ) C_ NN
27 f1ores 
 |-  ( ( J : NN -1-1-> ( NN X. NN ) /\ ( 1 ... K ) C_ NN ) -> ( J |` ( 1 ... K ) ) : ( 1 ... K ) -1-1-onto-> ( J " ( 1 ... K ) ) )
28 25 26 27 sylancl 
 |-  ( ph -> ( J |` ( 1 ... K ) ) : ( 1 ... K ) -1-1-onto-> ( J " ( 1 ... K ) ) )
29 fvres 
 |-  ( m e. ( 1 ... K ) -> ( ( J |` ( 1 ... K ) ) ` m ) = ( J ` m ) )
30 29 adantl 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( ( J |` ( 1 ... K ) ) ` m ) = ( J ` m ) )
31 11 adantr 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
32 imassrn 
 |-  ( J " ( 1 ... K ) ) C_ ran J
33 f1of 
 |-  ( J : NN -1-1-onto-> ( NN X. NN ) -> J : NN --> ( NN X. NN ) )
34 10 33 syl 
 |-  ( ph -> J : NN --> ( NN X. NN ) )
35 34 frnd 
 |-  ( ph -> ran J C_ ( NN X. NN ) )
36 32 35 sstrid 
 |-  ( ph -> ( J " ( 1 ... K ) ) C_ ( NN X. NN ) )
37 36 sselda 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> j e. ( NN X. NN ) )
38 xp1st 
 |-  ( j e. ( NN X. NN ) -> ( 1st ` j ) e. NN )
39 37 38 syl 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( 1st ` j ) e. NN )
40 31 39 ffvelcdmd 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( F ` ( 1st ` j ) ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
41 elovolmlem 
 |-  ( ( F ` ( 1st ` j ) ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> ( F ` ( 1st ` j ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
42 40 41 sylib 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( F ` ( 1st ` j ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
43 xp2nd 
 |-  ( j e. ( NN X. NN ) -> ( 2nd ` j ) e. NN )
44 37 43 syl 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( 2nd ` j ) e. NN )
45 42 44 ffvelcdmd 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) e. ( <_ i^i ( RR X. RR ) ) )
46 45 elin2d 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) e. ( RR X. RR ) )
47 xp2nd 
 |-  ( ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) e. ( RR X. RR ) -> ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) e. RR )
48 46 47 syl 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) e. RR )
49 xp1st 
 |-  ( ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) e. ( RR X. RR ) -> ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) e. RR )
50 46 49 syl 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) e. RR )
51 48 50 resubcld 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) e. RR )
52 51 recnd 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) e. CC )
53 22 23 28 30 52 fsumf1o 
 |-  ( ph -> sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) = sum_ m e. ( 1 ... K ) ( ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) - ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) ) )
54 11 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
55 34 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( J ` k ) e. ( NN X. NN ) )
56 xp1st 
 |-  ( ( J ` k ) e. ( NN X. NN ) -> ( 1st ` ( J ` k ) ) e. NN )
57 55 56 syl 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( J ` k ) ) e. NN )
58 54 57 ffvelcdmd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( 1st ` ( J ` k ) ) ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
59 elovolmlem 
 |-  ( ( F ` ( 1st ` ( J ` k ) ) ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> ( F ` ( 1st ` ( J ` k ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
60 58 59 sylib 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( 1st ` ( J ` k ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
61 xp2nd 
 |-  ( ( J ` k ) e. ( NN X. NN ) -> ( 2nd ` ( J ` k ) ) e. NN )
62 55 61 syl 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( J ` k ) ) e. NN )
63 60 62 ffvelcdmd 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) e. ( <_ i^i ( RR X. RR ) ) )
64 63 9 fmptd 
 |-  ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
65 elfznn 
 |-  ( m e. ( 1 ... K ) -> m e. NN )
66 eqid 
 |-  ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
67 66 ovolfsval 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ m e. NN ) -> ( ( ( abs o. - ) o. H ) ` m ) = ( ( 2nd ` ( H ` m ) ) - ( 1st ` ( H ` m ) ) ) )
68 64 65 67 syl2an 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( ( ( abs o. - ) o. H ) ` m ) = ( ( 2nd ` ( H ` m ) ) - ( 1st ` ( H ` m ) ) ) )
69 65 adantl 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> m e. NN )
70 2fveq3 
 |-  ( k = m -> ( 1st ` ( J ` k ) ) = ( 1st ` ( J ` m ) ) )
71 70 fveq2d 
 |-  ( k = m -> ( F ` ( 1st ` ( J ` k ) ) ) = ( F ` ( 1st ` ( J ` m ) ) ) )
72 2fveq3 
 |-  ( k = m -> ( 2nd ` ( J ` k ) ) = ( 2nd ` ( J ` m ) ) )
73 71 72 fveq12d 
 |-  ( k = m -> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) = ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) )
74 fvex 
 |-  ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) e. _V
75 73 9 74 fvmpt 
 |-  ( m e. NN -> ( H ` m ) = ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) )
76 69 75 syl 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( H ` m ) = ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) )
77 76 fveq2d 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( 2nd ` ( H ` m ) ) = ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) )
78 76 fveq2d 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( 1st ` ( H ` m ) ) = ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) )
79 77 78 oveq12d 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( ( 2nd ` ( H ` m ) ) - ( 1st ` ( H ` m ) ) ) = ( ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) - ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) ) )
80 68 79 eqtrd 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( ( ( abs o. - ) o. H ) ` m ) = ( ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) - ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) ) )
81 nnuz 
 |-  NN = ( ZZ>= ` 1 )
82 14 81 eleqtrdi 
 |-  ( ph -> K e. ( ZZ>= ` 1 ) )
83 ffvelcdm 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ m e. NN ) -> ( H ` m ) e. ( <_ i^i ( RR X. RR ) ) )
84 64 65 83 syl2an 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( H ` m ) e. ( <_ i^i ( RR X. RR ) ) )
85 84 elin2d 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( H ` m ) e. ( RR X. RR ) )
86 xp2nd 
 |-  ( ( H ` m ) e. ( RR X. RR ) -> ( 2nd ` ( H ` m ) ) e. RR )
87 85 86 syl 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( 2nd ` ( H ` m ) ) e. RR )
88 xp1st 
 |-  ( ( H ` m ) e. ( RR X. RR ) -> ( 1st ` ( H ` m ) ) e. RR )
89 85 88 syl 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( 1st ` ( H ` m ) ) e. RR )
90 87 89 resubcld 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( ( 2nd ` ( H ` m ) ) - ( 1st ` ( H ` m ) ) ) e. RR )
91 90 recnd 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( ( 2nd ` ( H ` m ) ) - ( 1st ` ( H ` m ) ) ) e. CC )
92 79 91 eqeltrrd 
 |-  ( ( ph /\ m e. ( 1 ... K ) ) -> ( ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) - ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) ) e. CC )
93 80 82 92 fsumser 
 |-  ( ph -> sum_ m e. ( 1 ... K ) ( ( 2nd ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) - ( 1st ` ( ( F ` ( 1st ` ( J ` m ) ) ) ` ( 2nd ` ( J ` m ) ) ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` K ) )
94 53 93 eqtrd 
 |-  ( ph -> sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` K ) )
95 8 fveq1i 
 |-  ( U ` K ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` K )
96 94 95 eqtr4di 
 |-  ( ph -> sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) = ( U ` K ) )
97 f1oeng 
 |-  ( ( ( 1 ... K ) e. Fin /\ ( J |` ( 1 ... K ) ) : ( 1 ... K ) -1-1-onto-> ( J " ( 1 ... K ) ) ) -> ( 1 ... K ) ~~ ( J " ( 1 ... K ) ) )
98 23 28 97 syl2anc 
 |-  ( ph -> ( 1 ... K ) ~~ ( J " ( 1 ... K ) ) )
99 98 ensymd 
 |-  ( ph -> ( J " ( 1 ... K ) ) ~~ ( 1 ... K ) )
100 enfii 
 |-  ( ( ( 1 ... K ) e. Fin /\ ( J " ( 1 ... K ) ) ~~ ( 1 ... K ) ) -> ( J " ( 1 ... K ) ) e. Fin )
101 23 99 100 syl2anc 
 |-  ( ph -> ( J " ( 1 ... K ) ) e. Fin )
102 101 51 fsumrecl 
 |-  ( ph -> sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) e. RR )
103 fzfid 
 |-  ( ph -> ( 1 ... L ) e. Fin )
104 elfznn 
 |-  ( n e. ( 1 ... L ) -> n e. NN )
105 104 4 sylan2 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( vol* ` A ) e. RR )
106 103 105 fsumrecl 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( vol* ` A ) e. RR )
107 6 rpred 
 |-  ( ph -> B e. RR )
108 2nn 
 |-  2 e. NN
109 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
110 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
111 108 109 110 sylancr 
 |-  ( n e. NN -> ( 2 ^ n ) e. NN )
112 104 111 syl 
 |-  ( n e. ( 1 ... L ) -> ( 2 ^ n ) e. NN )
113 nndivre 
 |-  ( ( B e. RR /\ ( 2 ^ n ) e. NN ) -> ( B / ( 2 ^ n ) ) e. RR )
114 107 112 113 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( B / ( 2 ^ n ) ) e. RR )
115 103 114 fsumrecl 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) e. RR )
116 106 115 readdcld 
 |-  ( ph -> ( sum_ n e. ( 1 ... L ) ( vol* ` A ) + sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) ) e. RR )
117 5 107 readdcld 
 |-  ( ph -> ( sup ( ran T , RR* , < ) + B ) e. RR )
118 relxp 
 |-  Rel ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) )
119 relres 
 |-  Rel ( ( J " ( 1 ... K ) ) |` { n } )
120 elsni 
 |-  ( x e. { n } -> x = n )
121 120 opeq1d 
 |-  ( x e. { n } -> <. x , y >. = <. n , y >. )
122 121 eleq1d 
 |-  ( x e. { n } -> ( <. x , y >. e. ( J " ( 1 ... K ) ) <-> <. n , y >. e. ( J " ( 1 ... K ) ) ) )
123 vex 
 |-  n e. _V
124 vex 
 |-  y e. _V
125 123 124 elimasn 
 |-  ( y e. ( ( J " ( 1 ... K ) ) " { n } ) <-> <. n , y >. e. ( J " ( 1 ... K ) ) )
126 122 125 bitr4di 
 |-  ( x e. { n } -> ( <. x , y >. e. ( J " ( 1 ... K ) ) <-> y e. ( ( J " ( 1 ... K ) ) " { n } ) ) )
127 126 pm5.32i 
 |-  ( ( x e. { n } /\ <. x , y >. e. ( J " ( 1 ... K ) ) ) <-> ( x e. { n } /\ y e. ( ( J " ( 1 ... K ) ) " { n } ) ) )
128 124 opelresi 
 |-  ( <. x , y >. e. ( ( J " ( 1 ... K ) ) |` { n } ) <-> ( x e. { n } /\ <. x , y >. e. ( J " ( 1 ... K ) ) ) )
129 opelxp 
 |-  ( <. x , y >. e. ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) <-> ( x e. { n } /\ y e. ( ( J " ( 1 ... K ) ) " { n } ) ) )
130 127 128 129 3bitr4ri 
 |-  ( <. x , y >. e. ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) <-> <. x , y >. e. ( ( J " ( 1 ... K ) ) |` { n } ) )
131 118 119 130 eqrelriiv 
 |-  ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) = ( ( J " ( 1 ... K ) ) |` { n } )
132 df-res 
 |-  ( ( J " ( 1 ... K ) ) |` { n } ) = ( ( J " ( 1 ... K ) ) i^i ( { n } X. _V ) )
133 131 132 eqtri 
 |-  ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) = ( ( J " ( 1 ... K ) ) i^i ( { n } X. _V ) )
134 133 a1i 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) = ( ( J " ( 1 ... K ) ) i^i ( { n } X. _V ) ) )
135 134 iuneq2dv 
 |-  ( ph -> U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) = U_ n e. ( 1 ... L ) ( ( J " ( 1 ... K ) ) i^i ( { n } X. _V ) ) )
136 iunin2 
 |-  U_ n e. ( 1 ... L ) ( ( J " ( 1 ... K ) ) i^i ( { n } X. _V ) ) = ( ( J " ( 1 ... K ) ) i^i U_ n e. ( 1 ... L ) ( { n } X. _V ) )
137 135 136 eqtrdi 
 |-  ( ph -> U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) = ( ( J " ( 1 ... K ) ) i^i U_ n e. ( 1 ... L ) ( { n } X. _V ) ) )
138 relxp 
 |-  Rel ( NN X. NN )
139 relss 
 |-  ( ( J " ( 1 ... K ) ) C_ ( NN X. NN ) -> ( Rel ( NN X. NN ) -> Rel ( J " ( 1 ... K ) ) ) )
140 36 138 139 mpisyl 
 |-  ( ph -> Rel ( J " ( 1 ... K ) ) )
141 34 ffnd 
 |-  ( ph -> J Fn NN )
142 fveq2 
 |-  ( j = ( J ` w ) -> ( 1st ` j ) = ( 1st ` ( J ` w ) ) )
143 142 breq1d 
 |-  ( j = ( J ` w ) -> ( ( 1st ` j ) <_ L <-> ( 1st ` ( J ` w ) ) <_ L ) )
144 143 ralima 
 |-  ( ( J Fn NN /\ ( 1 ... K ) C_ NN ) -> ( A. j e. ( J " ( 1 ... K ) ) ( 1st ` j ) <_ L <-> A. w e. ( 1 ... K ) ( 1st ` ( J ` w ) ) <_ L ) )
145 141 26 144 sylancl 
 |-  ( ph -> ( A. j e. ( J " ( 1 ... K ) ) ( 1st ` j ) <_ L <-> A. w e. ( 1 ... K ) ( 1st ` ( J ` w ) ) <_ L ) )
146 16 145 mpbird 
 |-  ( ph -> A. j e. ( J " ( 1 ... K ) ) ( 1st ` j ) <_ L )
147 146 r19.21bi 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( 1st ` j ) <_ L )
148 39 81 eleqtrdi 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( 1st ` j ) e. ( ZZ>= ` 1 ) )
149 15 adantr 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> L e. ZZ )
150 elfz5 
 |-  ( ( ( 1st ` j ) e. ( ZZ>= ` 1 ) /\ L e. ZZ ) -> ( ( 1st ` j ) e. ( 1 ... L ) <-> ( 1st ` j ) <_ L ) )
151 148 149 150 syl2anc 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( ( 1st ` j ) e. ( 1 ... L ) <-> ( 1st ` j ) <_ L ) )
152 147 151 mpbird 
 |-  ( ( ph /\ j e. ( J " ( 1 ... K ) ) ) -> ( 1st ` j ) e. ( 1 ... L ) )
153 152 ralrimiva 
 |-  ( ph -> A. j e. ( J " ( 1 ... K ) ) ( 1st ` j ) e. ( 1 ... L ) )
154 vex 
 |-  x e. _V
155 154 124 op1std 
 |-  ( j = <. x , y >. -> ( 1st ` j ) = x )
156 155 eleq1d 
 |-  ( j = <. x , y >. -> ( ( 1st ` j ) e. ( 1 ... L ) <-> x e. ( 1 ... L ) ) )
157 156 rspccv 
 |-  ( A. j e. ( J " ( 1 ... K ) ) ( 1st ` j ) e. ( 1 ... L ) -> ( <. x , y >. e. ( J " ( 1 ... K ) ) -> x e. ( 1 ... L ) ) )
158 153 157 syl 
 |-  ( ph -> ( <. x , y >. e. ( J " ( 1 ... K ) ) -> x e. ( 1 ... L ) ) )
159 opelxp 
 |-  ( <. x , y >. e. ( U_ n e. ( 1 ... L ) { n } X. _V ) <-> ( x e. U_ n e. ( 1 ... L ) { n } /\ y e. _V ) )
160 124 biantru 
 |-  ( x e. U_ n e. ( 1 ... L ) { n } <-> ( x e. U_ n e. ( 1 ... L ) { n } /\ y e. _V ) )
161 iunid 
 |-  U_ n e. ( 1 ... L ) { n } = ( 1 ... L )
162 161 eleq2i 
 |-  ( x e. U_ n e. ( 1 ... L ) { n } <-> x e. ( 1 ... L ) )
163 159 160 162 3bitr2i 
 |-  ( <. x , y >. e. ( U_ n e. ( 1 ... L ) { n } X. _V ) <-> x e. ( 1 ... L ) )
164 158 163 imbitrrdi 
 |-  ( ph -> ( <. x , y >. e. ( J " ( 1 ... K ) ) -> <. x , y >. e. ( U_ n e. ( 1 ... L ) { n } X. _V ) ) )
165 140 164 relssdv 
 |-  ( ph -> ( J " ( 1 ... K ) ) C_ ( U_ n e. ( 1 ... L ) { n } X. _V ) )
166 xpiundir 
 |-  ( U_ n e. ( 1 ... L ) { n } X. _V ) = U_ n e. ( 1 ... L ) ( { n } X. _V )
167 165 166 sseqtrdi 
 |-  ( ph -> ( J " ( 1 ... K ) ) C_ U_ n e. ( 1 ... L ) ( { n } X. _V ) )
168 dfss2 
 |-  ( ( J " ( 1 ... K ) ) C_ U_ n e. ( 1 ... L ) ( { n } X. _V ) <-> ( ( J " ( 1 ... K ) ) i^i U_ n e. ( 1 ... L ) ( { n } X. _V ) ) = ( J " ( 1 ... K ) ) )
169 167 168 sylib 
 |-  ( ph -> ( ( J " ( 1 ... K ) ) i^i U_ n e. ( 1 ... L ) ( { n } X. _V ) ) = ( J " ( 1 ... K ) ) )
170 137 169 eqtrd 
 |-  ( ph -> U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) = ( J " ( 1 ... K ) ) )
171 170 101 eqeltrd 
 |-  ( ph -> U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) e. Fin )
172 ssiun2 
 |-  ( n e. ( 1 ... L ) -> ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) C_ U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) )
173 ssfi 
 |-  ( ( U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) e. Fin /\ ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) C_ U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) e. Fin )
174 171 172 173 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) e. Fin )
175 2ndconst 
 |-  ( n e. _V -> ( 2nd |` ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ) : ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) -1-1-onto-> ( ( J " ( 1 ... K ) ) " { n } ) )
176 175 elv 
 |-  ( 2nd |` ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ) : ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) -1-1-onto-> ( ( J " ( 1 ... K ) ) " { n } )
177 f1oeng 
 |-  ( ( ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) e. Fin /\ ( 2nd |` ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ) : ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) -1-1-onto-> ( ( J " ( 1 ... K ) ) " { n } ) ) -> ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ~~ ( ( J " ( 1 ... K ) ) " { n } ) )
178 174 176 177 sylancl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ~~ ( ( J " ( 1 ... K ) ) " { n } ) )
179 178 ensymd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( ( J " ( 1 ... K ) ) " { n } ) ~~ ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) )
180 enfii 
 |-  ( ( ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) e. Fin /\ ( ( J " ( 1 ... K ) ) " { n } ) ~~ ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( ( J " ( 1 ... K ) ) " { n } ) e. Fin )
181 174 179 180 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( ( J " ( 1 ... K ) ) " { n } ) e. Fin )
182 ffvelcdm 
 |-  ( ( F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( F ` n ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
183 11 104 182 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( F ` n ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
184 elovolmlem 
 |-  ( ( F ` n ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) )
185 183 184 sylib 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) )
186 185 adantrr 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) )
187 imassrn 
 |-  ( ( J " ( 1 ... K ) ) " { n } ) C_ ran ( J " ( 1 ... K ) )
188 36 adantr 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( J " ( 1 ... K ) ) C_ ( NN X. NN ) )
189 rnss 
 |-  ( ( J " ( 1 ... K ) ) C_ ( NN X. NN ) -> ran ( J " ( 1 ... K ) ) C_ ran ( NN X. NN ) )
190 188 189 syl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ran ( J " ( 1 ... K ) ) C_ ran ( NN X. NN ) )
191 rnxpid 
 |-  ran ( NN X. NN ) = NN
192 190 191 sseqtrdi 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ran ( J " ( 1 ... K ) ) C_ NN )
193 187 192 sstrid 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( ( J " ( 1 ... K ) ) " { n } ) C_ NN )
194 193 sseld 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( i e. ( ( J " ( 1 ... K ) ) " { n } ) -> i e. NN ) )
195 194 impr 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> i e. NN )
196 186 195 ffvelcdmd 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( ( F ` n ) ` i ) e. ( <_ i^i ( RR X. RR ) ) )
197 196 elin2d 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( ( F ` n ) ` i ) e. ( RR X. RR ) )
198 xp2nd 
 |-  ( ( ( F ` n ) ` i ) e. ( RR X. RR ) -> ( 2nd ` ( ( F ` n ) ` i ) ) e. RR )
199 197 198 syl 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( 2nd ` ( ( F ` n ) ` i ) ) e. RR )
200 xp1st 
 |-  ( ( ( F ` n ) ` i ) e. ( RR X. RR ) -> ( 1st ` ( ( F ` n ) ` i ) ) e. RR )
201 197 200 syl 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( 1st ` ( ( F ` n ) ` i ) ) e. RR )
202 199 201 resubcld 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. RR )
203 202 anassrs 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) -> ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. RR )
204 181 203 fsumrecl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sum_ i e. ( ( J " ( 1 ... K ) ) " { n } ) ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. RR )
205 107 111 113 syl2an 
 |-  ( ( ph /\ n e. NN ) -> ( B / ( 2 ^ n ) ) e. RR )
206 4 205 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) e. RR )
207 104 206 sylan2 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) e. RR )
208 eqid 
 |-  ( ( abs o. - ) o. ( F ` n ) ) = ( ( abs o. - ) o. ( F ` n ) )
209 208 7 ovolsf 
 |-  ( ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
210 185 209 syl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> S : NN --> ( 0 [,) +oo ) )
211 210 frnd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ran S C_ ( 0 [,) +oo ) )
212 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
213 211 212 sstrdi 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ran S C_ RR* )
214 supxrcl 
 |-  ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
215 213 214 syl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sup ( ran S , RR* , < ) e. RR* )
216 mnfxr 
 |-  -oo e. RR*
217 216 a1i 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> -oo e. RR* )
218 105 rexrd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( vol* ` A ) e. RR* )
219 105 mnfltd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> -oo < ( vol* ` A ) )
220 104 12 sylan2 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> A C_ U. ran ( (,) o. ( F ` n ) ) )
221 7 ovollb 
 |-  ( ( ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. ( F ` n ) ) ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )
222 185 220 221 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( vol* ` A ) <_ sup ( ran S , RR* , < ) )
223 217 218 215 219 222 xrltletrd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> -oo < sup ( ran S , RR* , < ) )
224 104 13 sylan2 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
225 xrre 
 |-  ( ( ( sup ( ran S , RR* , < ) e. RR* /\ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) e. RR ) /\ ( -oo < sup ( ran S , RR* , < ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) -> sup ( ran S , RR* , < ) e. RR )
226 215 207 223 224 225 syl22anc 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sup ( ran S , RR* , < ) e. RR )
227 1zzd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> 1 e. ZZ )
228 208 ovolfsval 
 |-  ( ( ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) /\ i e. NN ) -> ( ( ( abs o. - ) o. ( F ` n ) ) ` i ) = ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) )
229 185 228 sylan 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ i e. NN ) -> ( ( ( abs o. - ) o. ( F ` n ) ) ` i ) = ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) )
230 208 ovolfsf 
 |-  ( ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. ( F ` n ) ) : NN --> ( 0 [,) +oo ) )
231 185 230 syl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( ( abs o. - ) o. ( F ` n ) ) : NN --> ( 0 [,) +oo ) )
232 231 ffvelcdmda 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ i e. NN ) -> ( ( ( abs o. - ) o. ( F ` n ) ) ` i ) e. ( 0 [,) +oo ) )
233 229 232 eqeltrrd 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ i e. NN ) -> ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. ( 0 [,) +oo ) )
234 elrege0 
 |-  ( ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. ( 0 [,) +oo ) <-> ( ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. RR /\ 0 <_ ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) ) )
235 233 234 sylib 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ i e. NN ) -> ( ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. RR /\ 0 <_ ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) ) )
236 235 simpld 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ i e. NN ) -> ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. RR )
237 235 simprd 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ i e. NN ) -> 0 <_ ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) )
238 supxrub 
 |-  ( ( ran S C_ RR* /\ z e. ran S ) -> z <_ sup ( ran S , RR* , < ) )
239 213 238 sylan 
 |-  ( ( ( ph /\ n e. ( 1 ... L ) ) /\ z e. ran S ) -> z <_ sup ( ran S , RR* , < ) )
240 239 ralrimiva 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> A. z e. ran S z <_ sup ( ran S , RR* , < ) )
241 brralrspcev 
 |-  ( ( sup ( ran S , RR* , < ) e. RR /\ A. z e. ran S z <_ sup ( ran S , RR* , < ) ) -> E. x e. RR A. z e. ran S z <_ x )
242 226 240 241 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> E. x e. RR A. z e. ran S z <_ x )
243 210 ffnd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> S Fn NN )
244 breq1 
 |-  ( z = ( S ` k ) -> ( z <_ x <-> ( S ` k ) <_ x ) )
245 244 ralrn 
 |-  ( S Fn NN -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
246 243 245 syl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( A. z e. ran S z <_ x <-> A. k e. NN ( S ` k ) <_ x ) )
247 246 rexbidv 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( E. x e. RR A. z e. ran S z <_ x <-> E. x e. RR A. k e. NN ( S ` k ) <_ x ) )
248 242 247 mpbid 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> E. x e. RR A. k e. NN ( S ` k ) <_ x )
249 81 7 227 229 236 237 248 isumsup2 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> S ~~> sup ( ran S , RR , < ) )
250 7 249 eqbrtrrid 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) ) ~~> sup ( ran S , RR , < ) )
251 climrel 
 |-  Rel ~~>
252 251 releldmi 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) ) ~~> sup ( ran S , RR , < ) -> seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) ) e. dom ~~> )
253 250 252 syl 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) ) e. dom ~~> )
254 81 227 181 193 229 236 237 253 isumless 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sum_ i e. ( ( J " ( 1 ... K ) ) " { n } ) ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) <_ sum_ i e. NN ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) )
255 81 7 227 229 236 237 248 isumsup 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sum_ i e. NN ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) = sup ( ran S , RR , < ) )
256 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
257 211 256 sstrdi 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ran S C_ RR )
258 1nn 
 |-  1 e. NN
259 210 fdmd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> dom S = NN )
260 258 259 eleqtrrid 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> 1 e. dom S )
261 260 ne0d 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> dom S =/= (/) )
262 dm0rn0 
 |-  ( dom S = (/) <-> ran S = (/) )
263 262 necon3bii 
 |-  ( dom S =/= (/) <-> ran S =/= (/) )
264 261 263 sylib 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ran S =/= (/) )
265 supxrre 
 |-  ( ( ran S C_ RR /\ ran S =/= (/) /\ E. x e. RR A. z e. ran S z <_ x ) -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
266 257 264 242 265 syl3anc 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sup ( ran S , RR* , < ) = sup ( ran S , RR , < ) )
267 255 266 eqtr4d 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sum_ i e. NN ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) = sup ( ran S , RR* , < ) )
268 254 267 breqtrd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sum_ i e. ( ( J " ( 1 ... K ) ) " { n } ) ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) <_ sup ( ran S , RR* , < ) )
269 204 226 207 268 224 letrd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> sum_ i e. ( ( J " ( 1 ... K ) ) " { n } ) ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
270 103 204 207 269 fsumle 
 |-  ( ph -> sum_ n e. ( 1 ... L ) sum_ i e. ( ( J " ( 1 ... K ) ) " { n } ) ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) <_ sum_ n e. ( 1 ... L ) ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
271 vex 
 |-  i e. _V
272 123 271 op1std 
 |-  ( j = <. n , i >. -> ( 1st ` j ) = n )
273 272 fveq2d 
 |-  ( j = <. n , i >. -> ( F ` ( 1st ` j ) ) = ( F ` n ) )
274 123 271 op2ndd 
 |-  ( j = <. n , i >. -> ( 2nd ` j ) = i )
275 273 274 fveq12d 
 |-  ( j = <. n , i >. -> ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) = ( ( F ` n ) ` i ) )
276 275 fveq2d 
 |-  ( j = <. n , i >. -> ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) = ( 2nd ` ( ( F ` n ) ` i ) ) )
277 275 fveq2d 
 |-  ( j = <. n , i >. -> ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) = ( 1st ` ( ( F ` n ) ` i ) ) )
278 276 277 oveq12d 
 |-  ( j = <. n , i >. -> ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) = ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) )
279 202 recnd 
 |-  ( ( ph /\ ( n e. ( 1 ... L ) /\ i e. ( ( J " ( 1 ... K ) ) " { n } ) ) ) -> ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) e. CC )
280 278 103 181 279 fsum2d 
 |-  ( ph -> sum_ n e. ( 1 ... L ) sum_ i e. ( ( J " ( 1 ... K ) ) " { n } ) ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) = sum_ j e. U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) )
281 170 sumeq1d 
 |-  ( ph -> sum_ j e. U_ n e. ( 1 ... L ) ( { n } X. ( ( J " ( 1 ... K ) ) " { n } ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) = sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) )
282 280 281 eqtrd 
 |-  ( ph -> sum_ n e. ( 1 ... L ) sum_ i e. ( ( J " ( 1 ... K ) ) " { n } ) ( ( 2nd ` ( ( F ` n ) ` i ) ) - ( 1st ` ( ( F ` n ) ` i ) ) ) = sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) )
283 105 recnd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( vol* ` A ) e. CC )
284 114 recnd 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( B / ( 2 ^ n ) ) e. CC )
285 103 283 284 fsumadd 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) = ( sum_ n e. ( 1 ... L ) ( vol* ` A ) + sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) ) )
286 270 282 285 3brtr3d 
 |-  ( ph -> sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) <_ ( sum_ n e. ( 1 ... L ) ( vol* ` A ) + sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) ) )
287 1zzd 
 |-  ( ph -> 1 e. ZZ )
288 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
289 2 fvmpt2 
 |-  ( ( n e. NN /\ ( vol* ` A ) e. RR ) -> ( G ` n ) = ( vol* ` A ) )
290 288 4 289 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) = ( vol* ` A ) )
291 290 4 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. RR )
292 81 287 291 serfre 
 |-  ( ph -> seq 1 ( + , G ) : NN --> RR )
293 1 feq1i 
 |-  ( T : NN --> RR <-> seq 1 ( + , G ) : NN --> RR )
294 292 293 sylibr 
 |-  ( ph -> T : NN --> RR )
295 294 frnd 
 |-  ( ph -> ran T C_ RR )
296 ressxr 
 |-  RR C_ RR*
297 295 296 sstrdi 
 |-  ( ph -> ran T C_ RR* )
298 104 290 sylan2 
 |-  ( ( ph /\ n e. ( 1 ... L ) ) -> ( G ` n ) = ( vol* ` A ) )
299 1red 
 |-  ( ph -> 1 e. RR )
300 ffvelcdm 
 |-  ( ( J : NN --> ( NN X. NN ) /\ 1 e. NN ) -> ( J ` 1 ) e. ( NN X. NN ) )
301 34 258 300 sylancl 
 |-  ( ph -> ( J ` 1 ) e. ( NN X. NN ) )
302 xp1st 
 |-  ( ( J ` 1 ) e. ( NN X. NN ) -> ( 1st ` ( J ` 1 ) ) e. NN )
303 301 302 syl 
 |-  ( ph -> ( 1st ` ( J ` 1 ) ) e. NN )
304 303 nnred 
 |-  ( ph -> ( 1st ` ( J ` 1 ) ) e. RR )
305 15 zred 
 |-  ( ph -> L e. RR )
306 303 nnge1d 
 |-  ( ph -> 1 <_ ( 1st ` ( J ` 1 ) ) )
307 2fveq3 
 |-  ( w = 1 -> ( 1st ` ( J ` w ) ) = ( 1st ` ( J ` 1 ) ) )
308 307 breq1d 
 |-  ( w = 1 -> ( ( 1st ` ( J ` w ) ) <_ L <-> ( 1st ` ( J ` 1 ) ) <_ L ) )
309 eluzfz1 
 |-  ( K e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... K ) )
310 82 309 syl 
 |-  ( ph -> 1 e. ( 1 ... K ) )
311 308 16 310 rspcdva 
 |-  ( ph -> ( 1st ` ( J ` 1 ) ) <_ L )
312 299 304 305 306 311 letrd 
 |-  ( ph -> 1 <_ L )
313 elnnz1 
 |-  ( L e. NN <-> ( L e. ZZ /\ 1 <_ L ) )
314 15 312 313 sylanbrc 
 |-  ( ph -> L e. NN )
315 314 81 eleqtrdi 
 |-  ( ph -> L e. ( ZZ>= ` 1 ) )
316 298 315 283 fsumser 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( vol* ` A ) = ( seq 1 ( + , G ) ` L ) )
317 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , G ) Fn ( ZZ>= ` 1 ) )
318 287 317 syl 
 |-  ( ph -> seq 1 ( + , G ) Fn ( ZZ>= ` 1 ) )
319 fnfvelrn 
 |-  ( ( seq 1 ( + , G ) Fn ( ZZ>= ` 1 ) /\ L e. ( ZZ>= ` 1 ) ) -> ( seq 1 ( + , G ) ` L ) e. ran seq 1 ( + , G ) )
320 318 315 319 syl2anc 
 |-  ( ph -> ( seq 1 ( + , G ) ` L ) e. ran seq 1 ( + , G ) )
321 1 rneqi 
 |-  ran T = ran seq 1 ( + , G )
322 320 321 eleqtrrdi 
 |-  ( ph -> ( seq 1 ( + , G ) ` L ) e. ran T )
323 316 322 eqeltrd 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( vol* ` A ) e. ran T )
324 supxrub 
 |-  ( ( ran T C_ RR* /\ sum_ n e. ( 1 ... L ) ( vol* ` A ) e. ran T ) -> sum_ n e. ( 1 ... L ) ( vol* ` A ) <_ sup ( ran T , RR* , < ) )
325 297 323 324 syl2anc 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( vol* ` A ) <_ sup ( ran T , RR* , < ) )
326 107 recnd 
 |-  ( ph -> B e. CC )
327 geo2sum 
 |-  ( ( L e. NN /\ B e. CC ) -> sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) = ( B - ( B / ( 2 ^ L ) ) ) )
328 314 326 327 syl2anc 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) = ( B - ( B / ( 2 ^ L ) ) ) )
329 314 nnnn0d 
 |-  ( ph -> L e. NN0 )
330 nnexpcl 
 |-  ( ( 2 e. NN /\ L e. NN0 ) -> ( 2 ^ L ) e. NN )
331 108 329 330 sylancr 
 |-  ( ph -> ( 2 ^ L ) e. NN )
332 331 nnrpd 
 |-  ( ph -> ( 2 ^ L ) e. RR+ )
333 6 332 rpdivcld 
 |-  ( ph -> ( B / ( 2 ^ L ) ) e. RR+ )
334 333 rpge0d 
 |-  ( ph -> 0 <_ ( B / ( 2 ^ L ) ) )
335 107 331 nndivred 
 |-  ( ph -> ( B / ( 2 ^ L ) ) e. RR )
336 107 335 subge02d 
 |-  ( ph -> ( 0 <_ ( B / ( 2 ^ L ) ) <-> ( B - ( B / ( 2 ^ L ) ) ) <_ B ) )
337 334 336 mpbid 
 |-  ( ph -> ( B - ( B / ( 2 ^ L ) ) ) <_ B )
338 328 337 eqbrtrd 
 |-  ( ph -> sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) <_ B )
339 106 115 5 107 325 338 le2addd 
 |-  ( ph -> ( sum_ n e. ( 1 ... L ) ( vol* ` A ) + sum_ n e. ( 1 ... L ) ( B / ( 2 ^ n ) ) ) <_ ( sup ( ran T , RR* , < ) + B ) )
340 102 116 117 286 339 letrd 
 |-  ( ph -> sum_ j e. ( J " ( 1 ... K ) ) ( ( 2nd ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) - ( 1st ` ( ( F ` ( 1st ` j ) ) ` ( 2nd ` j ) ) ) ) <_ ( sup ( ran T , RR* , < ) + B ) )
341 96 340 eqbrtrrd 
 |-  ( ph -> ( U ` K ) <_ ( sup ( ran T , RR* , < ) + B ) )