Step | Hyp | Ref
| Expression |
1 | | limsupre2lem.3 |
. . . . 5
β’ (π β πΉ:π΄βΆβ*) |
2 | | reex 11201 |
. . . . . . 7
β’ β
β V |
3 | 2 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
4 | | limsupre2lem.2 |
. . . . . 6
β’ (π β π΄ β β) |
5 | 3, 4 | ssexd 5325 |
. . . . 5
β’ (π β π΄ β V) |
6 | 1, 5 | fexd 7229 |
. . . 4
β’ (π β πΉ β V) |
7 | 6 | limsupcld 44406 |
. . 3
β’ (π β (lim supβπΉ) β
β*) |
8 | | xrre4 44121 |
. . 3
β’ ((lim
supβπΉ) β
β* β ((lim supβπΉ) β β β ((lim
supβπΉ) β -β
β§ (lim supβπΉ)
β +β))) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β ((lim supβπΉ) β β β ((lim
supβπΉ) β -β
β§ (lim supβπΉ)
β +β))) |
10 | | df-ne 2942 |
. . . . 5
β’ ((lim
supβπΉ) β -β
β Β¬ (lim supβπΉ) = -β) |
11 | 10 | a1i 11 |
. . . 4
β’ (π β ((lim supβπΉ) β -β β Β¬
(lim supβπΉ) =
-β)) |
12 | | limsupre2lem.1 |
. . . . . 6
β’
β²ππΉ |
13 | 12, 4, 1 | limsupmnf 44437 |
. . . . 5
β’ (π β ((lim supβπΉ) = -β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
14 | 13 | notbid 318 |
. . . 4
β’ (π β (Β¬ (lim
supβπΉ) = -β
β Β¬ βπ₯
β β βπ
β β βπ
β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
15 | | annim 405 |
. . . . . . . . . . . 12
β’ ((π β€ π β§ Β¬ (πΉβπ) β€ π₯) β Β¬ (π β€ π β (πΉβπ) β€ π₯)) |
16 | 15 | rexbii 3095 |
. . . . . . . . . . 11
β’
(βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β π΄ Β¬ (π β€ π β (πΉβπ) β€ π₯)) |
17 | | rexnal 3101 |
. . . . . . . . . . 11
β’
(βπ β
π΄ Β¬ (π β€ π β (πΉβπ) β€ π₯) β Β¬ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
18 | 16, 17 | bitri 275 |
. . . . . . . . . 10
β’
(βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β Β¬ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
19 | 18 | ralbii 3094 |
. . . . . . . . 9
β’
(βπ β
β βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β β Β¬ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
20 | | ralnex 3073 |
. . . . . . . . 9
β’
(βπ β
β Β¬ βπ
β π΄ (π β€ π β (πΉβπ) β€ π₯) β Β¬ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
21 | 19, 20 | bitri 275 |
. . . . . . . 8
β’
(βπ β
β βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β Β¬ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
22 | 21 | rexbii 3095 |
. . . . . . 7
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ₯ β β Β¬ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
23 | | rexnal 3101 |
. . . . . . 7
β’
(βπ₯ β
β Β¬ βπ
β β βπ
β π΄ (π β€ π β (πΉβπ) β€ π₯) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
24 | 22, 23 | bitr2i 276 |
. . . . . 6
β’ (Β¬
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯)) |
25 | 24 | a1i 11 |
. . . . 5
β’ (π β (Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯))) |
26 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π΄) β π₯ β β) |
27 | 26 | rexrd 11264 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π΄) β π₯ β β*) |
28 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β πΉ:π΄βΆβ*) |
29 | 28 | ffvelcdmda 7087 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π΄) β (πΉβπ) β
β*) |
30 | 27, 29 | xrltnled 44073 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π΄) β (π₯ < (πΉβπ) β Β¬ (πΉβπ) β€ π₯)) |
31 | 30 | bicomd 222 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π΄) β (Β¬ (πΉβπ) β€ π₯ β π₯ < (πΉβπ))) |
32 | 31 | anbi2d 630 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β π΄) β ((π β€ π β§ Β¬ (πΉβπ) β€ π₯) β (π β€ π β§ π₯ < (πΉβπ)))) |
33 | 32 | rexbidva 3177 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
34 | 33 | ralbidv 3178 |
. . . . . 6
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
35 | 34 | rexbidva 3177 |
. . . . 5
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
36 | 25, 35 | bitrd 279 |
. . . 4
β’ (π β (Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
37 | 11, 14, 36 | 3bitrd 305 |
. . 3
β’ (π β ((lim supβπΉ) β -β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
38 | | df-ne 2942 |
. . . . 5
β’ ((lim
supβπΉ) β +β
β Β¬ (lim supβπΉ) = +β) |
39 | 38 | a1i 11 |
. . . 4
β’ (π β ((lim supβπΉ) β +β β Β¬
(lim supβπΉ) =
+β)) |
40 | 12, 4, 1 | limsuppnf 44427 |
. . . . 5
β’ (π β ((lim supβπΉ) = +β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
41 | 40 | notbid 318 |
. . . 4
β’ (π β (Β¬ (lim
supβπΉ) = +β
β Β¬ βπ₯
β β βπ
β β βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
42 | 29, 27 | xrltnled 44073 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π΄) β ((πΉβπ) < π₯ β Β¬ π₯ β€ (πΉβπ))) |
43 | 42 | imbi2d 341 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β π΄) β ((π β€ π β (πΉβπ) < π₯) β (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
44 | 43 | ralbidva 3176 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (βπ β π΄ (π β€ π β (πΉβπ) < π₯) β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
45 | 44 | rexbidv 3179 |
. . . . . 6
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯) β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
46 | 45 | rexbidva 3177 |
. . . . 5
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
47 | | imnan 401 |
. . . . . . . . . . . 12
β’ ((π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ (π β€ π β§ π₯ β€ (πΉβπ))) |
48 | 47 | ralbii 3094 |
. . . . . . . . . . 11
β’
(βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β π΄ Β¬ (π β€ π β§ π₯ β€ (πΉβπ))) |
49 | | ralnex 3073 |
. . . . . . . . . . 11
β’
(βπ β
π΄ Β¬ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
50 | 48, 49 | bitri 275 |
. . . . . . . . . 10
β’
(βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
51 | 50 | rexbii 3095 |
. . . . . . . . 9
β’
(βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
52 | | rexnal 3101 |
. . . . . . . . 9
β’
(βπ β
β Β¬ βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
53 | 51, 52 | bitri 275 |
. . . . . . . 8
β’
(βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
54 | 53 | rexbii 3095 |
. . . . . . 7
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ₯ β β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
55 | | rexnal 3101 |
. . . . . . 7
β’
(βπ₯ β
β Β¬ βπ
β β βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
56 | 54, 55 | bitri 275 |
. . . . . 6
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
57 | 56 | a1i 11 |
. . . . 5
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
58 | 46, 57 | bitr2d 280 |
. . . 4
β’ (π β (Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯))) |
59 | 39, 41, 58 | 3bitrd 305 |
. . 3
β’ (π β ((lim supβπΉ) β +β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) < π₯))) |
60 | 37, 59 | anbi12d 632 |
. 2
β’ (π β (((lim supβπΉ) β -β β§ (lim
supβπΉ) β +β)
β (βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β§ π₯ < (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯)))) |
61 | 9, 60 | bitrd 279 |
1
β’ (π β ((lim supβπΉ) β β β
(βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯)))) |