Step | Hyp | Ref
| Expression |
1 | | limsupre3lem.1 |
. . 3
β’
β²ππΉ |
2 | | limsupre3lem.2 |
. . 3
β’ (π β π΄ β β) |
3 | | limsupre3lem.3 |
. . 3
β’ (π β πΉ:π΄βΆβ*) |
4 | 1, 2, 3 | limsupre2 45026 |
. 2
β’ (π β ((lim supβπΉ) β β β
(βπ¦ β β
βπ β β
βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β§ βπ¦ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦)))) |
5 | | simp2 1135 |
. . . . . . 7
β’ ((π β§ π¦ β β β§ βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ))) β π¦ β β) |
6 | | nfv 1910 |
. . . . . . . . . 10
β’
β²π(π β§ π¦ β β) |
7 | | simp3l 1199 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π β π΄ β§ (π β€ π β§ π¦ < (πΉβπ))) β π β€ π) |
8 | | simp1r 1196 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β) β§ π β π΄ β§ π¦ < (πΉβπ)) β π¦ β β) |
9 | 8 | rexrd 11280 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π β π΄ β§ π¦ < (πΉβπ)) β π¦ β β*) |
10 | 3 | ffvelcdmda 7088 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β (πΉβπ) β
β*) |
11 | 10 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β) β§ π β π΄) β (πΉβπ) β
β*) |
12 | 11 | 3adant3 1130 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π β π΄ β§ π¦ < (πΉβπ)) β (πΉβπ) β
β*) |
13 | | simp3 1136 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π β π΄ β§ π¦ < (πΉβπ)) β π¦ < (πΉβπ)) |
14 | 9, 12, 13 | xrltled 13147 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π β π΄ β§ π¦ < (πΉβπ)) β π¦ β€ (πΉβπ)) |
15 | 14 | 3adant3l 1178 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π β π΄ β§ (π β€ π β§ π¦ < (πΉβπ))) β π¦ β€ (πΉβπ)) |
16 | 7, 15 | jca 511 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π β π΄ β§ (π β€ π β§ π¦ < (πΉβπ))) β (π β€ π β§ π¦ β€ (πΉβπ))) |
17 | 16 | 3exp 1117 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (π β π΄ β ((π β€ π β§ π¦ < (πΉβπ)) β (π β€ π β§ π¦ β€ (πΉβπ))))) |
18 | 6, 17 | reximdai 3253 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β βπ β π΄ (π β€ π β§ π¦ β€ (πΉβπ)))) |
19 | 18 | ralimdv 3164 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β βπ β β βπ β π΄ (π β€ π β§ π¦ β€ (πΉβπ)))) |
20 | 19 | 3impia 1115 |
. . . . . . 7
β’ ((π β§ π¦ β β β§ βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ))) β βπ β β βπ β π΄ (π β€ π β§ π¦ β€ (πΉβπ))) |
21 | | breq1 5145 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π₯ β€ (πΉβπ) β π¦ β€ (πΉβπ))) |
22 | 21 | anbi2d 628 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π β€ π β§ π₯ β€ (πΉβπ)) β (π β€ π β§ π¦ β€ (πΉβπ)))) |
23 | 22 | rexbidv 3173 |
. . . . . . . . 9
β’ (π₯ = π¦ β (βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ β π΄ (π β€ π β§ π¦ β€ (πΉβπ)))) |
24 | 23 | ralbidv 3172 |
. . . . . . . 8
β’ (π₯ = π¦ β (βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ β β βπ β π΄ (π β€ π β§ π¦ β€ (πΉβπ)))) |
25 | 24 | rspcev 3607 |
. . . . . . 7
β’ ((π¦ β β β§
βπ β β
βπ β π΄ (π β€ π β§ π¦ β€ (πΉβπ))) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
26 | 5, 20, 25 | syl2anc 583 |
. . . . . 6
β’ ((π β§ π¦ β β β§ βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ))) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) |
27 | 26 | 3exp 1117 |
. . . . 5
β’ (π β (π¦ β β β (βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))))) |
28 | 27 | rexlimdv 3148 |
. . . 4
β’ (π β (βπ¦ β β βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
29 | | peano2rem 11543 |
. . . . . . 7
β’ (π₯ β β β (π₯ β 1) β
β) |
30 | 29 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β (π₯ β 1) β β) |
31 | | nfv 1910 |
. . . . . . . . 9
β’
β²π(π β§ π₯ β β) |
32 | | simp3l 1199 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β π β€ π) |
33 | | simp1r 1196 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β π₯ β β) |
34 | 29 | rexrd 11280 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π₯ β 1) β
β*) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β (π₯ β 1) β
β*) |
36 | 33 | rexrd 11280 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β π₯ β β*) |
37 | 10 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β) β§ π β π΄) β (πΉβπ) β
β*) |
38 | 37 | 3adant3 1130 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β (πΉβπ) β
β*) |
39 | 33 | ltm1d 12162 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β (π₯ β 1) < π₯) |
40 | | simp3r 1200 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β π₯ β€ (πΉβπ)) |
41 | 35, 36, 38, 39, 40 | xrltletrd 13158 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β (π₯ β 1) < (πΉβπ)) |
42 | 32, 41 | jca 511 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π΄ β§ (π β€ π β§ π₯ β€ (πΉβπ))) β (π β€ π β§ (π₯ β 1) < (πΉβπ))) |
43 | 42 | 3exp 1117 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (π β π΄ β ((π β€ π β§ π₯ β€ (πΉβπ)) β (π β€ π β§ (π₯ β 1) < (πΉβπ))))) |
44 | 31, 43 | reximdai 3253 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ β π΄ (π β€ π β§ (π₯ β 1) < (πΉβπ)))) |
45 | 44 | ralimdv 3164 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ β β βπ β π΄ (π β€ π β§ (π₯ β 1) < (πΉβπ)))) |
46 | 45 | imp 406 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β βπ β β βπ β π΄ (π β€ π β§ (π₯ β 1) < (πΉβπ))) |
47 | | breq1 5145 |
. . . . . . . . . 10
β’ (π¦ = (π₯ β 1) β (π¦ < (πΉβπ) β (π₯ β 1) < (πΉβπ))) |
48 | 47 | anbi2d 628 |
. . . . . . . . 9
β’ (π¦ = (π₯ β 1) β ((π β€ π β§ π¦ < (πΉβπ)) β (π β€ π β§ (π₯ β 1) < (πΉβπ)))) |
49 | 48 | rexbidv 3173 |
. . . . . . . 8
β’ (π¦ = (π₯ β 1) β (βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β βπ β π΄ (π β€ π β§ (π₯ β 1) < (πΉβπ)))) |
50 | 49 | ralbidv 3172 |
. . . . . . 7
β’ (π¦ = (π₯ β 1) β (βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β βπ β β βπ β π΄ (π β€ π β§ (π₯ β 1) < (πΉβπ)))) |
51 | 50 | rspcev 3607 |
. . . . . 6
β’ (((π₯ β 1) β β β§
βπ β β
βπ β π΄ (π β€ π β§ (π₯ β 1) < (πΉβπ))) β βπ¦ β β βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ))) |
52 | 30, 46, 51 | syl2anc 583 |
. . . . 5
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β βπ¦ β β βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ))) |
53 | 52 | rexlimdva2 3152 |
. . . 4
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β βπ¦ β β βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)))) |
54 | 28, 53 | impbid 211 |
. . 3
β’ (π β (βπ¦ β β βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) |
55 | | simplr 768 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦)) β π¦ β β) |
56 | 11 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π β π΄) β§ (πΉβπ) < π¦) β (πΉβπ) β
β*) |
57 | | rexr 11276 |
. . . . . . . . . . . . 13
β’ (π¦ β β β π¦ β
β*) |
58 | 57 | ad3antlr 730 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π β π΄) β§ (πΉβπ) < π¦) β π¦ β β*) |
59 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π β π΄) β§ (πΉβπ) < π¦) β (πΉβπ) < π¦) |
60 | 56, 58, 59 | xrltled 13147 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π β π΄) β§ (πΉβπ) < π¦) β (πΉβπ) β€ π¦) |
61 | 60 | ex 412 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β π΄) β ((πΉβπ) < π¦ β (πΉβπ) β€ π¦)) |
62 | 61 | imim2d 57 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π β π΄) β ((π β€ π β (πΉβπ) < π¦) β (π β€ π β (πΉβπ) β€ π¦))) |
63 | 62 | ralimdva 3162 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (βπ β π΄ (π β€ π β (πΉβπ) < π¦) β βπ β π΄ (π β€ π β (πΉβπ) β€ π¦))) |
64 | 63 | reximdv 3165 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π¦))) |
65 | 64 | imp 406 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦)) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π¦)) |
66 | | breq2 5146 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π¦)) |
67 | 66 | imbi2d 340 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((π β€ π β (πΉβπ) β€ π₯) β (π β€ π β (πΉβπ) β€ π¦))) |
68 | 67 | ralbidv 3172 |
. . . . . . . 8
β’ (π₯ = π¦ β (βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ β π΄ (π β€ π β (πΉβπ) β€ π¦))) |
69 | 68 | rexbidv 3173 |
. . . . . . 7
β’ (π₯ = π¦ β (βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π¦))) |
70 | 69 | rspcev 3607 |
. . . . . 6
β’ ((π¦ β β β§
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) β€ π¦)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
71 | 55, 65, 70 | syl2anc 583 |
. . . . 5
β’ (((π β§ π¦ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦)) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
72 | 71 | rexlimdva2 3152 |
. . . 4
β’ (π β (βπ¦ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
73 | | peano2re 11403 |
. . . . . . 7
β’ (π₯ β β β (π₯ + 1) β
β) |
74 | 73 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (π₯ + 1) β β) |
75 | 37 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β (πΉβπ) β
β*) |
76 | | rexr 11276 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π₯ β
β*) |
77 | 76 | ad3antlr 730 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β π₯ β β*) |
78 | 73 | rexrd 11280 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π₯ + 1) β
β*) |
79 | 78 | ad3antlr 730 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β (π₯ + 1) β
β*) |
80 | | simpr 484 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β (πΉβπ) β€ π₯) |
81 | | ltp1 12070 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π₯ < (π₯ + 1)) |
82 | 81 | ad3antlr 730 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β π₯ < (π₯ + 1)) |
83 | 75, 77, 79, 80, 82 | xrlelttrd 13157 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β (πΉβπ) < (π₯ + 1)) |
84 | 83 | ex 412 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β π΄) β ((πΉβπ) β€ π₯ β (πΉβπ) < (π₯ + 1))) |
85 | 84 | imim2d 57 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π΄) β ((π β€ π β (πΉβπ) β€ π₯) β (π β€ π β (πΉβπ) < (π₯ + 1)))) |
86 | 85 | ralimdva 3162 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ β π΄ (π β€ π β (πΉβπ) < (π₯ + 1)))) |
87 | 86 | reximdv 3165 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < (π₯ + 1)))) |
88 | 87 | imp 406 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < (π₯ + 1))) |
89 | | breq2 5146 |
. . . . . . . . . 10
β’ (π¦ = (π₯ + 1) β ((πΉβπ) < π¦ β (πΉβπ) < (π₯ + 1))) |
90 | 89 | imbi2d 340 |
. . . . . . . . 9
β’ (π¦ = (π₯ + 1) β ((π β€ π β (πΉβπ) < π¦) β (π β€ π β (πΉβπ) < (π₯ + 1)))) |
91 | 90 | ralbidv 3172 |
. . . . . . . 8
β’ (π¦ = (π₯ + 1) β (βπ β π΄ (π β€ π β (πΉβπ) < π¦) β βπ β π΄ (π β€ π β (πΉβπ) < (π₯ + 1)))) |
92 | 91 | rexbidv 3173 |
. . . . . . 7
β’ (π¦ = (π₯ + 1) β (βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < (π₯ + 1)))) |
93 | 92 | rspcev 3607 |
. . . . . 6
β’ (((π₯ + 1) β β β§
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) < (π₯ + 1))) β βπ¦ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦)) |
94 | 74, 88, 93 | syl2anc 583 |
. . . . 5
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β βπ¦ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦)) |
95 | 94 | rexlimdva2 3152 |
. . . 4
β’ (π β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ¦ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦))) |
96 | 72, 95 | impbid 211 |
. . 3
β’ (π β (βπ¦ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦) β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
97 | 54, 96 | anbi12d 630 |
. 2
β’ (π β ((βπ¦ β β βπ β β βπ β π΄ (π β€ π β§ π¦ < (πΉβπ)) β§ βπ¦ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π¦)) β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)))) |
98 | 4, 97 | bitrd 279 |
1
β’ (π β ((lim supβπΉ) β β β
(βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)))) |