Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . 5
β’ (((π β§ πΉ~~>*π΄) β§ π΄ β β) β πΉ~~>*π΄) |
2 | | dfxlim2v.1 |
. . . . . . . 8
β’ (π β π β β€) |
3 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β β) β π β β€) |
4 | | dfxlim2v.2 |
. . . . . . 7
β’ π =
(β€β₯βπ) |
5 | | dfxlim2v.3 |
. . . . . . . 8
β’ (π β πΉ:πβΆβ*) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β β) β πΉ:πβΆβ*) |
7 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π΄ β β) β π΄ β β) |
8 | 3, 4, 6, 7 | xlimclim2 44167 |
. . . . . 6
β’ ((π β§ π΄ β β) β (πΉ~~>*π΄ β πΉ β π΄)) |
9 | 8 | adantlr 714 |
. . . . 5
β’ (((π β§ πΉ~~>*π΄) β§ π΄ β β) β (πΉ~~>*π΄ β πΉ β π΄)) |
10 | 1, 9 | mpbid 231 |
. . . 4
β’ (((π β§ πΉ~~>*π΄) β§ π΄ β β) β πΉ β π΄) |
11 | 10 | 3mix1d 1337 |
. . 3
β’ (((π β§ πΉ~~>*π΄) β§ π΄ β β) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
12 | | simpr 486 |
. . . . . 6
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = -β) β π΄ = -β) |
13 | | simpl 484 |
. . . . . . . . 9
β’ ((πΉ~~>*π΄ β§ π΄ = -β) β πΉ~~>*π΄) |
14 | | simpr 486 |
. . . . . . . . 9
β’ ((πΉ~~>*π΄ β§ π΄ = -β) β π΄ = -β) |
15 | 13, 14 | breqtrd 5132 |
. . . . . . . 8
β’ ((πΉ~~>*π΄ β§ π΄ = -β) β πΉ~~>*-β) |
16 | 15 | adantll 713 |
. . . . . . 7
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = -β) β πΉ~~>*-β) |
17 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππΉ |
18 | 17, 2, 4, 5 | xlimmnf 44168 |
. . . . . . . 8
β’ (π β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
19 | 18 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = -β) β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
20 | 16, 19 | mpbid 231 |
. . . . . 6
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = -β) β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
21 | | 3mix2 1332 |
. . . . . 6
β’ ((π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
22 | 12, 20, 21 | syl2anc 585 |
. . . . 5
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = -β) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
23 | 22 | adantlr 714 |
. . . 4
β’ ((((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β§ π΄ = -β) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
24 | | simpll 766 |
. . . . 5
β’ ((((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β§ Β¬ π΄ = -β) β (π β§ πΉ~~>*π΄)) |
25 | | xlimcl 44149 |
. . . . . . 7
β’ (πΉ~~>*π΄ β π΄ β
β*) |
26 | 25 | ad3antlr 730 |
. . . . . 6
β’ ((((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β§ Β¬ π΄ = -β) β π΄ β
β*) |
27 | | simplr 768 |
. . . . . 6
β’ ((((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β§ Β¬ π΄ = -β) β Β¬ π΄ β
β) |
28 | | neqne 2948 |
. . . . . . 7
β’ (Β¬
π΄ = -β β π΄ β -β) |
29 | 28 | adantl 483 |
. . . . . 6
β’ ((((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β§ Β¬ π΄ = -β) β π΄ β -β) |
30 | 26, 27, 29 | xrnmnfpnf 43381 |
. . . . 5
β’ ((((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β§ Β¬ π΄ = -β) β π΄ = +β) |
31 | | simpr 486 |
. . . . . 6
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = +β) β π΄ = +β) |
32 | | simpl 484 |
. . . . . . . . 9
β’ ((πΉ~~>*π΄ β§ π΄ = +β) β πΉ~~>*π΄) |
33 | | simpr 486 |
. . . . . . . . 9
β’ ((πΉ~~>*π΄ β§ π΄ = +β) β π΄ = +β) |
34 | 32, 33 | breqtrd 5132 |
. . . . . . . 8
β’ ((πΉ~~>*π΄ β§ π΄ = +β) β πΉ~~>*+β) |
35 | 34 | adantll 713 |
. . . . . . 7
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = +β) β πΉ~~>*+β) |
36 | 17, 2, 4, 5 | xlimpnf 44169 |
. . . . . . . 8
β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
37 | 36 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = +β) β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
38 | 35, 37 | mpbid 231 |
. . . . . 6
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = +β) β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
39 | | 3mix3 1333 |
. . . . . 6
β’ ((π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
40 | 31, 38, 39 | syl2anc 585 |
. . . . 5
β’ (((π β§ πΉ~~>*π΄) β§ π΄ = +β) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
41 | 24, 30, 40 | syl2anc 585 |
. . . 4
β’ ((((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β§ Β¬ π΄ = -β) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
42 | 23, 41 | pm2.61dan 812 |
. . 3
β’ (((π β§ πΉ~~>*π΄) β§ Β¬ π΄ β β) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
43 | 11, 42 | pm2.61dan 812 |
. 2
β’ ((π β§ πΉ~~>*π΄) β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) |
44 | 2 | adantr 482 |
. . . 4
β’ ((π β§ πΉ β π΄) β π β β€) |
45 | 5 | adantr 482 |
. . . 4
β’ ((π β§ πΉ β π΄) β πΉ:πβΆβ*) |
46 | | simpr 486 |
. . . 4
β’ ((π β§ πΉ β π΄) β πΉ β π΄) |
47 | 44, 4, 45, 46 | climxlim2 44173 |
. . 3
β’ ((π β§ πΉ β π΄) β πΉ~~>*π΄) |
48 | 18 | biimpar 479 |
. . . . 5
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β πΉ~~>*-β) |
49 | 48 | adantrl 715 |
. . . 4
β’ ((π β§ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) β πΉ~~>*-β) |
50 | | simprl 770 |
. . . 4
β’ ((π β§ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) β π΄ = -β) |
51 | 49, 50 | breqtrrd 5134 |
. . 3
β’ ((π β§ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) β πΉ~~>*π΄) |
52 | 36 | biimpar 479 |
. . . . 5
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β πΉ~~>*+β) |
53 | 52 | adantrl 715 |
. . . 4
β’ ((π β§ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) β πΉ~~>*+β) |
54 | | simprl 770 |
. . . 4
β’ ((π β§ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) β π΄ = +β) |
55 | 53, 54 | breqtrrd 5134 |
. . 3
β’ ((π β§ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) β πΉ~~>*π΄) |
56 | 47, 51, 55 | 3jaodan 1431 |
. 2
β’ ((π β§ (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)))) β πΉ~~>*π΄) |
57 | 43, 56 | impbida 800 |
1
β’ (π β (πΉ~~>*π΄ β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))))) |