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 vol * A
ovoliun.a φ n A
ovoliun.v φ n vol * A
ovoliun.r φ sup ran T * <
ovoliun.b φ B +
ovoliun.s S = seq 1 + abs F n
ovoliun.u U = seq 1 + abs H
ovoliun.h H = k F 1 st J k 2 nd J k
ovoliun.j φ J : 1-1 onto ×
ovoliun.f φ F : 2
ovoliun.x1 φ n A ran . F n
ovoliun.x2 φ n sup ran S * < vol * A + B 2 n
ovoliun.k φ K
ovoliun.l1 φ L
ovoliun.l2 φ w 1 K 1 st J w L
Assertion ovoliunlem1 φ U K sup ran T * < + B

Proof

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