Step | Hyp | Ref
| Expression |
1 | | xlimpnfxnegmnf2.j |
. . 3
β’
β²ππΉ |
2 | | xlimpnfxnegmnf2.z |
. . 3
β’ π =
(β€β₯βπ) |
3 | | xlimpnfxnegmnf2.f |
. . 3
β’ (π β πΉ:πβΆβ*) |
4 | 1, 2, 3 | xlimpnfxnegmnf 44145 |
. 2
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
5 | | xlimpnfxnegmnf2.m |
. . 3
β’ (π β π β β€) |
6 | 1, 5, 2, 3 | xlimpnf 44173 |
. 2
β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
7 | | nfmpt1 5217 |
. . . 4
β’
β²π(π β π β¦ -π(πΉβπ)) |
8 | 3 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
9 | 8 | xnegcld 13228 |
. . . . 5
β’ ((π β§ π β π) β -π(πΉβπ) β
β*) |
10 | | nfcv 2904 |
. . . . . 6
β’
β²π-π(πΉβπ) |
11 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ |
12 | 1, 11 | nffv 6856 |
. . . . . . 7
β’
β²π(πΉβπ) |
13 | 12 | nfxneg 43786 |
. . . . . 6
β’
β²π-π(πΉβπ) |
14 | | fveq2 6846 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
15 | 14 | xnegeqd 43762 |
. . . . . 6
β’ (π = π β -π(πΉβπ) = -π(πΉβπ)) |
16 | 10, 13, 15 | cbvmpt 5220 |
. . . . 5
β’ (π β π β¦ -π(πΉβπ)) = (π β π β¦ -π(πΉβπ)) |
17 | 9, 16 | fmptd 7066 |
. . . 4
β’ (π β (π β π β¦ -π(πΉβπ)):πβΆβ*) |
18 | 7, 5, 2, 17 | xlimmnf 44172 |
. . 3
β’ (π β ((π β π β¦ -π(πΉβπ))~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯)) |
19 | 2 | uztrn2 12790 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
20 | | xnegex 13136 |
. . . . . . . . 9
β’
-π(πΉβπ) β V |
21 | | fvmpt4 43555 |
. . . . . . . . 9
β’ ((π β π β§ -π(πΉβπ) β V) β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
22 | 20, 21 | mpan2 690 |
. . . . . . . 8
β’ (π β π β ((π β π β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
23 | 22 | breq1d 5119 |
. . . . . . 7
β’ (π β π β (((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β -π(πΉβπ) β€ π₯)) |
24 | 19, 23 | syl 17 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯βπ)) β (((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β -π(πΉβπ) β€ π₯)) |
25 | 24 | ralbidva 3169 |
. . . . 5
β’ (π β π β (βπ β (β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
26 | 25 | rexbiia 3092 |
. . . 4
β’
(βπ β
π βπ β
(β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯) |
27 | 26 | ralbii 3093 |
. . 3
β’
(βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)((π β π β¦ -π(πΉβπ))βπ) β€ π₯ β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯) |
28 | 18, 27 | bitrdi 287 |
. 2
β’ (π β ((π β π β¦ -π(πΉβπ))~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
29 | 4, 6, 28 | 3bitr4d 311 |
1
β’ (π β (πΉ~~>*+β β (π β π β¦ -π(πΉβπ))~~>*-β)) |