Metamath Proof Explorer

Theorem ovolval5lem2

Description: |- ( ( ph /\ n e. NN ) -> <. ( ( 1st( Fn ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd( Fn ) ) >. e. ( RR X. RR ) ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval5lem2.q 
|- Q = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
ovolval5lem2.y 
|- ( ph -> Y = ( sum^ ` ( ( vol o. [,) ) o. F ) ) )
ovolval5lem2.z 
|- Z = ( sum^ ` ( ( vol o. (,) ) o. G ) )
ovolval5lem2.f 
|- ( ph -> F : NN --> ( RR X. RR ) )
ovolval5lem2.s 
|- ( ph -> A C_ U. ran ( [,) o. F ) )
ovolval5lem2.w 
|- ( ph -> W e. RR+ )
ovolval5lem2.g 
|- G = ( n e. NN |-> <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. )
Assertion ovolval5lem2 
|- ( ph -> E. z e. Q z <_ ( Y +e W ) )

Proof

Step Hyp Ref Expression
1 ovolval5lem2.q 
 |-  Q = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
2 ovolval5lem2.y 
 |-  ( ph -> Y = ( sum^ ` ( ( vol o. [,) ) o. F ) ) )
3 ovolval5lem2.z 
 |-  Z = ( sum^ ` ( ( vol o. (,) ) o. G ) )
4 ovolval5lem2.f 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
5 ovolval5lem2.s 
 |-  ( ph -> A C_ U. ran ( [,) o. F ) )
6 ovolval5lem2.w 
 |-  ( ph -> W e. RR+ )
7 ovolval5lem2.g 
 |-  G = ( n e. NN |-> <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. )
8 3 a1i 
 |-  ( ph -> Z = ( sum^ ` ( ( vol o. (,) ) o. G ) ) )
9 nnex 
 |-  NN e. _V
10 9 a1i 
 |-  ( ph -> NN e. _V )
11 volioof 
 |-  ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo )
12 11 a1i 
 |-  ( ph -> ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo ) )
13 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
14 13 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( RR* X. RR* ) )
15 4 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. ( RR X. RR ) )
16 xp1st 
 |-  ( ( F ` n ) e. ( RR X. RR ) -> ( 1st ` ( F ` n ) ) e. RR )
17 15 16 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR )
18 6 rpred 
 |-  ( ph -> W e. RR )
19 18 adantr 
 |-  ( ( ph /\ n e. NN ) -> W e. RR )
20 2nn 
 |-  2 e. NN
21 20 a1i 
 |-  ( n e. NN -> 2 e. NN )
22 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
23 21 22 nnexpcld 
 |-  ( n e. NN -> ( 2 ^ n ) e. NN )
24 23 nnred 
 |-  ( n e. NN -> ( 2 ^ n ) e. RR )
25 24 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR )
26 23 nnne0d 
 |-  ( n e. NN -> ( 2 ^ n ) =/= 0 )
27 26 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) =/= 0 )
28 19 25 27 redivcld 
 |-  ( ( ph /\ n e. NN ) -> ( W / ( 2 ^ n ) ) e. RR )
29 17 28 resubcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) e. RR )
30 xp2nd 
 |-  ( ( F ` n ) e. ( RR X. RR ) -> ( 2nd ` ( F ` n ) ) e. RR )
31 15 30 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR )
32 29 31 opelxpd 
 |-  ( ( ph /\ n e. NN ) -> <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. e. ( RR X. RR ) )
33 32 7 fmptd 
 |-  ( ph -> G : NN --> ( RR X. RR ) )
34 12 14 33 fcoss 
 |-  ( ph -> ( ( vol o. (,) ) o. G ) : NN --> ( 0 [,] +oo ) )
35 10 34 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( ( vol o. (,) ) o. G ) ) e. RR* )
36 8 35 eqeltrd 
 |-  ( ph -> Z e. RR* )
37 reex 
 |-  RR e. _V
38 37 37 xpex 
 |-  ( RR X. RR ) e. _V
39 38 a1i 
 |-  ( ph -> ( RR X. RR ) e. _V )
40 39 10 elmapd 
 |-  ( ph -> ( G e. ( ( RR X. RR ) ^m NN ) <-> G : NN --> ( RR X. RR ) ) )
41 33 40 mpbird 
 |-  ( ph -> G e. ( ( RR X. RR ) ^m NN ) )
42 33 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. ( RR X. RR ) )
43 xp1st 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 1st ` ( G ` n ) ) e. RR )
44 42 43 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) e. RR )
45 44 rexrd 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) e. RR* )
46 xp2nd 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( 2nd ` ( G ` n ) ) e. RR )
47 42 46 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) e. RR )
48 47 rexrd 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) e. RR* )
49 6 adantr 
 |-  ( ( ph /\ n e. NN ) -> W e. RR+ )
50 23 nnrpd 
 |-  ( n e. NN -> ( 2 ^ n ) e. RR+ )
51 50 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. RR+ )
52 49 51 rpdivcld 
 |-  ( ( ph /\ n e. NN ) -> ( W / ( 2 ^ n ) ) e. RR+ )
53 17 52 ltsubrpd 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) < ( 1st ` ( F ` n ) ) )
54 id 
 |-  ( n e. NN -> n e. NN )
55 opex 
 |-  <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. e. _V
56 55 a1i 
 |-  ( n e. NN -> <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. e. _V )
57 7 fvmpt2 
 |-  ( ( n e. NN /\ <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. e. _V ) -> ( G ` n ) = <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. )
58 54 56 57 syl2anc 
 |-  ( n e. NN -> ( G ` n ) = <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. )
59 58 fveq2d 
 |-  ( n e. NN -> ( 1st ` ( G ` n ) ) = ( 1st ` <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. ) )
60 ovex 
 |-  ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) e. _V
61 fvex 
 |-  ( 2nd ` ( F ` n ) ) e. _V
62 op1stg 
 |-  ( ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) e. _V /\ ( 2nd ` ( F ` n ) ) e. _V ) -> ( 1st ` <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. ) = ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) )
63 60 61 62 mp2an 
 |-  ( 1st ` <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. ) = ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) )
64 63 a1i 
 |-  ( n e. NN -> ( 1st ` <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. ) = ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) )
65 59 64 eqtrd 
 |-  ( n e. NN -> ( 1st ` ( G ` n ) ) = ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) )
66 65 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) )
67 66 breq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( G ` n ) ) < ( 1st ` ( F ` n ) ) <-> ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) < ( 1st ` ( F ` n ) ) ) )
68 53 67 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( 1st ` ( G ` n ) ) < ( 1st ` ( F ` n ) ) )
69 58 fveq2d 
 |-  ( n e. NN -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. ) )
70 60 61 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. ) = ( 2nd ` ( F ` n ) )
71 70 a1i 
 |-  ( n e. NN -> ( 2nd ` <. ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd ` ( F ` n ) ) >. ) = ( 2nd ` ( F ` n ) ) )
72 69 71 eqtrd 
 |-  ( n e. NN -> ( 2nd ` ( G ` n ) ) = ( 2nd ` ( F ` n ) ) )
73 72 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( 2nd ` ( F ` n ) ) )
74 73 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) = ( 2nd ` ( G ` n ) ) )
75 31 74 eqled 
 |-  ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) <_ ( 2nd ` ( G ` n ) ) )
76 icossioo 
 |-  ( ( ( ( 1st ` ( G ` n ) ) e. RR* /\ ( 2nd ` ( G ` n ) ) e. RR* ) /\ ( ( 1st ` ( G ` n ) ) < ( 1st ` ( F ` n ) ) /\ ( 2nd ` ( F ` n ) ) <_ ( 2nd ` ( G ` n ) ) ) ) -> ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) C_ ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) )
77 45 48 68 75 76 syl22anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) C_ ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) )
78 1st2nd2 
 |-  ( ( F ` n ) e. ( RR X. RR ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
79 15 78 syl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
80 79 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( [,) ` ( F ` n ) ) = ( [,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
81 df-ov 
 |-  ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) = ( [,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
82 81 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) = ( [,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
83 80 82 eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( [,) ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) )
84 1st2nd2 
 |-  ( ( G ` n ) e. ( RR X. RR ) -> ( G ` n ) = <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. )
85 42 84 syl 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) = <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. )
86 85 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( (,) ` ( G ` n ) ) = ( (,) ` <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. ) )
87 df-ov 
 |-  ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) = ( (,) ` <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. )
88 87 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) = ( (,) ` <. ( 1st ` ( G ` n ) ) , ( 2nd ` ( G ` n ) ) >. ) )
89 86 88 eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( (,) ` ( G ` n ) ) = ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) )
90 83 89 sseq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( [,) ` ( F ` n ) ) C_ ( (,) ` ( G ` n ) ) <-> ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) C_ ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) ) )
91 77 90 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( [,) ` ( F ` n ) ) C_ ( (,) ` ( G ` n ) ) )
92 91 ralrimiva 
 |-  ( ph -> A. n e. NN ( [,) ` ( F ` n ) ) C_ ( (,) ` ( G ` n ) ) )
93 ss2iun 
 |-  ( A. n e. NN ( [,) ` ( F ` n ) ) C_ ( (,) ` ( G ` n ) ) -> U_ n e. NN ( [,) ` ( F ` n ) ) C_ U_ n e. NN ( (,) ` ( G ` n ) ) )
94 92 93 syl 
 |-  ( ph -> U_ n e. NN ( [,) ` ( F ` n ) ) C_ U_ n e. NN ( (,) ` ( G ` n ) ) )
95 fvex 
 |-  ( [,) ` ( F ` n ) ) e. _V
96 95 rgenw 
 |-  A. n e. NN ( [,) ` ( F ` n ) ) e. _V
97 96 a1i 
 |-  ( ph -> A. n e. NN ( [,) ` ( F ` n ) ) e. _V )
98 dfiun3g 
 |-  ( A. n e. NN ( [,) ` ( F ` n ) ) e. _V -> U_ n e. NN ( [,) ` ( F ` n ) ) = U. ran ( n e. NN |-> ( [,) ` ( F ` n ) ) ) )
99 97 98 syl 
 |-  ( ph -> U_ n e. NN ( [,) ` ( F ` n ) ) = U. ran ( n e. NN |-> ( [,) ` ( F ` n ) ) ) )
100 icof 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
101 100 a1i 
 |-  ( ph -> [,) : ( RR* X. RR* ) --> ~P RR* )
102 4 14 101 fcomptss 
 |-  ( ph -> ( [,) o. F ) = ( n e. NN |-> ( [,) ` ( F ` n ) ) ) )
103 102 eqcomd 
 |-  ( ph -> ( n e. NN |-> ( [,) ` ( F ` n ) ) ) = ( [,) o. F ) )
104 103 rneqd 
 |-  ( ph -> ran ( n e. NN |-> ( [,) ` ( F ` n ) ) ) = ran ( [,) o. F ) )
105 104 unieqd 
 |-  ( ph -> U. ran ( n e. NN |-> ( [,) ` ( F ` n ) ) ) = U. ran ( [,) o. F ) )
106 99 105 eqtr2d 
 |-  ( ph -> U. ran ( [,) o. F ) = U_ n e. NN ( [,) ` ( F ` n ) ) )
107 fvex 
 |-  ( (,) ` ( G ` n ) ) e. _V
108 107 rgenw 
 |-  A. n e. NN ( (,) ` ( G ` n ) ) e. _V
109 108 a1i 
 |-  ( ph -> A. n e. NN ( (,) ` ( G ` n ) ) e. _V )
110 dfiun3g 
 |-  ( A. n e. NN ( (,) ` ( G ` n ) ) e. _V -> U_ n e. NN ( (,) ` ( G ` n ) ) = U. ran ( n e. NN |-> ( (,) ` ( G ` n ) ) ) )
111 109 110 syl 
 |-  ( ph -> U_ n e. NN ( (,) ` ( G ` n ) ) = U. ran ( n e. NN |-> ( (,) ` ( G ` n ) ) ) )
112 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
113 112 a1i 
 |-  ( ph -> (,) : ( RR* X. RR* ) --> ~P RR )
114 33 14 113 fcomptss 
 |-  ( ph -> ( (,) o. G ) = ( n e. NN |-> ( (,) ` ( G ` n ) ) ) )
115 114 eqcomd 
 |-  ( ph -> ( n e. NN |-> ( (,) ` ( G ` n ) ) ) = ( (,) o. G ) )
116 115 rneqd 
 |-  ( ph -> ran ( n e. NN |-> ( (,) ` ( G ` n ) ) ) = ran ( (,) o. G ) )
117 116 unieqd 
 |-  ( ph -> U. ran ( n e. NN |-> ( (,) ` ( G ` n ) ) ) = U. ran ( (,) o. G ) )
118 111 117 eqtr2d 
 |-  ( ph -> U. ran ( (,) o. G ) = U_ n e. NN ( (,) ` ( G ` n ) ) )
119 106 118 sseq12d 
 |-  ( ph -> ( U. ran ( [,) o. F ) C_ U. ran ( (,) o. G ) <-> U_ n e. NN ( [,) ` ( F ` n ) ) C_ U_ n e. NN ( (,) ` ( G ` n ) ) ) )
120 94 119 mpbird 
 |-  ( ph -> U. ran ( [,) o. F ) C_ U. ran ( (,) o. G ) )
121 5 120 sstrd 
 |-  ( ph -> A C_ U. ran ( (,) o. G ) )
122 121 8 jca 
 |-  ( ph -> ( A C_ U. ran ( (,) o. G ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) )
123 coeq2 
 |-  ( f = G -> ( (,) o. f ) = ( (,) o. G ) )
124 123 rneqd 
 |-  ( f = G -> ran ( (,) o. f ) = ran ( (,) o. G ) )
125 124 unieqd 
 |-  ( f = G -> U. ran ( (,) o. f ) = U. ran ( (,) o. G ) )
126 125 sseq2d 
 |-  ( f = G -> ( A C_ U. ran ( (,) o. f ) <-> A C_ U. ran ( (,) o. G ) ) )
127 coeq2 
 |-  ( f = G -> ( ( vol o. (,) ) o. f ) = ( ( vol o. (,) ) o. G ) )
128 127 fveq2d 
 |-  ( f = G -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( vol o. (,) ) o. G ) ) )
129 128 eqeq2d 
 |-  ( f = G -> ( Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) <-> Z = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) )
130 126 129 anbi12d 
 |-  ( f = G -> ( ( A C_ U. ran ( (,) o. f ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> ( A C_ U. ran ( (,) o. G ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) ) )
131 130 rspcev 
 |-  ( ( G e. ( ( RR X. RR ) ^m NN ) /\ ( A C_ U. ran ( (,) o. G ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. G ) ) ) ) -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
132 41 122 131 syl2anc 
 |-  ( ph -> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
133 36 132 jca 
 |-  ( ph -> ( Z e. RR* /\ E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
134 eqeq1 
 |-  ( z = Z -> ( z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) <-> Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) )
135 134 anbi2d 
 |-  ( z = Z -> ( ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
136 135 rexbidv 
 |-  ( z = Z -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
137 136 1 elrab2 
 |-  ( Z e. Q <-> ( Z e. RR* /\ E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ Z = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) ) )
138 133 137 sylibr 
 |-  ( ph -> Z e. Q )
139 2fveq3 
 |-  ( m = n -> ( 1st ` ( F ` m ) ) = ( 1st ` ( F ` n ) ) )
140 2fveq3 
 |-  ( m = n -> ( 2nd ` ( F ` m ) ) = ( 2nd ` ( F ` n ) ) )
141 139 140 breq12d 
 |-  ( m = n -> ( ( 1st ` ( F ` m ) ) < ( 2nd ` ( F ` m ) ) <-> ( 1st ` ( F ` n ) ) < ( 2nd ` ( F ` n ) ) ) )
142 141 cbvrabv 
 |-  { m e. NN | ( 1st ` ( F ` m ) ) < ( 2nd ` ( F ` m ) ) } = { n e. NN | ( 1st ` ( F ` n ) ) < ( 2nd ` ( F ` n ) ) }
143 17 31 6 142 ovolval5lem1 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( vol ` ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) ) ) ) <_ ( ( sum^ ` ( n e. NN |-> ( vol ` ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) ) ) ) +e W ) )
144 nfcv 
 |-  F/_ n G
145 33 14 fssd 
 |-  ( ph -> G : NN --> ( RR* X. RR* ) )
146 144 145 volioofmpt 
 |-  ( ph -> ( ( vol o. (,) ) o. G ) = ( n e. NN |-> ( vol ` ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) ) ) )
147 66 73 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) = ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) )
148 147 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( vol ` ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) ) = ( vol ` ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) ) )
149 148 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> ( vol ` ( ( 1st ` ( G ` n ) ) (,) ( 2nd ` ( G ` n ) ) ) ) ) = ( n e. NN |-> ( vol ` ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) ) ) )
150 146 149 eqtrd 
 |-  ( ph -> ( ( vol o. (,) ) o. G ) = ( n e. NN |-> ( vol ` ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) ) ) )
151 150 fveq2d 
 |-  ( ph -> ( sum^ ` ( ( vol o. (,) ) o. G ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) ) ) ) )
152 8 151 eqtrd 
 |-  ( ph -> Z = ( sum^ ` ( n e. NN |-> ( vol ` ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) ) ) ) )
153 nfcv 
 |-  F/_ n F
154 ressxr 
 |-  RR C_ RR*
155 xpss2 
 |-  ( RR C_ RR* -> ( RR X. RR ) C_ ( RR X. RR* ) )
156 154 155 ax-mp 
 |-  ( RR X. RR ) C_ ( RR X. RR* )
157 156 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( RR X. RR* ) )
158 4 157 fssd 
 |-  ( ph -> F : NN --> ( RR X. RR* ) )
159 153 158 volicofmpt 
 |-  ( ph -> ( ( vol o. [,) ) o. F ) = ( n e. NN |-> ( vol ` ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) ) ) )
160 159 fveq2d 
 |-  ( ph -> ( sum^ ` ( ( vol o. [,) ) o. F ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) ) ) ) )
161 2 160 eqtrd 
 |-  ( ph -> Y = ( sum^ ` ( n e. NN |-> ( vol ` ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) ) ) ) )
162 161 oveq1d 
 |-  ( ph -> ( Y +e W ) = ( ( sum^ ` ( n e. NN |-> ( vol ` ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) ) ) ) +e W ) )
163 152 162 breq12d 
 |-  ( ph -> ( Z <_ ( Y +e W ) <-> ( sum^ ` ( n e. NN |-> ( vol ` ( ( ( 1st ` ( F ` n ) ) - ( W / ( 2 ^ n ) ) ) (,) ( 2nd ` ( F ` n ) ) ) ) ) ) <_ ( ( sum^ ` ( n e. NN |-> ( vol ` ( ( 1st ` ( F ` n ) ) [,) ( 2nd ` ( F ` n ) ) ) ) ) ) +e W ) ) )
164 143 163 mpbird 
 |-  ( ph -> Z <_ ( Y +e W ) )
165 breq1 
 |-  ( z = Z -> ( z <_ ( Y +e W ) <-> Z <_ ( Y +e W ) ) )
166 165 rspcev 
 |-  ( ( Z e. Q /\ Z <_ ( Y +e W ) ) -> E. z e. Q z <_ ( Y +e W ) )
167 138 164 166 syl2anc 
 |-  ( ph -> E. z e. Q z <_ ( Y +e W ) )