Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . 7
β’ (π β π) |
2 | | imnan 401 |
. . . . . . . . . . . . . 14
β’ ((π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ (π β€ π β§ π₯ β€ (πΉβπ))) |
3 | 2 | ralbii 3093 |
. . . . . . . . . . . . 13
β’
(βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β π΄ Β¬ (π β€ π β§ π₯ β€ (πΉβπ))) |
4 | | ralnex 3072 |
. . . . . . . . . . . . 13
β’
(βπ β
π΄ Β¬ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
5 | 3, 4 | bitri 275 |
. . . . . . . . . . . 12
β’
(βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
6 | 5 | rexbii 3094 |
. . . . . . . . . . 11
β’
(βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β β Β¬ βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
7 | | rexnal 3100 |
. . . . . . . . . . 11
β’
(βπ β
β Β¬ βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
8 | 6, 7 | bitri 275 |
. . . . . . . . . 10
β’
(βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
9 | 8 | rexbii 3094 |
. . . . . . . . 9
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ₯ β β Β¬ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
10 | | rexnal 3100 |
. . . . . . . . 9
β’
(βπ₯ β
β Β¬ βπ
β β βπ
β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
11 | 9, 10 | bitri 275 |
. . . . . . . 8
β’
(βπ₯ β
β βπ β
β βπ β
π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
12 | 11 | biimpri 227 |
. . . . . . 7
β’ (Β¬
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ))) |
13 | | simp1 1137 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β§ π β€ π) β (((π β§ π₯ β β) β§ π β β) β§ π β π΄)) |
14 | | id 22 |
. . . . . . . . . . . . . . 15
β’ ((π β€ π β Β¬ π₯ β€ (πΉβπ)) β (π β€ π β Β¬ π₯ β€ (πΉβπ))) |
15 | 14 | imp 408 |
. . . . . . . . . . . . . 14
β’ (((π β€ π β Β¬ π₯ β€ (πΉβπ)) β§ π β€ π) β Β¬ π₯ β€ (πΉβπ)) |
16 | 15 | 3adant1 1131 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β§ π β€ π) β Β¬ π₯ β€ (πΉβπ)) |
17 | | limsuppnflem.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:π΄βΆβ*) |
18 | 17 | ffvelcdmda 7041 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β (πΉβπ) β
β*) |
19 | 18 | ad4ant14 751 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β (πΉβπ) β
β*) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β (πΉβπ) β
β*) |
21 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β π₯ β β) |
22 | | rexr 11211 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β π₯ β
β*) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β π₯ β β*) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β π₯ β β*) |
25 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β Β¬ π₯ β€ (πΉβπ)) |
26 | 18 | ad4ant13 750 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β (πΉβπ) β
β*) |
27 | 22 | ad3antlr 730 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β π₯ β β*) |
28 | 26, 27 | xrltnled 43700 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β ((πΉβπ) < π₯ β Β¬ π₯ β€ (πΉβπ))) |
29 | 25, 28 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β (πΉβπ) < π₯) |
30 | 29 | adantllr 718 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β (πΉβπ) < π₯) |
31 | 20, 24, 30 | xrltled 13080 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ Β¬ π₯ β€ (πΉβπ)) β (πΉβπ) β€ π₯) |
32 | 13, 16, 31 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β§ π β€ π) β (πΉβπ) β€ π₯) |
33 | 32 | 3exp 1120 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β ((π β€ π β Β¬ π₯ β€ (πΉβπ)) β (π β€ π β (πΉβπ) β€ π₯))) |
34 | 33 | ralimdva 3161 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β β) β (βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
35 | 34 | reximdva 3162 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
36 | 35 | reximdva 3162 |
. . . . . . . 8
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
37 | 36 | imp 408 |
. . . . . . 7
β’ ((π β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β Β¬ π₯ β€ (πΉβπ))) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
38 | 1, 12, 37 | syl2an 597 |
. . . . . 6
β’ ((π β§ Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
39 | | reex 11152 |
. . . . . . . . . . . . . 14
β’ β
β V |
40 | 39 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β β
V) |
41 | | limsuppnflem.a |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
42 | 40, 41 | ssexd 5287 |
. . . . . . . . . . . 12
β’ (π β π΄ β V) |
43 | 17, 42 | fexd 7183 |
. . . . . . . . . . 11
β’ (π β πΉ β V) |
44 | 43 | limsupcld 44033 |
. . . . . . . . . 10
β’ (π β (lim supβπΉ) β
β*) |
45 | 44 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (lim supβπΉ) β
β*) |
46 | 22 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β π₯ β β*) |
47 | | pnfxr 11219 |
. . . . . . . . . 10
β’ +β
β β* |
48 | 47 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β +β β
β*) |
49 | | limsuppnflem.j |
. . . . . . . . . 10
β’
β²ππΉ |
50 | 41 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β π΄ β β) |
51 | 17 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β πΉ:π΄βΆβ*) |
52 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
53 | 49, 50, 51, 46, 52 | limsupbnd1f 44029 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (lim supβπΉ) β€ π₯) |
54 | | ltpnf 13051 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ < +β) |
55 | 54 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β π₯ < +β) |
56 | 45, 46, 48, 53, 55 | xrlelttrd 13090 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (lim supβπΉ) < +β) |
57 | 56 | rexlimdva2 3151 |
. . . . . . 7
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β (lim supβπΉ) < +β)) |
58 | 57 | imp 408 |
. . . . . 6
β’ ((π β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (lim supβπΉ) < +β) |
59 | 38, 58 | syldan 592 |
. . . . 5
β’ ((π β§ Β¬ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β (lim supβπΉ) < +β) |
60 | 59 | adantlr 714 |
. . . 4
β’ (((π β§ (lim supβπΉ) = +β) β§ Β¬
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β (lim supβπΉ) < +β) |
61 | | id 22 |
. . . . . . . 8
β’ ((lim
supβπΉ) = +β
β (lim supβπΉ) =
+β) |
62 | 47 | a1i 11 |
. . . . . . . 8
β’ ((lim
supβπΉ) = +β
β +β β β*) |
63 | 61, 62 | eqeltrd 2833 |
. . . . . . 7
β’ ((lim
supβπΉ) = +β
β (lim supβπΉ)
β β*) |
64 | 63, 61 | xreqnltd 43732 |
. . . . . 6
β’ ((lim
supβπΉ) = +β
β Β¬ (lim supβπΉ) < +β) |
65 | 64 | adantl 483 |
. . . . 5
β’ ((π β§ (lim supβπΉ) = +β) β Β¬ (lim
supβπΉ) <
+β) |
66 | 65 | adantr 482 |
. . . 4
β’ (((π β§ (lim supβπΉ) = +β) β§ Β¬
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β Β¬ (lim supβπΉ) <
+β) |
67 | 60, 66 | condan 817 |
. . 3
β’ ((π β§ (lim supβπΉ) = +β) β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
68 | 67 | ex 414 |
. 2
β’ (π β ((lim supβπΉ) = +β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
69 | 41 | adantr 482 |
. . . 4
β’ ((π β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β π΄ β β) |
70 | 17 | adantr 482 |
. . . 4
β’ ((π β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β πΉ:π΄βΆβ*) |
71 | | simpr 486 |
. . . 4
β’ ((π β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
72 | 49, 69, 70, 71 | limsuppnfd 44045 |
. . 3
β’ ((π β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β (lim supβπΉ) = +β) |
73 | 72 | ex 414 |
. 2
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β (lim supβπΉ) = +β)) |
74 | 68, 73 | impbid 211 |
1
β’ (π β ((lim supβπΉ) = +β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |