Step | Hyp | Ref
| Expression |
1 | | caurcvgr.1 |
. . . . 5
β’ (π β π΄ β β) |
2 | | caurcvgr.2 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
3 | | caurcvgr.3 |
. . . . 5
β’ (π β sup(π΄, β*, < ) =
+β) |
4 | | caurcvgr.4 |
. . . . 5
β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
5 | | 1rp 12924 |
. . . . . 6
β’ 1 β
β+ |
6 | 5 | a1i 11 |
. . . . 5
β’ (π β 1 β
β+) |
7 | 1, 2, 3, 4, 6 | caucvgrlem 15563 |
. . . 4
β’ (π β βπ β π΄ ((lim supβπΉ) β β β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· 1)))) |
8 | | simpl 484 |
. . . . 5
β’ (((lim
supβπΉ) β β
β§ βπ β
π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· 1))) β (lim
supβπΉ) β
β) |
9 | 8 | rexlimivw 3145 |
. . . 4
β’
(βπ β
π΄ ((lim supβπΉ) β β β§
βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· 1))) β (lim
supβπΉ) β
β) |
10 | 7, 9 | syl 17 |
. . 3
β’ (π β (lim supβπΉ) β
β) |
11 | 10 | recnd 11188 |
. 2
β’ (π β (lim supβπΉ) β
β) |
12 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β β+) β π΄ β
β) |
13 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β πΉ:π΄βΆβ) |
14 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β sup(π΄, β*, < ) =
+β) |
15 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β
βπ₯ β
β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
16 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π¦ β β+) β π¦ β
β+) |
17 | | 3rp 12926 |
. . . . . . . 8
β’ 3 β
β+ |
18 | | rpdivcl 12945 |
. . . . . . . 8
β’ ((π¦ β β+
β§ 3 β β+) β (π¦ / 3) β
β+) |
19 | 16, 17, 18 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β (π¦ / 3) β
β+) |
20 | 12, 13, 14, 15, 19 | caucvgrlem 15563 |
. . . . . 6
β’ ((π β§ π¦ β β+) β
βπ β π΄ ((lim supβπΉ) β β β§
βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3))))) |
21 | | simpr 486 |
. . . . . . 7
β’ (((lim
supβπΉ) β β
β§ βπ β
π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3)))) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3)))) |
22 | 21 | reximi 3084 |
. . . . . 6
β’
(βπ β
π΄ ((lim supβπΉ) β β β§
βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3)))) β βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3)))) |
23 | 20, 22 | syl 17 |
. . . . 5
β’ ((π β§ π¦ β β+) β
βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3)))) |
24 | | ssrexv 4012 |
. . . . 5
β’ (π΄ β β β
(βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3))) β βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3))))) |
25 | 12, 23, 24 | sylc 65 |
. . . 4
β’ ((π β§ π¦ β β+) β
βπ β β
βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3)))) |
26 | | rpcn 12930 |
. . . . . . . . 9
β’ (π¦ β β+
β π¦ β
β) |
27 | 26 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π¦ β β+) β π¦ β
β) |
28 | | 3cn 12239 |
. . . . . . . . 9
β’ 3 β
β |
29 | 28 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π¦ β β+) β 3 β
β) |
30 | | 3ne0 12264 |
. . . . . . . . 9
β’ 3 β
0 |
31 | 30 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π¦ β β+) β 3 β
0) |
32 | 27, 29, 31 | divcan2d 11938 |
. . . . . . 7
β’ ((π β§ π¦ β β+) β (3
Β· (π¦ / 3)) = π¦) |
33 | 32 | breq2d 5118 |
. . . . . 6
β’ ((π β§ π¦ β β+) β
((absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3)) β (absβ((πΉβπ) β (lim supβπΉ))) < π¦)) |
34 | 33 | imbi2d 341 |
. . . . 5
β’ ((π β§ π¦ β β+) β ((π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3))) β (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < π¦))) |
35 | 34 | rexralbidv 3211 |
. . . 4
β’ ((π β§ π¦ β β+) β
(βπ β β
βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· (π¦ / 3))) β βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < π¦))) |
36 | 25, 35 | mpbid 231 |
. . 3
β’ ((π β§ π¦ β β+) β
βπ β β
βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < π¦)) |
37 | 36 | ralrimiva 3140 |
. 2
β’ (π β βπ¦ β β+ βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < π¦)) |
38 | | ax-resscn 11113 |
. . . 4
β’ β
β β |
39 | | fss 6686 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ β β
β) β πΉ:π΄βΆβ) |
40 | 2, 38, 39 | sylancl 587 |
. . 3
β’ (π β πΉ:π΄βΆβ) |
41 | | eqidd 2734 |
. . 3
β’ ((π β§ π β π΄) β (πΉβπ) = (πΉβπ)) |
42 | 40, 1, 41 | rlim 15383 |
. 2
β’ (π β (πΉ βπ (lim
supβπΉ) β ((lim
supβπΉ) β β
β§ βπ¦ β
β+ βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < π¦)))) |
43 | 11, 37, 42 | mpbir2and 712 |
1
β’ (π β πΉ βπ (lim
supβπΉ)) |