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*|f2Aran.fz=sum^vol.f
ovolval5lem2.y φY=sum^vol.F
ovolval5lem2.z Z=sum^vol.G
ovolval5lem2.f φF:2
ovolval5lem2.s φAran.F
ovolval5lem2.w φW+
ovolval5lem2.g G=n1stFnW2n2ndFn
Assertion ovolval5lem2 φzQzY+𝑒W

Proof

Step Hyp Ref Expression
1 ovolval5lem2.q Q=z*|f2Aran.fz=sum^vol.f
2 ovolval5lem2.y φY=sum^vol.F
3 ovolval5lem2.z Z=sum^vol.G
4 ovolval5lem2.f φF:2
5 ovolval5lem2.s φAran.F
6 ovolval5lem2.w φW+
7 ovolval5lem2.g G=n1stFnW2n2ndFn
8 3 a1i φZ=sum^vol.G
9 nnex V
10 9 a1i φV
11 volioof vol.:*×*0+∞
12 11 a1i φvol.:*×*0+∞
13 rexpssxrxp 2*×*
14 13 a1i φ2*×*
15 4 ffvelrnda φnFn2
16 xp1st Fn21stFn
17 15 16 syl φn1stFn
18 6 rpred φW
19 18 adantr φnW
20 2nn 2
21 20 a1i n2
22 nnnn0 nn0
23 21 22 nnexpcld n2n
24 23 nnred n2n
25 24 adantl φn2n
26 23 nnne0d n2n0
27 26 adantl φn2n0
28 19 25 27 redivcld φnW2n
29 17 28 resubcld φn1stFnW2n
30 xp2nd Fn22ndFn
31 15 30 syl φn2ndFn
32 29 31 opelxpd φn1stFnW2n2ndFn2
33 32 7 fmptd φG:2
34 12 14 33 fcoss φvol.G:0+∞
35 10 34 sge0xrcl φsum^vol.G*
36 8 35 eqeltrd φZ*
37 reex V
38 37 37 xpex 2V
39 38 a1i φ2V
40 39 10 elmapd φG2G:2
41 33 40 mpbird φG2
42 33 ffvelrnda φnGn2
43 xp1st Gn21stGn
44 42 43 syl φn1stGn
45 44 rexrd φn1stGn*
46 xp2nd Gn22ndGn
47 42 46 syl φn2ndGn
48 47 rexrd φn2ndGn*
49 6 adantr φnW+
50 23 nnrpd n2n+
51 50 adantl φn2n+
52 49 51 rpdivcld φnW2n+
53 17 52 ltsubrpd φn1stFnW2n<1stFn
54 id nn
55 opex 1stFnW2n2ndFnV
56 55 a1i n1stFnW2n2ndFnV
57 7 fvmpt2 n1stFnW2n2ndFnVGn=1stFnW2n2ndFn
58 54 56 57 syl2anc nGn=1stFnW2n2ndFn
59 58 fveq2d n1stGn=1st1stFnW2n2ndFn
60 ovex 1stFnW2nV
61 fvex 2ndFnV
62 op1stg 1stFnW2nV2ndFnV1st1stFnW2n2ndFn=1stFnW2n
63 60 61 62 mp2an 1st1stFnW2n2ndFn=1stFnW2n
64 63 a1i n1st1stFnW2n2ndFn=1stFnW2n
65 59 64 eqtrd n1stGn=1stFnW2n
66 65 adantl φn1stGn=1stFnW2n
67 66 breq1d φn1stGn<1stFn1stFnW2n<1stFn
68 53 67 mpbird φn1stGn<1stFn
69 58 fveq2d n2ndGn=2nd1stFnW2n2ndFn
70 60 61 op2nd 2nd1stFnW2n2ndFn=2ndFn
71 70 a1i n2nd1stFnW2n2ndFn=2ndFn
72 69 71 eqtrd n2ndGn=2ndFn
73 72 adantl φn2ndGn=2ndFn
74 73 eqcomd φn2ndFn=2ndGn
75 31 74 eqled φn2ndFn2ndGn
76 icossioo 1stGn*2ndGn*1stGn<1stFn2ndFn2ndGn1stFn2ndFn1stGn2ndGn
77 45 48 68 75 76 syl22anc φn1stFn2ndFn1stGn2ndGn
78 1st2nd2 Fn2Fn=1stFn2ndFn
79 15 78 syl φnFn=1stFn2ndFn
80 79 fveq2d φn.Fn=.1stFn2ndFn
81 df-ov 1stFn2ndFn=.1stFn2ndFn
82 81 a1i φn1stFn2ndFn=.1stFn2ndFn
83 80 82 eqtr4d φn.Fn=1stFn2ndFn
84 1st2nd2 Gn2Gn=1stGn2ndGn
85 42 84 syl φnGn=1stGn2ndGn
86 85 fveq2d φn.Gn=.1stGn2ndGn
87 df-ov 1stGn2ndGn=.1stGn2ndGn
88 87 a1i φn1stGn2ndGn=.1stGn2ndGn
89 86 88 eqtr4d φn.Gn=1stGn2ndGn
90 83 89 sseq12d φn.Fn.Gn1stFn2ndFn1stGn2ndGn
91 77 90 mpbird φn.Fn.Gn
92 91 ralrimiva φn.Fn.Gn
93 ss2iun n.Fn.Gnn.Fnn.Gn
94 92 93 syl φn.Fnn.Gn
95 fvex .FnV
96 95 rgenw n.FnV
97 96 a1i φn.FnV
98 dfiun3g n.FnVn.Fn=rann.Fn
99 97 98 syl φn.Fn=rann.Fn
100 icof .:*×*𝒫*
101 100 a1i φ.:*×*𝒫*
102 4 14 101 fcomptss φ.F=n.Fn
103 102 eqcomd φn.Fn=.F
104 103 rneqd φrann.Fn=ran.F
105 104 unieqd φrann.Fn=ran.F
106 99 105 eqtr2d φran.F=n.Fn
107 fvex .GnV
108 107 rgenw n.GnV
109 108 a1i φn.GnV
110 dfiun3g n.GnVn.Gn=rann.Gn
111 109 110 syl φn.Gn=rann.Gn
112 ioof .:*×*𝒫
113 112 a1i φ.:*×*𝒫
114 33 14 113 fcomptss φ.G=n.Gn
115 114 eqcomd φn.Gn=.G
116 115 rneqd φrann.Gn=ran.G
117 116 unieqd φrann.Gn=ran.G
118 111 117 eqtr2d φran.G=n.Gn
119 106 118 sseq12d φran.Fran.Gn.Fnn.Gn
120 94 119 mpbird φran.Fran.G
121 5 120 sstrd φAran.G
122 121 8 jca φAran.GZ=sum^vol.G
123 coeq2 f=G.f=.G
124 123 rneqd f=Gran.f=ran.G
125 124 unieqd f=Gran.f=ran.G
126 125 sseq2d f=GAran.fAran.G
127 coeq2 f=Gvol.f=vol.G
128 127 fveq2d f=Gsum^vol.f=sum^vol.G
129 128 eqeq2d f=GZ=sum^vol.fZ=sum^vol.G
130 126 129 anbi12d f=GAran.fZ=sum^vol.fAran.GZ=sum^vol.G
131 130 rspcev G2Aran.GZ=sum^vol.Gf2Aran.fZ=sum^vol.f
132 41 122 131 syl2anc φf2Aran.fZ=sum^vol.f
133 36 132 jca φZ*f2Aran.fZ=sum^vol.f
134 eqeq1 z=Zz=sum^vol.fZ=sum^vol.f
135 134 anbi2d z=ZAran.fz=sum^vol.fAran.fZ=sum^vol.f
136 135 rexbidv z=Zf2Aran.fz=sum^vol.ff2Aran.fZ=sum^vol.f
137 136 1 elrab2 ZQZ*f2Aran.fZ=sum^vol.f
138 133 137 sylibr φZQ
139 2fveq3 m=n1stFm=1stFn
140 2fveq3 m=n2ndFm=2ndFn
141 139 140 breq12d m=n1stFm<2ndFm1stFn<2ndFn
142 141 cbvrabv m|1stFm<2ndFm=n|1stFn<2ndFn
143 17 31 6 142 ovolval5lem1 φsum^nvol1stFnW2n2ndFnsum^nvol1stFn2ndFn+𝑒W
144 nfcv _nG
145 33 14 fssd φG:*×*
146 144 145 volioofmpt φvol.G=nvol1stGn2ndGn
147 66 73 oveq12d φn1stGn2ndGn=1stFnW2n2ndFn
148 147 fveq2d φnvol1stGn2ndGn=vol1stFnW2n2ndFn
149 148 mpteq2dva φnvol1stGn2ndGn=nvol1stFnW2n2ndFn
150 146 149 eqtrd φvol.G=nvol1stFnW2n2ndFn
151 150 fveq2d φsum^vol.G=sum^nvol1stFnW2n2ndFn
152 8 151 eqtrd φZ=sum^nvol1stFnW2n2ndFn
153 nfcv _nF
154 ressxr *
155 xpss2 *2×*
156 154 155 ax-mp 2×*
157 156 a1i φ2×*
158 4 157 fssd φF:×*
159 153 158 volicofmpt φvol.F=nvol1stFn2ndFn
160 159 fveq2d φsum^vol.F=sum^nvol1stFn2ndFn
161 2 160 eqtrd φY=sum^nvol1stFn2ndFn
162 161 oveq1d φY+𝑒W=sum^nvol1stFn2ndFn+𝑒W
163 152 162 breq12d φZY+𝑒Wsum^nvol1stFnW2n2ndFnsum^nvol1stFn2ndFn+𝑒W
164 143 163 mpbird φZY+𝑒W
165 breq1 z=ZzY+𝑒WZY+𝑒W
166 165 rspcev ZQZY+𝑒WzQzY+𝑒W
167 138 164 166 syl2anc φzQzY+𝑒W