Step | Hyp | Ref
| Expression |
1 | | caurcvg.1 |
. . . . . 6
β’ π =
(β€β₯βπ) |
2 | | uzssz 12789 |
. . . . . 6
β’
(β€β₯βπ) β β€ |
3 | 1, 2 | eqsstri 3979 |
. . . . 5
β’ π β
β€ |
4 | | zssre 12511 |
. . . . 5
β’ β€
β β |
5 | 3, 4 | sstri 3954 |
. . . 4
β’ π β
β |
6 | 5 | a1i 11 |
. . 3
β’ (π β π β β) |
7 | | caurcvg.3 |
. . 3
β’ (π β πΉ:πβΆβ) |
8 | | 1rp 12924 |
. . . . . 6
β’ 1 β
β+ |
9 | 8 | ne0ii 4298 |
. . . . 5
β’
β+ β β
|
10 | | caurcvg.4 |
. . . . 5
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) |
11 | | r19.2z 4453 |
. . . . 5
β’
((β+ β β
β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) |
12 | 9, 10, 11 | sylancr 588 |
. . . 4
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) |
13 | | eluzel2 12773 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β β€) |
14 | 13, 1 | eleq2s 2852 |
. . . . . . . 8
β’ (π β π β π β β€) |
15 | 1 | uzsup 13774 |
. . . . . . . 8
β’ (π β β€ β sup(π, β*, < ) =
+β) |
16 | 14, 15 | syl 17 |
. . . . . . 7
β’ (π β π β sup(π, β*, < ) =
+β) |
17 | 16 | a1d 25 |
. . . . . 6
β’ (π β π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β sup(π, β*, < ) =
+β)) |
18 | 17 | rexlimiv 3142 |
. . . . 5
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β sup(π, β*, < ) =
+β) |
19 | 18 | rexlimivw 3145 |
. . . 4
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β sup(π, β*, < ) =
+β) |
20 | 12, 19 | syl 17 |
. . 3
β’ (π β sup(π, β*, < ) =
+β) |
21 | 3 | sseli 3941 |
. . . . . . . . . . . 12
β’ (π β π β π β β€) |
22 | 3 | sseli 3941 |
. . . . . . . . . . . 12
β’ (π β π β π β β€) |
23 | | eluz 12782 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β (π β
(β€β₯βπ) β π β€ π)) |
24 | 21, 22, 23 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (π β (β€β₯βπ) β π β€ π)) |
25 | 24 | biimprd 248 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β (π β€ π β π β (β€β₯βπ))) |
26 | 25 | expimpd 455 |
. . . . . . . . 9
β’ (π β π β ((π β π β§ π β€ π) β π β (β€β₯βπ))) |
27 | 26 | imim1d 82 |
. . . . . . . 8
β’ (π β π β ((π β (β€β₯βπ) β (absβ((πΉβπ) β (πΉβπ))) < π₯) β ((π β π β§ π β€ π) β (absβ((πΉβπ) β (πΉβπ))) < π₯))) |
28 | 27 | exp4a 433 |
. . . . . . 7
β’ (π β π β ((π β (β€β₯βπ) β (absβ((πΉβπ) β (πΉβπ))) < π₯) β (π β π β (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)))) |
29 | 28 | ralimdv2 3157 |
. . . . . 6
β’ (π β π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β βπ β π (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯))) |
30 | 29 | reximia 3081 |
. . . . 5
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β βπ β π βπ β π (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
31 | 30 | ralimi 3083 |
. . . 4
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β βπ₯ β β+ βπ β π βπ β π (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
32 | 10, 31 | syl 17 |
. . 3
β’ (π β βπ₯ β β+ βπ β π βπ β π (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
33 | 6, 7, 20, 32 | caurcvgr 15564 |
. 2
β’ (π β πΉ βπ (lim
supβπΉ)) |
34 | 14 | a1d 25 |
. . . . . 6
β’ (π β π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β π β β€)) |
35 | 34 | rexlimiv 3142 |
. . . . 5
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β π β β€) |
36 | 35 | rexlimivw 3145 |
. . . 4
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯ β π β β€) |
37 | 12, 36 | syl 17 |
. . 3
β’ (π β π β β€) |
38 | | ax-resscn 11113 |
. . . 4
β’ β
β β |
39 | | fss 6686 |
. . . 4
β’ ((πΉ:πβΆβ β§ β β
β) β πΉ:πβΆβ) |
40 | 7, 38, 39 | sylancl 587 |
. . 3
β’ (π β πΉ:πβΆβ) |
41 | 1, 37, 40 | rlimclim 15434 |
. 2
β’ (π β (πΉ βπ (lim
supβπΉ) β πΉ β (lim supβπΉ))) |
42 | 33, 41 | mpbid 231 |
1
β’ (π β πΉ β (lim supβπΉ)) |