Step | Hyp | Ref
| Expression |
1 | | dfxlim2.m |
. . 3
β’ (π β π β β€) |
2 | | dfxlim2.z |
. . 3
β’ π =
(β€β₯βπ) |
3 | | dfxlim2.f |
. . 3
β’ (π β πΉ:πβΆβ*) |
4 | 1, 2, 3 | dfxlim2v 44174 |
. 2
β’ (π β (πΉ~~>*π΄ β (πΉ β π΄ β¨ (π΄ = -β β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦) β¨ (π΄ = +β β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ))))) |
5 | | biid 261 |
. . 3
β’ (πΉ β π΄ β πΉ β π΄) |
6 | | breq2 5110 |
. . . . . . 7
β’ (π¦ = π₯ β ((πΉβπ) β€ π¦ β (πΉβπ) β€ π₯)) |
7 | 6 | rexralbidv 3211 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
8 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
9 | 8 | raleqdv 3312 |
. . . . . . . 8
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
10 | | dfxlim2.k |
. . . . . . . . . . 11
β’
β²ππΉ |
11 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππ |
12 | 10, 11 | nffv 6853 |
. . . . . . . . . 10
β’
β²π(πΉβπ) |
13 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π
β€ |
14 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²ππ₯ |
15 | 12, 13, 14 | nfbr 5153 |
. . . . . . . . 9
β’
β²π(πΉβπ) β€ π₯ |
16 | | nfv 1918 |
. . . . . . . . 9
β’
β²π(πΉβπ) β€ π₯ |
17 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
18 | 17 | breq1d 5116 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) |
19 | 15, 16, 18 | cbvralw 3288 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
20 | 9, 19 | bitrdi 287 |
. . . . . . 7
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
21 | 20 | cbvrexvw 3225 |
. . . . . 6
β’
(βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
22 | 7, 21 | bitrdi 287 |
. . . . 5
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
23 | 22 | cbvralvw 3224 |
. . . 4
β’
(βπ¦ β
β βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π¦ β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
24 | 23 | anbi2i 624 |
. . 3
β’ ((π΄ = -β β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦) β (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
25 | | breq1 5109 |
. . . . . . 7
β’ (π¦ = π₯ β (π¦ β€ (πΉβπ) β π₯ β€ (πΉβπ))) |
26 | 25 | rexralbidv 3211 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
27 | 8 | raleqdv 3312 |
. . . . . . . 8
β’ (π = π β (βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
28 | 14, 13, 12 | nfbr 5153 |
. . . . . . . . 9
β’
β²π π₯ β€ (πΉβπ) |
29 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π₯ β€ (πΉβπ) |
30 | 17 | breq2d 5118 |
. . . . . . . . 9
β’ (π = π β (π₯ β€ (πΉβπ) β π₯ β€ (πΉβπ))) |
31 | 28, 29, 30 | cbvralw 3288 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
32 | 27, 31 | bitrdi 287 |
. . . . . . 7
β’ (π = π β (βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
33 | 32 | cbvrexvw 3225 |
. . . . . 6
β’
(βπ β
π βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
34 | 26, 33 | bitrdi 287 |
. . . . 5
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
35 | 34 | cbvralvw 3224 |
. . . 4
β’
(βπ¦ β
β βπ β
π βπ β
(β€β₯βπ)π¦ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
36 | 35 | anbi2i 624 |
. . 3
β’ ((π΄ = +β β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) β (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
37 | 5, 24, 36 | 3orbi123i 1157 |
. 2
β’ ((πΉ β π΄ β¨ (π΄ = -β β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦) β¨ (π΄ = +β β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ))) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
38 | 4, 37 | bitrdi 287 |
1
β’ (π β (πΉ~~>*π΄ β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))))) |