Step | Hyp | Ref
| Expression |
1 | | limsupref.a |
. 2
β’ (π β π΄ β β) |
2 | | limsupref.s |
. 2
β’ (π β sup(π΄, β*, < ) =
+β) |
3 | | limsupref.f |
. 2
β’ (π β πΉ:π΄βΆβ) |
4 | | limsupref.b |
. . 3
β’ (π β βπ β β βπ β β βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π)) |
5 | | breq2 5152 |
. . . . . 6
β’ (π = π¦ β ((absβ(πΉβπ)) β€ π β (absβ(πΉβπ)) β€ π¦)) |
6 | 5 | imbi2d 340 |
. . . . 5
β’ (π = π¦ β ((π β€ π β (absβ(πΉβπ)) β€ π) β (π β€ π β (absβ(πΉβπ)) β€ π¦))) |
7 | 6 | ralbidv 3177 |
. . . 4
β’ (π = π¦ β (βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π) β βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π¦))) |
8 | | breq1 5151 |
. . . . . . 7
β’ (π = π β (π β€ π β π β€ π)) |
9 | 8 | imbi1d 341 |
. . . . . 6
β’ (π = π β ((π β€ π β (absβ(πΉβπ)) β€ π¦) β (π β€ π β (absβ(πΉβπ)) β€ π¦))) |
10 | 9 | ralbidv 3177 |
. . . . 5
β’ (π = π β (βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π¦) β βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π¦))) |
11 | | nfv 1917 |
. . . . . . 7
β’
β²π₯(π β€ π β (absβ(πΉβπ)) β€ π¦) |
12 | | nfv 1917 |
. . . . . . . 8
β’
β²π π β€ π₯ |
13 | | nfcv 2903 |
. . . . . . . . . 10
β’
β²πabs |
14 | | limsupref.j |
. . . . . . . . . . 11
β’
β²ππΉ |
15 | | nfcv 2903 |
. . . . . . . . . . 11
β’
β²ππ₯ |
16 | 14, 15 | nffv 6901 |
. . . . . . . . . 10
β’
β²π(πΉβπ₯) |
17 | 13, 16 | nffv 6901 |
. . . . . . . . 9
β’
β²π(absβ(πΉβπ₯)) |
18 | | nfcv 2903 |
. . . . . . . . 9
β’
β²π
β€ |
19 | | nfcv 2903 |
. . . . . . . . 9
β’
β²ππ¦ |
20 | 17, 18, 19 | nfbr 5195 |
. . . . . . . 8
β’
β²π(absβ(πΉβπ₯)) β€ π¦ |
21 | 12, 20 | nfim 1899 |
. . . . . . 7
β’
β²π(π β€ π₯ β (absβ(πΉβπ₯)) β€ π¦) |
22 | | breq2 5152 |
. . . . . . . 8
β’ (π = π₯ β (π β€ π β π β€ π₯)) |
23 | | 2fveq3 6896 |
. . . . . . . . 9
β’ (π = π₯ β (absβ(πΉβπ)) = (absβ(πΉβπ₯))) |
24 | 23 | breq1d 5158 |
. . . . . . . 8
β’ (π = π₯ β ((absβ(πΉβπ)) β€ π¦ β (absβ(πΉβπ₯)) β€ π¦)) |
25 | 22, 24 | imbi12d 344 |
. . . . . . 7
β’ (π = π₯ β ((π β€ π β (absβ(πΉβπ)) β€ π¦) β (π β€ π₯ β (absβ(πΉβπ₯)) β€ π¦))) |
26 | 11, 21, 25 | cbvralw 3303 |
. . . . . 6
β’
(βπ β
π΄ (π β€ π β (absβ(πΉβπ)) β€ π¦) β βπ₯ β π΄ (π β€ π₯ β (absβ(πΉβπ₯)) β€ π¦)) |
27 | 26 | a1i 11 |
. . . . 5
β’ (π = π β (βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π¦) β βπ₯ β π΄ (π β€ π₯ β (absβ(πΉβπ₯)) β€ π¦))) |
28 | 10, 27 | bitrd 278 |
. . . 4
β’ (π = π β (βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π¦) β βπ₯ β π΄ (π β€ π₯ β (absβ(πΉβπ₯)) β€ π¦))) |
29 | 7, 28 | cbvrex2vw 3239 |
. . 3
β’
(βπ β
β βπ β
β βπ β
π΄ (π β€ π β (absβ(πΉβπ)) β€ π) β βπ¦ β β βπ β β βπ₯ β π΄ (π β€ π₯ β (absβ(πΉβπ₯)) β€ π¦)) |
30 | 4, 29 | sylib 217 |
. 2
β’ (π β βπ¦ β β βπ β β βπ₯ β π΄ (π β€ π₯ β (absβ(πΉβπ₯)) β€ π¦)) |
31 | 1, 2, 3, 30 | limsupre 44347 |
1
β’ (π β (lim supβπΉ) β
β) |