Metamath Proof Explorer

Theorem ovoliunlem3

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014)

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+ )
Assertion ovoliunlem3 
|- ( ph -> ( vol* ` U_ n e. NN A ) <_ ( 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 nfcv 
 |-  F/_ m A
8 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
9 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
10 7 8 9 cbviun 
 |-  U_ n e. NN A = U_ m e. NN [_ m / n ]_ A
11 10 fveq2i 
 |-  ( vol* ` U_ n e. NN A ) = ( vol* ` U_ m e. NN [_ m / n ]_ A )
12 2nn 
 |-  2 e. NN
13 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
14 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
15 12 13 14 sylancr 
 |-  ( n e. NN -> ( 2 ^ n ) e. NN )
16 15 nnrpd 
 |-  ( n e. NN -> ( 2 ^ n ) e. RR+ )
17 rpdivcl 
 |-  ( ( B e. RR+ /\ ( 2 ^ n ) e. RR+ ) -> ( B / ( 2 ^ n ) ) e. RR+ )
18 6 16 17 syl2an 
 |-  ( ( ph /\ n e. NN ) -> ( B / ( 2 ^ n ) ) e. RR+ )
19 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
20 19 ovolgelb 
 |-  ( ( A C_ RR /\ ( vol* ` A ) e. RR /\ ( B / ( 2 ^ n ) ) e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) )
21 3 4 18 20 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) )
22 21 ralrimiva 
 |-  ( ph -> A. n e. NN E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) )
23 ovex 
 |-  ( ( <_ i^i ( RR X. RR ) ) ^m NN ) e. _V
24 nnenom 
 |-  NN ~~ _om
25 coeq2 
 |-  ( f = ( g ` n ) -> ( (,) o. f ) = ( (,) o. ( g ` n ) ) )
26 25 rneqd 
 |-  ( f = ( g ` n ) -> ran ( (,) o. f ) = ran ( (,) o. ( g ` n ) ) )
27 26 unieqd 
 |-  ( f = ( g ` n ) -> U. ran ( (,) o. f ) = U. ran ( (,) o. ( g ` n ) ) )
28 27 sseq2d 
 |-  ( f = ( g ` n ) -> ( A C_ U. ran ( (,) o. f ) <-> A C_ U. ran ( (,) o. ( g ` n ) ) ) )
29 coeq2 
 |-  ( f = ( g ` n ) -> ( ( abs o. - ) o. f ) = ( ( abs o. - ) o. ( g ` n ) ) )
30 29 seqeq3d 
 |-  ( f = ( g ` n ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) )
31 30 rneqd 
 |-  ( f = ( g ` n ) -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) = ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) )
32 31 supeq1d 
 |-  ( f = ( g ` n ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) )
33 32 breq1d 
 |-  ( f = ( g ` n ) -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) <-> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) )
34 28 33 anbi12d 
 |-  ( f = ( g ` n ) -> ( ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) <-> ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) )
35 23 24 34 axcc4 
 |-  ( A. n e. NN E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) -> E. g ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) )
36 22 35 syl 
 |-  ( ph -> E. g ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) )
37 xpnnen 
 |-  ( NN X. NN ) ~~ NN
38 37 ensymi 
 |-  NN ~~ ( NN X. NN )
39 bren 
 |-  ( NN ~~ ( NN X. NN ) <-> E. j j : NN -1-1-onto-> ( NN X. NN ) )
40 38 39 mpbi 
 |-  E. j j : NN -1-1-onto-> ( NN X. NN )
41 nfcv 
 |-  F/_ m ( vol* ` A )
42 nfcv 
 |-  F/_ n vol*
43 42 8 nffv 
 |-  F/_ n ( vol* ` [_ m / n ]_ A )
44 9 fveq2d 
 |-  ( n = m -> ( vol* ` A ) = ( vol* ` [_ m / n ]_ A ) )
45 41 43 44 cbvmpt 
 |-  ( n e. NN |-> ( vol* ` A ) ) = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
46 2 45 eqtri 
 |-  G = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
47 3 ralrimiva 
 |-  ( ph -> A. n e. NN A C_ RR )
48 nfv 
 |-  F/ m A C_ RR
49 nfcv 
 |-  F/_ n RR
50 8 49 nfss 
 |-  F/ n [_ m / n ]_ A C_ RR
51 9 sseq1d 
 |-  ( n = m -> ( A C_ RR <-> [_ m / n ]_ A C_ RR ) )
52 48 50 51 cbvralw 
 |-  ( A. n e. NN A C_ RR <-> A. m e. NN [_ m / n ]_ A C_ RR )
53 47 52 sylib 
 |-  ( ph -> A. m e. NN [_ m / n ]_ A C_ RR )
54 53 r19.21bi 
 |-  ( ( ph /\ m e. NN ) -> [_ m / n ]_ A C_ RR )
55 54 ad4ant14 
 |-  ( ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) /\ m e. NN ) -> [_ m / n ]_ A C_ RR )
56 4 ralrimiva 
 |-  ( ph -> A. n e. NN ( vol* ` A ) e. RR )
57 41 nfel1 
 |-  F/ m ( vol* ` A ) e. RR
58 43 nfel1 
 |-  F/ n ( vol* ` [_ m / n ]_ A ) e. RR
59 44 eleq1d 
 |-  ( n = m -> ( ( vol* ` A ) e. RR <-> ( vol* ` [_ m / n ]_ A ) e. RR ) )
60 57 58 59 cbvralw 
 |-  ( A. n e. NN ( vol* ` A ) e. RR <-> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
61 56 60 sylib 
 |-  ( ph -> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
62 61 r19.21bi 
 |-  ( ( ph /\ m e. NN ) -> ( vol* ` [_ m / n ]_ A ) e. RR )
63 62 ad4ant14 
 |-  ( ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) /\ m e. NN ) -> ( vol* ` [_ m / n ]_ A ) e. RR )
64 5 ad2antrr 
 |-  ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) -> sup ( ran T , RR* , < ) e. RR )
65 6 ad2antrr 
 |-  ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) -> B e. RR+ )
66 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) )
67 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. ( k e. NN |-> ( ( g ` ( 1st ` ( j ` k ) ) ) ` ( 2nd ` ( j ` k ) ) ) ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( k e. NN |-> ( ( g ` ( 1st ` ( j ` k ) ) ) ` ( 2nd ` ( j ` k ) ) ) ) ) )
68 eqid 
 |-  ( k e. NN |-> ( ( g ` ( 1st ` ( j ` k ) ) ) ` ( 2nd ` ( j ` k ) ) ) ) = ( k e. NN |-> ( ( g ` ( 1st ` ( j ` k ) ) ) ` ( 2nd ` ( j ` k ) ) ) )
69 simplr 
 |-  ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) -> j : NN -1-1-onto-> ( NN X. NN ) )
70 simprl 
 |-  ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) -> g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
71 simprr 
 |-  ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) -> A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) )
72 nfv 
 |-  F/ m ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
73 nfcv 
 |-  F/_ n U. ran ( (,) o. ( g ` m ) )
74 8 73 nfss 
 |-  F/ n [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) )
75 nfcv 
 |-  F/_ n sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < )
76 nfcv 
 |-  F/_ n <_
77 nfcv 
 |-  F/_ n +
78 nfcv 
 |-  F/_ n ( B / ( 2 ^ m ) )
79 43 77 78 nfov 
 |-  F/_ n ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) )
80 75 76 79 nfbr 
 |-  F/ n sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) )
81 74 80 nfan 
 |-  F/ n ( [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) )
82 fveq2 
 |-  ( n = m -> ( g ` n ) = ( g ` m ) )
83 82 coeq2d 
 |-  ( n = m -> ( (,) o. ( g ` n ) ) = ( (,) o. ( g ` m ) ) )
84 83 rneqd 
 |-  ( n = m -> ran ( (,) o. ( g ` n ) ) = ran ( (,) o. ( g ` m ) ) )
85 84 unieqd 
 |-  ( n = m -> U. ran ( (,) o. ( g ` n ) ) = U. ran ( (,) o. ( g ` m ) ) )
86 9 85 sseq12d 
 |-  ( n = m -> ( A C_ U. ran ( (,) o. ( g ` n ) ) <-> [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) ) ) )
87 82 coeq2d 
 |-  ( n = m -> ( ( abs o. - ) o. ( g ` n ) ) = ( ( abs o. - ) o. ( g ` m ) ) )
88 87 seqeq3d 
 |-  ( n = m -> seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) )
89 88 rneqd 
 |-  ( n = m -> ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) = ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) )
90 89 supeq1d 
 |-  ( n = m -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) )
91 oveq2 
 |-  ( n = m -> ( 2 ^ n ) = ( 2 ^ m ) )
92 91 oveq2d 
 |-  ( n = m -> ( B / ( 2 ^ n ) ) = ( B / ( 2 ^ m ) ) )
93 44 92 oveq12d 
 |-  ( n = m -> ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) = ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) )
94 90 93 breq12d 
 |-  ( n = m -> ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) <-> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) ) )
95 86 94 anbi12d 
 |-  ( n = m -> ( ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) <-> ( [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) ) ) )
96 72 81 95 cbvralw 
 |-  ( A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) <-> A. m e. NN ( [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) ) )
97 71 96 sylib 
 |-  ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) -> A. m e. NN ( [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) ) )
98 97 r19.21bi 
 |-  ( ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) /\ m e. NN ) -> ( [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) ) )
99 98 simpld 
 |-  ( ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) /\ m e. NN ) -> [_ m / n ]_ A C_ U. ran ( (,) o. ( g ` m ) ) )
100 98 simprd 
 |-  ( ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) /\ m e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` m ) ) ) , RR* , < ) <_ ( ( vol* ` [_ m / n ]_ A ) + ( B / ( 2 ^ m ) ) ) )
101 1 46 55 63 64 65 66 67 68 69 70 99 100 ovoliunlem2 
 |-  ( ( ( ph /\ j : NN -1-1-onto-> ( NN X. NN ) ) /\ ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) ) -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + B ) )
102 101 exp31 
 |-  ( ph -> ( j : NN -1-1-onto-> ( NN X. NN ) -> ( ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + B ) ) ) )
103 102 exlimdv 
 |-  ( ph -> ( E. j j : NN -1-1-onto-> ( NN X. NN ) -> ( ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + B ) ) ) )
104 40 103 mpi 
 |-  ( ph -> ( ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
105 104 exlimdv 
 |-  ( ph -> ( E. g ( g : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A. n e. NN ( A C_ U. ran ( (,) o. ( g ` n ) ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( g ` n ) ) ) , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) ) ) -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
106 36 105 mpd 
 |-  ( ph -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + B ) )
107 11 106 eqbrtrid 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + B ) )