Step | Hyp | Ref
| Expression |
1 | | limsupub2.1 |
. . . . . . 7
β’
β²ππ |
2 | | nfv 1918 |
. . . . . . 7
β’
β²π π₯ β β |
3 | 1, 2 | nfan 1903 |
. . . . . 6
β’
β²π(π β§ π₯ β β) |
4 | | nfv 1918 |
. . . . . 6
β’
β²π π β β |
5 | 3, 4 | nfan 1903 |
. . . . 5
β’
β²π((π β§ π₯ β β) β§ π β β) |
6 | | limsupub2.4 |
. . . . . . . . . 10
β’ (π β πΉ:π΄βΆβ*) |
7 | 6 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β (πΉβπ) β
β*) |
8 | 7 | ad5ant14 757 |
. . . . . . . 8
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β (πΉβπ) β
β*) |
9 | | rexr 11206 |
. . . . . . . . 9
β’ (π₯ β β β π₯ β
β*) |
10 | 9 | ad4antlr 732 |
. . . . . . . 8
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β π₯ β β*) |
11 | | pnfxr 11214 |
. . . . . . . . 9
β’ +β
β β* |
12 | 11 | a1i 11 |
. . . . . . . 8
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β +β β
β*) |
13 | | simpr 486 |
. . . . . . . 8
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β (πΉβπ) β€ π₯) |
14 | | ltpnf 13046 |
. . . . . . . . 9
β’ (π₯ β β β π₯ < +β) |
15 | 14 | ad4antlr 732 |
. . . . . . . 8
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β π₯ < +β) |
16 | 8, 10, 12, 13, 15 | xrlelttrd 13085 |
. . . . . . 7
β’
(((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β§ (πΉβπ) β€ π₯) β (πΉβπ) < +β) |
17 | 16 | ex 414 |
. . . . . 6
β’ ((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β ((πΉβπ) β€ π₯ β (πΉβπ) < +β)) |
18 | 17 | imim2d 57 |
. . . . 5
β’ ((((π β§ π₯ β β) β§ π β β) β§ π β π΄) β ((π β€ π β (πΉβπ) β€ π₯) β (π β€ π β (πΉβπ) < +β))) |
19 | 5, 18 | ralimdaa 3242 |
. . . 4
β’ (((π β§ π₯ β β) β§ π β β) β (βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ β π΄ (π β€ π β (πΉβπ) < +β))) |
20 | 19 | reximdva 3162 |
. . 3
β’ ((π β§ π₯ β β) β (βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < +β))) |
21 | 20 | imp 408 |
. 2
β’ (((π β§ π₯ β β) β§ βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < +β)) |
22 | | limsupub2.2 |
. . 3
β’
β²ππΉ |
23 | | limsupub2.3 |
. . 3
β’ (π β π΄ β β) |
24 | | limsupub2.5 |
. . 3
β’ (π β (lim supβπΉ) β
+β) |
25 | 1, 22, 23, 6, 24 | limsupub 44031 |
. 2
β’ (π β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
26 | 21, 25 | r19.29a 3156 |
1
β’ (π β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < +β)) |