Step | Hyp | Ref
| Expression |
1 | | limsupre2lem.3 |
. . . . 5
β’ (π β πΉ:π΄βΆβ*) |
2 | | reex 11166 |
. . . . . . 7
β’ β
β V |
3 | 2 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
4 | | limsupre2lem.2 |
. . . . . 6
β’ (π β π΄ β β) |
5 | 3, 4 | ssexd 5301 |
. . . . 5
β’ (π β π΄ β V) |
6 | 1, 5 | fexd 7197 |
. . . 4
β’ (π β πΉ β V) |
7 | 6 | limsupcld 44084 |
. . 3
β’ (π β (lim supβπΉ) β
β*) |
8 | | xrre4 43799 |
. . 3
β’ ((lim
supβπΉ) β
β* β ((lim supβπΉ) β β β ((lim
supβπΉ) β -β
β§ (lim supβπΉ)
β +β))) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β ((lim supβπΉ) β β β ((lim
supβπΉ) β -β
β§ (lim supβπΉ)
β +β))) |
10 | | df-ne 2940 |
. . . . 5
β’ ((lim
supβπΉ) β -β
β Β¬ (lim supβπΉ) = -β) |
11 | 10 | a1i 11 |
. . . 4
β’ (π β ((lim supβπΉ) β -β β Β¬
(lim supβπΉ) =
-β)) |
12 | | limsupre2lem.1 |
. . . . . 6
β’
β²ππΉ |
13 | 12, 4, 1 | limsupmnf 44115 |
. . . . 5
β’ (π β ((lim supβπΉ) = -β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
14 | 13 | notbid 317 |
. . . 4
β’ (π β (Β¬ (lim
supβπΉ) = -β
β Β¬ βπ₯
β β βπ
β β βπ
β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
15 | | annim 404 |
. . . . . . . . . . . 12
β’ ((π β€ π β§ Β¬ (πΉβπ) β€ π₯) β Β¬ (π β€ π β (πΉβπ) β€ π₯)) |
16 | 15 | rexbii 3093 |
. . . . . . . . . . 11
β’
(βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β π΄ Β¬ (π β€ π β (πΉβπ) β€ π₯)) |
17 | | rexnal 3099 |
. . . . . . . . . . 11
β’
(βπ β
π΄ Β¬ (π β€ π β (πΉβπ) β€ π₯) β Β¬ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
18 | 16, 17 | bitri 274 |
. . . . . . . . . 10
β’
(βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β Β¬ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
19 | 18 | ralbii 3092 |
. . . . . . . . 9
β’
(βπ β
β βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β β Β¬ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
20 | | ralnex 3071 |
. . . . . . . . 9
β’
(βπ β
β Β¬ βπ
β π΄ (π β€ π β (πΉβπ) β€ π₯) β Β¬ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
21 | 19, 20 | bitri 274 |
. . . . . . . 8
β’
(βπ β
β βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β Β¬ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
22 | 21 | rexbii 3093 |
. . . . . . 7
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ₯ β β Β¬ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
23 | | rexnal 3099 |
. . . . . . 7
β’
(βπ₯ β
β Β¬ βπ
β β βπ
β π΄ (π β€ π β (πΉβπ) β€ π₯) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
24 | 22, 23 | bitr2i 275 |
. . . . . 6
β’ (Β¬
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯)) |
25 | 24 | a1i 11 |
. . . . 5
β’ (π β (Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯))) |
26 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π΄) β π₯ β β) |
27 | 26 | rexrd 11229 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π΄) β π₯ β β*) |
28 | 1 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β πΉ:π΄βΆβ*) |
29 | 28 | ffvelcdmda 7055 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π΄) β (πΉβπ) β
β*) |
30 | 27, 29 | xrltnled 43751 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π΄) β (π₯ < (πΉβπ) β Β¬ (πΉβπ) β€ π₯)) |
31 | 30 | bicomd 222 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π΄) β (Β¬ (πΉβπ) β€ π₯ β π₯ < (πΉβπ))) |
32 | 31 | anbi2d 629 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β π΄) β ((π β€ π β§ Β¬ (πΉβπ) β€ π₯) β (π β€ π β§ π₯ < (πΉβπ)))) |
33 | 32 | rexbidva 3175 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
34 | 33 | ralbidv 3176 |
. . . . . 6
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
35 | 34 | rexbidva 3175 |
. . . . 5
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ Β¬ (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
36 | 25, 35 | bitrd 278 |
. . . 4
β’ (π β (Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
37 | 11, 14, 36 | 3bitrd 304 |
. . 3
β’ (π β ((lim supβπΉ) β -β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)))) |
38 | | df-ne 2940 |
. . . . 5
β’ ((lim
supβπΉ) β +β
β Β¬ (lim supβπΉ) = +β) |
39 | 38 | a1i 11 |
. . . 4
β’ (π β ((lim supβπΉ) β +β β Β¬
(lim supβπΉ) =
+β)) |
40 | 12, 4, 1 | limsuppnf 44105 |
. . . . 5
β’ (π β ((lim supβπΉ) = +β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
41 | 40 | notbid 317 |
. . . 4
β’ (π β (Β¬ (lim
supβπΉ) = +β
β Β¬ βπ₯
β β βπ
β β βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
42 | 29, 27 | xrltnled 43751 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π΄) β ((πΉβπ) < π₯ β Β¬ π₯ β€ (πΉβπ))) |
43 | 42 | imbi2d 340 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β π΄) β ((π β€ π β (πΉβπ) < π₯) β (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
44 | 43 | ralbidva 3174 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (βπ β π΄ (π β€ π β (πΉβπ) < π₯) β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
45 | 44 | rexbidv 3177 |
. . . . . 6
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯) β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
46 | 45 | rexbidva 3175 |
. . . . 5
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)))) |
47 | | imnan 400 |
. . . . . . . . . . . 12
β’ ((π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ (π β€ π β§ π₯ β€ (πΉβπ))) |
48 | 47 | ralbii 3092 |
. . . . . . . . . . 11
β’
(βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β π΄ Β¬ (π β€ π β§ π₯ β€ (πΉβπ))) |
49 | | ralnex 3071 |
. . . . . . . . . . 11
β’
(βπ β
π΄ Β¬ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
50 | 48, 49 | bitri 274 |
. . . . . . . . . 10
β’
(βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
51 | 50 | rexbii 3093 |
. . . . . . . . 9
β’
(βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
52 | | rexnal 3099 |
. . . . . . . . 9
β’
(βπ β
β Β¬ βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
53 | 51, 52 | bitri 274 |
. . . . . . . 8
β’
(βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
54 | 53 | rexbii 3093 |
. . . . . . 7
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ₯ β β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
55 | | rexnal 3099 |
. . . . . . 7
β’
(βπ₯ β
β Β¬ βπ
β β βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
56 | 54, 55 | bitri 274 |
. . . . . 6
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
57 | 56 | a1i 11 |
. . . . 5
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
58 | 46, 57 | bitr2d 279 |
. . . 4
β’ (π β (Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯))) |
59 | 39, 41, 58 | 3bitrd 304 |
. . 3
β’ (π β ((lim supβπΉ) β +β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) < π₯))) |
60 | 37, 59 | anbi12d 631 |
. 2
β’ (π β (((lim supβπΉ) β -β β§ (lim
supβπΉ) β +β)
β (βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β§ π₯ < (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯)))) |
61 | 9, 60 | bitrd 278 |
1
β’ (π β ((lim supβπΉ) β β β
(βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯)))) |