Metamath Proof Explorer


Theorem ioodvbdlimc2lem

Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc2lem.a φ A
ioodvbdlimc2lem.b φ B
ioodvbdlimc2lem.altb φ A < B
ioodvbdlimc2lem.f φ F : A B
ioodvbdlimc2lem.dmdv φ dom F = A B
ioodvbdlimc2lem.dvbd φ y x A B F x y
ioodvbdlimc2lem.y Y = sup ran x A B F x <
ioodvbdlimc2lem.m M = 1 B A + 1
ioodvbdlimc2lem.s S = j M F B 1 j
ioodvbdlimc2lem.r R = j M B 1 j
ioodvbdlimc2lem.n N = if M Y x 2 + 1 Y x 2 + 1 M
ioodvbdlimc2lem.ch χ φ x + j N S j lim sup S < x 2 z A B z B < 1 j
Assertion ioodvbdlimc2lem φ lim sup S F lim B

Proof

Step Hyp Ref Expression
1 ioodvbdlimc2lem.a φ A
2 ioodvbdlimc2lem.b φ B
3 ioodvbdlimc2lem.altb φ A < B
4 ioodvbdlimc2lem.f φ F : A B
5 ioodvbdlimc2lem.dmdv φ dom F = A B
6 ioodvbdlimc2lem.dvbd φ y x A B F x y
7 ioodvbdlimc2lem.y Y = sup ran x A B F x <
8 ioodvbdlimc2lem.m M = 1 B A + 1
9 ioodvbdlimc2lem.s S = j M F B 1 j
10 ioodvbdlimc2lem.r R = j M B 1 j
11 ioodvbdlimc2lem.n N = if M Y x 2 + 1 Y x 2 + 1 M
12 ioodvbdlimc2lem.ch χ φ x + j N S j lim sup S < x 2 z A B z B < 1 j
13 uzssz M
14 zssre
15 13 14 sstri M
16 15 a1i φ M
17 2 1 resubcld φ B A
18 1 2 posdifd φ A < B 0 < B A
19 3 18 mpbid φ 0 < B A
20 19 gt0ne0d φ B A 0
21 17 20 rereccld φ 1 B A
22 0red φ 0
23 17 19 recgt0d φ 0 < 1 B A
24 22 21 23 ltled φ 0 1 B A
25 flge0nn0 1 B A 0 1 B A 1 B A 0
26 21 24 25 syl2anc φ 1 B A 0
27 peano2nn0 1 B A 0 1 B A + 1 0
28 26 27 syl φ 1 B A + 1 0
29 8 28 eqeltrid φ M 0
30 29 nn0zd φ M
31 eqid M = M
32 31 uzsup M sup M * < = +∞
33 30 32 syl φ sup M * < = +∞
34 4 adantr φ j M F : A B
35 1 rexrd φ A *
36 35 adantr φ j M A *
37 2 rexrd φ B *
38 37 adantr φ j M B *
39 2 adantr φ j M B
40 eluzelre j M j
41 40 adantl φ j M j
42 0red φ j M 0
43 0red j M 0
44 1red j M 1
45 43 44 readdcld j M 0 + 1
46 45 adantl φ j M 0 + 1
47 43 ltp1d j M 0 < 0 + 1
48 47 adantl φ j M 0 < 0 + 1
49 eluzel2 j M M
50 49 zred j M M
51 50 adantl φ j M M
52 21 flcld φ 1 B A
53 52 zred φ 1 B A
54 1red φ 1
55 26 nn0ge0d φ 0 1 B A
56 22 53 54 55 leadd1dd φ 0 + 1 1 B A + 1
57 56 8 breqtrrdi φ 0 + 1 M
58 57 adantr φ j M 0 + 1 M
59 eluzle j M M j
60 59 adantl φ j M M j
61 46 51 41 58 60 letrd φ j M 0 + 1 j
62 42 46 41 48 61 ltletrd φ j M 0 < j
63 62 gt0ne0d φ j M j 0
64 41 63 rereccld φ j M 1 j
65 39 64 resubcld φ j M B 1 j
66 1 adantr φ j M A
67 29 nn0red φ M
68 22 54 readdcld φ 0 + 1
69 53 54 readdcld φ 1 B A + 1
70 22 ltp1d φ 0 < 0 + 1
71 22 68 69 70 56 ltletrd φ 0 < 1 B A + 1
72 71 8 breqtrrdi φ 0 < M
73 72 gt0ne0d φ M 0
74 67 73 rereccld φ 1 M
75 74 adantr φ j M 1 M
76 39 75 resubcld φ j M B 1 M
77 8 eqcomi 1 B A + 1 = M
78 77 oveq2i 1 1 B A + 1 = 1 M
79 78 74 eqeltrid φ 1 1 B A + 1
80 21 23 elrpd φ 1 B A +
81 69 71 elrpd φ 1 B A + 1 +
82 1rp 1 +
83 82 a1i φ 1 +
84 fllelt 1 B A 1 B A 1 B A 1 B A < 1 B A + 1
85 21 84 syl φ 1 B A 1 B A 1 B A < 1 B A + 1
86 85 simprd φ 1 B A < 1 B A + 1
87 80 81 83 86 ltdiv2dd φ 1 1 B A + 1 < 1 1 B A
88 17 recnd φ B A
89 88 20 recrecd φ 1 1 B A = B A
90 87 89 breqtrd φ 1 1 B A + 1 < B A
91 79 17 2 90 ltsub2dd φ B B A < B 1 1 B A + 1
92 2 recnd φ B
93 1 recnd φ A
94 92 93 nncand φ B B A = A
95 78 oveq2i B 1 1 B A + 1 = B 1 M
96 95 a1i φ B 1 1 B A + 1 = B 1 M
97 91 94 96 3brtr3d φ A < B 1 M
98 97 adantr φ j M A < B 1 M
99 67 72 elrpd φ M +
100 99 adantr φ j M M +
101 41 62 elrpd φ j M j +
102 1red φ j M 1
103 0le1 0 1
104 103 a1i φ j M 0 1
105 100 101 102 104 60 lediv2ad φ j M 1 j 1 M
106 64 75 39 105 lesub2dd φ j M B 1 M B 1 j
107 66 76 65 98 106 ltletrd φ j M A < B 1 j
108 101 rpreccld φ j M 1 j +
109 39 108 ltsubrpd φ j M B 1 j < B
110 36 38 65 107 109 eliood φ j M B 1 j A B
111 34 110 ffvelrnd φ j M F B 1 j
112 111 9 fmptd φ S : M
113 1 2 3 4 5 6 dvbdfbdioo φ b x A B F x b
114 67 adantr φ x A B F x b M
115 simpr φ j M j M
116 9 fvmpt2 j M F B 1 j S j = F B 1 j
117 115 111 116 syl2anc φ j M S j = F B 1 j
118 117 fveq2d φ j M S j = F B 1 j
119 118 adantlr φ x A B F x b j M S j = F B 1 j
120 simplr φ x A B F x b j M x A B F x b
121 110 adantlr φ x A B F x b j M B 1 j A B
122 2fveq3 x = B 1 j F x = F B 1 j
123 122 breq1d x = B 1 j F x b F B 1 j b
124 123 rspccva x A B F x b B 1 j A B F B 1 j b
125 120 121 124 syl2anc φ x A B F x b j M F B 1 j b
126 119 125 eqbrtrd φ x A B F x b j M S j b
127 126 a1d φ x A B F x b j M M j S j b
128 127 ralrimiva φ x A B F x b j M M j S j b
129 breq1 k = M k j M j
130 129 imbi1d k = M k j S j b M j S j b
131 130 ralbidv k = M j M k j S j b j M M j S j b
132 131 rspcev M j M M j S j b k j M k j S j b
133 114 128 132 syl2anc φ x A B F x b k j M k j S j b
134 133 ex φ x A B F x b k j M k j S j b
135 134 reximdv φ b x A B F x b b k j M k j S j b
136 113 135 mpd φ b k j M k j S j b
137 16 33 112 136 limsupre φ lim sup S
138 137 recnd φ lim sup S
139 eluzelre j N j
140 139 adantl φ x + j N j
141 0red φ x + j N 0
142 52 peano2zd φ 1 B A + 1
143 8 142 eqeltrid φ M
144 143 adantr φ x + M
145 144 zred φ x + M
146 145 adantr φ x + j N M
147 72 ad2antrr φ x + j N 0 < M
148 ioomidp A B A < B A + B 2 A B
149 1 2 3 148 syl3anc φ A + B 2 A B
150 ne0i A + B 2 A B A B
151 149 150 syl φ A B
152 ioossre A B
153 152 a1i φ A B
154 dvfre F : A B A B F : dom F
155 4 153 154 syl2anc φ F : dom F
156 5 feq2d φ F : dom F F : A B
157 155 156 mpbid φ F : A B
158 157 ffvelrnda φ x A B F x
159 158 recnd φ x A B F x
160 159 abscld φ x A B F x
161 eqid x A B F x = x A B F x
162 eqid sup ran x A B F x < = sup ran x A B F x <
163 151 160 6 161 162 suprnmpt φ sup ran x A B F x < x A B F x sup ran x A B F x <
164 163 simpld φ sup ran x A B F x <
165 7 164 eqeltrid φ Y
166 165 adantr φ x + Y
167 rpre x + x
168 167 rehalfcld x + x 2
169 168 adantl φ x + x 2
170 167 recnd x + x
171 170 adantl φ x + x
172 2cnd φ x + 2
173 rpne0 x + x 0
174 173 adantl φ x + x 0
175 2ne0 2 0
176 175 a1i φ x + 2 0
177 171 172 174 176 divne0d φ x + x 2 0
178 166 169 177 redivcld φ x + Y x 2
179 178 flcld φ x + Y x 2
180 179 peano2zd φ x + Y x 2 + 1
181 180 144 ifcld φ x + if M Y x 2 + 1 Y x 2 + 1 M
182 11 181 eqeltrid φ x + N
183 182 zred φ x + N
184 183 adantr φ x + j N N
185 180 zred φ x + Y x 2 + 1
186 max1 M Y x 2 + 1 M if M Y x 2 + 1 Y x 2 + 1 M
187 145 185 186 syl2anc φ x + M if M Y x 2 + 1 Y x 2 + 1 M
188 187 11 breqtrrdi φ x + M N
189 188 adantr φ x + j N M N
190 eluzle j N N j
191 190 adantl φ x + j N N j
192 146 184 140 189 191 letrd φ x + j N M j
193 141 146 140 147 192 ltletrd φ x + j N 0 < j
194 193 gt0ne0d φ x + j N j 0
195 140 194 rereccld φ x + j N 1 j
196 140 193 recgt0d φ x + j N 0 < 1 j
197 195 196 elrpd φ x + j N 1 j +
198 197 adantr φ x + j N S j lim sup S < x 2 1 j +
199 12 biimpi χ φ x + j N S j lim sup S < x 2 z A B z B < 1 j
200 simp-5l φ x + j N S j lim sup S < x 2 z A B z B < 1 j φ
201 199 200 syl χ φ
202 201 4 syl χ F : A B
203 199 simplrd χ z A B
204 202 203 ffvelrnd χ F z
205 204 recnd χ F z
206 201 112 syl χ S : M
207 simp-5r φ x + j N S j lim sup S < x 2 z A B z B < 1 j x +
208 199 207 syl χ x +
209 eluz2 N M M N M N
210 144 182 188 209 syl3anbrc φ x + N M
211 201 208 210 syl2anc χ N M
212 uzss N M N M
213 211 212 syl χ N M
214 simp-4r φ x + j N S j lim sup S < x 2 z A B z B < 1 j j N
215 199 214 syl χ j N
216 213 215 sseldd χ j M
217 206 216 ffvelrnd χ S j
218 217 recnd χ S j
219 201 138 syl χ lim sup S
220 205 218 219 npncand χ F z S j + S j - lim sup S = F z lim sup S
221 220 eqcomd χ F z lim sup S = F z S j + S j - lim sup S
222 221 fveq2d χ F z lim sup S = F z S j + S j - lim sup S
223 204 217 resubcld χ F z S j
224 201 137 syl χ lim sup S
225 217 224 resubcld χ S j lim sup S
226 223 225 readdcld χ F z S j + S j - lim sup S
227 226 recnd χ F z S j + S j - lim sup S
228 227 abscld χ F z S j + S j - lim sup S
229 223 recnd χ F z S j
230 229 abscld χ F z S j
231 225 recnd χ S j lim sup S
232 231 abscld χ S j lim sup S
233 230 232 readdcld χ F z S j + S j lim sup S
234 208 rpred χ x
235 229 231 abstrid χ F z S j + S j - lim sup S F z S j + S j lim sup S
236 234 rehalfcld χ x 2
237 201 216 117 syl2anc χ S j = F B 1 j
238 237 oveq2d χ F z S j = F z F B 1 j
239 238 fveq2d χ F z S j = F z F B 1 j
240 239 230 eqeltrrd χ F z F B 1 j
241 201 165 syl χ Y
242 152 203 sselid χ z
243 201 216 65 syl2anc χ B 1 j
244 242 243 resubcld χ z B 1 j
245 241 244 remulcld χ Y z B 1 j
246 201 1 syl χ A
247 201 2 syl χ B
248 201 5 syl χ dom F = A B
249 163 simprd φ x A B F x sup ran x A B F x <
250 7 breq2i F x Y F x sup ran x A B F x <
251 250 ralbii x A B F x Y x A B F x sup ran x A B F x <
252 249 251 sylibr φ x A B F x Y
253 201 252 syl χ x A B F x Y
254 2fveq3 w = x F w = F x
255 254 breq1d w = x F w Y F x Y
256 255 cbvralvw w A B F w Y x A B F x Y
257 253 256 sylibr χ w A B F w Y
258 201 216 110 syl2anc χ B 1 j A B
259 243 rexrd χ B 1 j *
260 201 37 syl χ B *
261 15 216 sselid χ j
262 201 216 63 syl2anc χ j 0
263 261 262 rereccld χ 1 j
264 247 242 resubcld χ B z
265 242 247 resubcld χ z B
266 265 recnd χ z B
267 266 abscld χ z B
268 264 leabsd χ B z B z
269 201 92 syl χ B
270 242 recnd χ z
271 269 270 abssubd χ B z = z B
272 268 271 breqtrd χ B z z B
273 199 simprd χ z B < 1 j
274 264 267 263 272 273 lelttrd χ B z < 1 j
275 247 242 263 274 ltsub23d χ B 1 j < z
276 201 35 syl χ A *
277 iooltub A * B * z A B z < B
278 276 260 203 277 syl3anc χ z < B
279 259 260 242 275 278 eliood χ z B 1 j B
280 246 247 202 248 241 257 258 279 dvbdfbdioolem1 χ F z F B 1 j Y z B 1 j F z F B 1 j Y B A
281 280 simpld χ F z F B 1 j Y z B 1 j
282 201 216 64 syl2anc χ 1 j
283 241 282 remulcld χ Y 1 j
284 157 149 ffvelrnd φ F A + B 2
285 284 recnd φ F A + B 2
286 285 abscld φ F A + B 2
287 285 absge0d φ 0 F A + B 2
288 2fveq3 x = A + B 2 F x = F A + B 2
289 7 eqcomi sup ran x A B F x < = Y
290 289 a1i x = A + B 2 sup ran x A B F x < = Y
291 288 290 breq12d x = A + B 2 F x sup ran x A B F x < F A + B 2 Y
292 291 rspcva A + B 2 A B x A B F x sup ran x A B F x < F A + B 2 Y
293 149 249 292 syl2anc φ F A + B 2 Y
294 22 286 165 287 293 letrd φ 0 Y
295 201 294 syl χ 0 Y
296 282 recnd χ 1 j
297 sub31 z B 1 j z B 1 j = 1 j B z
298 270 269 296 297 syl3anc χ z B 1 j = 1 j B z
299 242 247 posdifd χ z < B 0 < B z
300 278 299 mpbid χ 0 < B z
301 264 300 elrpd χ B z +
302 282 301 ltsubrpd χ 1 j B z < 1 j
303 298 302 eqbrtrd χ z B 1 j < 1 j
304 244 282 303 ltled χ z B 1 j 1 j
305 244 282 241 295 304 lemul2ad χ Y z B 1 j Y 1 j
306 283 adantr χ Y = 0 Y 1 j
307 236 adantr χ Y = 0 x 2
308 oveq1 Y = 0 Y 1 j = 0 1 j
309 296 mul02d χ 0 1 j = 0
310 308 309 sylan9eqr χ Y = 0 Y 1 j = 0
311 208 rphalfcld χ x 2 +
312 311 rpgt0d χ 0 < x 2
313 312 adantr χ Y = 0 0 < x 2
314 310 313 eqbrtrd χ Y = 0 Y 1 j < x 2
315 306 307 314 ltled χ Y = 0 Y 1 j x 2
316 241 adantr χ ¬ Y = 0 Y
317 295 adantr χ ¬ Y = 0 0 Y
318 neqne ¬ Y = 0 Y 0
319 318 adantl χ ¬ Y = 0 Y 0
320 316 317 319 ne0gt0d χ ¬ Y = 0 0 < Y
321 283 adantr χ 0 < Y Y 1 j
322 15 211 sselid χ N
323 0red χ 0
324 201 208 145 syl2anc χ M
325 201 72 syl χ 0 < M
326 201 208 188 syl2anc χ M N
327 323 324 322 325 326 ltletrd χ 0 < N
328 327 gt0ne0d χ N 0
329 322 328 rereccld χ 1 N
330 241 329 remulcld χ Y 1 N
331 330 adantr χ 0 < Y Y 1 N
332 236 adantr χ 0 < Y x 2
333 282 adantr χ 0 < Y 1 j
334 329 adantr χ 0 < Y 1 N
335 241 adantr χ 0 < Y Y
336 295 adantr χ 0 < Y 0 Y
337 322 327 elrpd χ N +
338 201 216 101 syl2anc χ j +
339 1red χ 1
340 103 a1i χ 0 1
341 215 190 syl χ N j
342 337 338 339 340 341 lediv2ad χ 1 j 1 N
343 342 adantr χ 0 < Y 1 j 1 N
344 333 334 335 336 343 lemul2ad χ 0 < Y Y 1 j Y 1 N
345 234 recnd χ x
346 2cnd χ 2
347 208 rpne0d χ x 0
348 175 a1i χ 2 0
349 345 346 347 348 divne0d χ x 2 0
350 241 236 349 redivcld χ Y x 2
351 350 adantr χ 0 < Y Y x 2
352 simpr χ 0 < Y 0 < Y
353 312 adantr χ 0 < Y 0 < x 2
354 335 332 352 353 divgt0d χ 0 < Y 0 < Y x 2
355 351 354 elrpd χ 0 < Y Y x 2 +
356 355 rprecred χ 0 < Y 1 Y x 2
357 337 adantr χ 0 < Y N +
358 1red χ 0 < Y 1
359 103 a1i χ 0 < Y 0 1
360 350 flcld χ Y x 2
361 360 peano2zd χ Y x 2 + 1
362 361 zred χ Y x 2 + 1
363 201 143 syl χ M
364 361 363 ifcld χ if M Y x 2 + 1 Y x 2 + 1 M
365 11 364 eqeltrid χ N
366 365 zred χ N
367 flltp1 Y x 2 Y x 2 < Y x 2 + 1
368 350 367 syl χ Y x 2 < Y x 2 + 1
369 201 67 syl χ M
370 max2 M Y x 2 + 1 Y x 2 + 1 if M Y x 2 + 1 Y x 2 + 1 M
371 369 362 370 syl2anc χ Y x 2 + 1 if M Y x 2 + 1 Y x 2 + 1 M
372 371 11 breqtrrdi χ Y x 2 + 1 N
373 350 362 366 368 372 ltletrd χ Y x 2 < N
374 350 322 373 ltled χ Y x 2 N
375 374 adantr χ 0 < Y Y x 2 N
376 355 357 358 359 375 lediv2ad χ 0 < Y 1 N 1 Y x 2
377 334 356 335 336 376 lemul2ad χ 0 < Y Y 1 N Y 1 Y x 2
378 335 recnd χ 0 < Y Y
379 351 recnd χ 0 < Y Y x 2
380 354 gt0ne0d χ 0 < Y Y x 2 0
381 378 379 380 divrecd χ 0 < Y Y Y x 2 = Y 1 Y x 2
382 332 recnd χ 0 < Y x 2
383 352 gt0ne0d χ 0 < Y Y 0
384 349 adantr χ 0 < Y x 2 0
385 378 382 383 384 ddcand χ 0 < Y Y Y x 2 = x 2
386 381 385 eqtr3d χ 0 < Y Y 1 Y x 2 = x 2
387 377 386 breqtrd χ 0 < Y Y 1 N x 2
388 321 331 332 344 387 letrd χ 0 < Y Y 1 j x 2
389 320 388 syldan χ ¬ Y = 0 Y 1 j x 2
390 315 389 pm2.61dan χ Y 1 j x 2
391 245 283 236 305 390 letrd χ Y z B 1 j x 2
392 240 245 236 281 391 letrd χ F z F B 1 j x 2
393 239 392 eqbrtrd χ F z S j x 2
394 simpllr φ x + j N S j lim sup S < x 2 z A B z B < 1 j S j lim sup S < x 2
395 199 394 syl χ S j lim sup S < x 2
396 230 232 236 236 393 395 leltaddd χ F z S j + S j lim sup S < x 2 + x 2
397 345 2halvesd χ x 2 + x 2 = x
398 396 397 breqtrd χ F z S j + S j lim sup S < x
399 228 233 234 235 398 lelttrd χ F z S j + S j - lim sup S < x
400 222 399 eqbrtrd χ F z lim sup S < x
401 12 400 sylbir φ x + j N S j lim sup S < x 2 z A B z B < 1 j F z lim sup S < x
402 401 adantrl φ x + j N S j lim sup S < x 2 z A B z B z B < 1 j F z lim sup S < x
403 402 ex φ x + j N S j lim sup S < x 2 z A B z B z B < 1 j F z lim sup S < x
404 403 ralrimiva φ x + j N S j lim sup S < x 2 z A B z B z B < 1 j F z lim sup S < x
405 brimralrspcev 1 j + z A B z B z B < 1 j F z lim sup S < x y + z A B z B z B < y F z lim sup S < x
406 198 404 405 syl2anc φ x + j N S j lim sup S < x 2 y + z A B z B z B < y F z lim sup S < x
407 simpr φ x + b N b N
408 407 iftrued φ x + b N if b N N b = N
409 uzid N N N
410 182 409 syl φ x + N N
411 410 adantr φ x + b N N N
412 408 411 eqeltrd φ x + b N if b N N b N
413 412 adantlr φ x + b b N if b N N b N
414 iffalse ¬ b N if b N N b = b
415 414 adantl φ x + b ¬ b N if b N N b = b
416 182 ad2antrr φ x + b ¬ b N N
417 simplr φ x + b ¬ b N b
418 416 zred φ x + b ¬ b N N
419 417 zred φ x + b ¬ b N b
420 simpr φ x + b ¬ b N ¬ b N
421 418 419 ltnled φ x + b ¬ b N N < b ¬ b N
422 420 421 mpbird φ x + b ¬ b N N < b
423 418 419 422 ltled φ x + b ¬ b N N b
424 eluz2 b N N b N b
425 416 417 423 424 syl3anbrc φ x + b ¬ b N b N
426 415 425 eqeltrd φ x + b ¬ b N if b N N b N
427 413 426 pm2.61dan φ x + b if b N N b N
428 427 adantr φ x + b c b S c S c lim sup S < x 2 if b N N b N
429 simpr φ x + b c b S c S c lim sup S < x 2 c b S c S c lim sup S < x 2
430 simpr φ x + b b
431 182 adantr φ x + b N
432 431 430 ifcld φ x + b if b N N b
433 430 zred φ x + b b
434 431 zred φ x + b N
435 max1 b N b if b N N b
436 433 434 435 syl2anc φ x + b b if b N N b
437 eluz2 if b N N b b b if b N N b b if b N N b
438 430 432 436 437 syl3anbrc φ x + b if b N N b b
439 438 adantr φ x + b c b S c S c lim sup S < x 2 if b N N b b
440 fveq2 c = if b N N b S c = S if b N N b
441 440 eleq1d c = if b N N b S c S if b N N b
442 440 fvoveq1d c = if b N N b S c lim sup S = S if b N N b lim sup S
443 442 breq1d c = if b N N b S c lim sup S < x 2 S if b N N b lim sup S < x 2
444 441 443 anbi12d c = if b N N b S c S c lim sup S < x 2 S if b N N b S if b N N b lim sup S < x 2
445 444 rspccva c b S c S c lim sup S < x 2 if b N N b b S if b N N b S if b N N b lim sup S < x 2
446 429 439 445 syl2anc φ x + b c b S c S c lim sup S < x 2 S if b N N b S if b N N b lim sup S < x 2
447 446 simprd φ x + b c b S c S c lim sup S < x 2 S if b N N b lim sup S < x 2
448 fveq2 j = if b N N b S j = S if b N N b
449 448 fvoveq1d j = if b N N b S j lim sup S = S if b N N b lim sup S
450 449 breq1d j = if b N N b S j lim sup S < x 2 S if b N N b lim sup S < x 2
451 450 rspcev if b N N b N S if b N N b lim sup S < x 2 j N S j lim sup S < x 2
452 428 447 451 syl2anc φ x + b c b S c S c lim sup S < x 2 j N S j lim sup S < x 2
453 ax-resscn
454 453 a1i φ
455 4 454 fssd φ F : A B
456 dvcn F : A B A B dom F = A B F : A B cn
457 454 455 153 5 456 syl31anc φ F : A B cn
458 cncffvrn F : A B cn F : A B cn F : A B
459 454 457 458 syl2anc φ F : A B cn F : A B
460 4 459 mpbird φ F : A B cn
461 110 10 fmptd φ R : M A B
462 eqid j M F R j = j M F R j
463 climrel Rel
464 463 a1i φ Rel
465 fvex M V
466 465 mptex j M B V
467 466 a1i φ j M B V
468 eqidd φ m M j M B = j M B
469 eqidd φ m M j = m B = B
470 simpr φ m M m M
471 2 adantr φ m M B
472 468 469 470 471 fvmptd φ m M j M B m = B
473 31 30 467 92 472 climconst φ j M B B
474 465 mptex j M B 1 j V
475 10 474 eqeltri R V
476 475 a1i φ R V
477 1cnd φ 1
478 elnnnn0b M M 0 0 < M
479 29 72 478 sylanbrc φ M
480 divcnvg 1 M j M 1 j 0
481 477 479 480 syl2anc φ j M 1 j 0
482 eqidd φ i M j M B = j M B
483 eqidd φ i M j = i B = B
484 simpr φ i M i M
485 2 adantr φ i M B
486 482 483 484 485 fvmptd φ i M j M B i = B
487 486 485 eqeltrd φ i M j M B i
488 487 recnd φ i M j M B i
489 eqidd φ i M j M 1 j = j M 1 j
490 oveq2 j = i 1 j = 1 i
491 490 adantl φ i M j = i 1 j = 1 i
492 15 484 sselid φ i M i
493 0red φ i M 0
494 67 adantr φ i M M
495 72 adantr φ i M 0 < M
496 eluzle i M M i
497 496 adantl φ i M M i
498 493 494 492 495 497 ltletrd φ i M 0 < i
499 498 gt0ne0d φ i M i 0
500 492 499 rereccld φ i M 1 i
501 489 491 484 500 fvmptd φ i M j M 1 j i = 1 i
502 492 recnd φ i M i
503 502 499 reccld φ i M 1 i
504 501 503 eqeltrd φ i M j M 1 j i
505 490 oveq2d j = i B 1 j = B 1 i
506 ovex B 1 i V
507 505 10 506 fvmpt i M R i = B 1 i
508 507 adantl φ i M R i = B 1 i
509 486 501 oveq12d φ i M j M B i j M 1 j i = B 1 i
510 508 509 eqtr4d φ i M R i = j M B i j M 1 j i
511 31 30 473 476 481 488 504 510 climsub φ R B 0
512 92 subid1d φ B 0 = B
513 511 512 breqtrd φ R B
514 releldm Rel R B R dom
515 464 513 514 syl2anc φ R dom
516 fveq2 l = k l = k
517 fveq2 l = k R l = R k
518 517 oveq2d l = k R h R l = R h R k
519 518 fveq2d l = k R h R l = R h R k
520 519 breq1d l = k R h R l < x sup ran z A B F z < + 1 R h R k < x sup ran z A B F z < + 1
521 516 520 raleqbidv l = k h l R h R l < x sup ran z A B F z < + 1 h k R h R k < x sup ran z A B F z < + 1
522 521 cbvrabv l M | h l R h R l < x sup ran z A B F z < + 1 = k M | h k R h R k < x sup ran z A B F z < + 1
523 fveq2 h = i R h = R i
524 523 fvoveq1d h = i R h R k = R i R k
525 524 breq1d h = i R h R k < x sup ran z A B F z < + 1 R i R k < x sup ran z A B F z < + 1
526 525 cbvralvw h k R h R k < x sup ran z A B F z < + 1 i k R i R k < x sup ran z A B F z < + 1
527 526 rgenw k M h k R h R k < x sup ran z A B F z < + 1 i k R i R k < x sup ran z A B F z < + 1
528 rabbi k M h k R h R k < x sup ran z A B F z < + 1 i k R i R k < x sup ran z A B F z < + 1 k M | h k R h R k < x sup ran z A B F z < + 1 = k M | i k R i R k < x sup ran z A B F z < + 1
529 527 528 mpbi k M | h k R h R k < x sup ran z A B F z < + 1 = k M | i k R i R k < x sup ran z A B F z < + 1
530 522 529 eqtri l M | h l R h R l < x sup ran z A B F z < + 1 = k M | i k R i R k < x sup ran z A B F z < + 1
531 530 infeq1i sup l M | h l R h R l < x sup ran z A B F z < + 1 < = sup k M | i k R i R k < x sup ran z A B F z < + 1 <
532 1 2 3 460 5 6 30 461 462 515 531 ioodvbdlimc1lem1 φ j M F R j lim sup j M F R j
533 10 fvmpt2 j M B 1 j R j = B 1 j
534 115 65 533 syl2anc φ j M R j = B 1 j
535 534 eqcomd φ j M B 1 j = R j
536 535 fveq2d φ j M F B 1 j = F R j
537 536 mpteq2dva φ j M F B 1 j = j M F R j
538 9 537 syl5eq φ S = j M F R j
539 538 fveq2d φ lim sup S = lim sup j M F R j
540 532 538 539 3brtr4d φ S lim sup S
541 465 mptex j M F B 1 j V
542 9 541 eqeltri S V
543 542 a1i φ S V
544 eqidd φ c S c = S c
545 543 544 clim φ S lim sup S lim sup S a + b c b S c S c lim sup S < a
546 540 545 mpbid φ lim sup S a + b c b S c S c lim sup S < a
547 546 simprd φ a + b c b S c S c lim sup S < a
548 547 adantr φ x + a + b c b S c S c lim sup S < a
549 simpr φ x + x +
550 549 rphalfcld φ x + x 2 +
551 breq2 a = x 2 S c lim sup S < a S c lim sup S < x 2
552 551 anbi2d a = x 2 S c S c lim sup S < a S c S c lim sup S < x 2
553 552 rexralbidv a = x 2 b c b S c S c lim sup S < a b c b S c S c lim sup S < x 2
554 553 rspccva a + b c b S c S c lim sup S < a x 2 + b c b S c S c lim sup S < x 2
555 548 550 554 syl2anc φ x + b c b S c S c lim sup S < x 2
556 452 555 r19.29a φ x + j N S j lim sup S < x 2
557 406 556 r19.29a φ x + y + z A B z B z B < y F z lim sup S < x
558 557 ralrimiva φ x + y + z A B z B z B < y F z lim sup S < x
559 ioosscn A B
560 559 a1i φ A B
561 455 560 92 ellimc3 φ lim sup S F lim B lim sup S x + y + z A B z B z B < y F z lim sup S < x
562 138 558 561 mpbir2and φ lim sup S F lim B