Step | Hyp | Ref
| Expression |
1 | | climxlim2lem.5 |
. . . 4
β’ (π β πΉ β π΄) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ π΄ β β) β πΉ β π΄) |
3 | | climxlim2lem.1 |
. . . . 5
β’ (π β π β β€) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β β) β π β β€) |
5 | | climxlim2lem.2 |
. . . 4
β’ π =
(β€β₯βπ) |
6 | | climxlim2lem.3 |
. . . . 5
β’ (π β πΉ:πβΆβ*) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β β) β πΉ:πβΆβ*) |
8 | | simpr 486 |
. . . 4
β’ ((π β§ π΄ β β) β π΄ β β) |
9 | 4, 5, 7, 8 | xlimclim2 44167 |
. . 3
β’ ((π β§ π΄ β β) β (πΉ~~>*π΄ β πΉ β π΄)) |
10 | 2, 9 | mpbird 257 |
. 2
β’ ((π β§ π΄ β β) β πΉ~~>*π΄) |
11 | | climxlim2lem.4 |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ) |
12 | 11 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) β β) |
13 | 12 | anim1i 616 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ (πΉβπ) β π΄) β ((πΉβπ) β β β§ (πΉβπ) β π΄)) |
14 | 13 | adantllr 718 |
. . . . . . . . 9
β’ ((((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β§ π β π) β§ (πΉβπ) β π΄) β ((πΉβπ) β β β§ (πΉβπ) β π΄)) |
15 | 6 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β πΉ:πβΆβ*) |
16 | 15 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ (((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β§ π β π) β (πΉβπ) β
β*) |
17 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β§ π β π) β βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) |
18 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΉβπ) β (π¦ β β β (πΉβπ) β β)) |
19 | | neeq1 3003 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΉβπ) β (π¦ β π΄ β (πΉβπ) β π΄)) |
20 | 18, 19 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π¦ = (πΉβπ) β ((π¦ β β β§ π¦ β π΄) β ((πΉβπ) β β β§ (πΉβπ) β π΄))) |
21 | | fvoveq1 7381 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΉβπ) β (absβ(π¦ β π΄)) = (absβ((πΉβπ) β π΄))) |
22 | 21 | breq2d 5118 |
. . . . . . . . . . . . 13
β’ (π¦ = (πΉβπ) β (π₯ β€ (absβ(π¦ β π΄)) β π₯ β€ (absβ((πΉβπ) β π΄)))) |
23 | 20, 22 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π¦ = (πΉβπ) β (((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄))) β (((πΉβπ) β β β§ (πΉβπ) β π΄) β π₯ β€ (absβ((πΉβπ) β π΄))))) |
24 | 23 | rspcva 3578 |
. . . . . . . . . . 11
β’ (((πΉβπ) β β* β§
βπ¦ β
β* ((π¦
β β β§ π¦ β
π΄) β π₯ β€ (absβ(π¦ β π΄)))) β (((πΉβπ) β β β§ (πΉβπ) β π΄) β π₯ β€ (absβ((πΉβπ) β π΄)))) |
25 | 16, 17, 24 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β§ π β π) β (((πΉβπ) β β β§ (πΉβπ) β π΄) β π₯ β€ (absβ((πΉβπ) β π΄)))) |
26 | 25 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β§ π β π) β§ (πΉβπ) β π΄) β (((πΉβπ) β β β§ (πΉβπ) β π΄) β π₯ β€ (absβ((πΉβπ) β π΄)))) |
27 | 14, 26 | mpd 15 |
. . . . . . . 8
β’ ((((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β§ π β π) β§ (πΉβπ) β π΄) β π₯ β€ (absβ((πΉβπ) β π΄))) |
28 | 27 | ex 414 |
. . . . . . 7
β’ (((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β§ π β π) β ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
29 | 28 | ralrimiva 3140 |
. . . . . 6
β’ ((π β§ βπ¦ β β* ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) β βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
30 | 29 | ad4ant14 751 |
. . . . 5
β’ ((((π β§ Β¬ π΄ β β) β§ π₯ β β+) β§
βπ¦ β
β* ((π¦
β β β§ π¦ β
π΄) β π₯ β€ (absβ(π¦ β π΄)))) β βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
31 | | climcl 15387 |
. . . . . . . 8
β’ (πΉ β π΄ β π΄ β β) |
32 | 1, 31 | syl 17 |
. . . . . . 7
β’ (π β π΄ β β) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β β) β π΄ β β) |
34 | | simpr 486 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β β) β Β¬ π΄ β
β) |
35 | | prfi 9269 |
. . . . . . 7
β’
{+β, -β} β Fin |
36 | 35 | a1i 11 |
. . . . . 6
β’ ((π β§ Β¬ π΄ β β) β {+β, -β}
β Fin) |
37 | | df-xr 11198 |
. . . . . 6
β’
β* = (β βͺ {+β,
-β}) |
38 | 33, 34, 36, 37 | cnrefiisp 44157 |
. . . . 5
β’ ((π β§ Β¬ π΄ β β) β βπ₯ β β+
βπ¦ β
β* ((π¦
β β β§ π¦ β
π΄) β π₯ β€ (absβ(π¦ β π΄)))) |
39 | 30, 38 | reximddv3 43449 |
. . . 4
β’ ((π β§ Β¬ π΄ β β) β βπ₯ β β+
βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
40 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π β§ π₯ β β+) |
41 | | nfra1 3266 |
. . . . . . . . . 10
β’
β²πβπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄))) |
42 | 40, 41 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π β§ π₯ β β+) β§
βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
43 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π β π |
44 | 42, 43 | nfan 1903 |
. . . . . . . 8
β’
β²π(((π β§ π₯ β β+) β§
βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) |
45 | | nfra1 3266 |
. . . . . . . 8
β’
β²πβπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ |
46 | 44, 45 | nfan 1903 |
. . . . . . 7
β’
β²π((((π β§ π₯ β β+) β§
βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
47 | | simpll 766 |
. . . . . . . . . . . 12
β’
(((βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄))) β§ π β π) β§ π β (β€β₯βπ)) β βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
48 | 5 | uztrn2 12787 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
49 | 48 | adantll 713 |
. . . . . . . . . . . 12
β’
(((βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄))) β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
50 | | rspa 3230 |
. . . . . . . . . . . 12
β’
((βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄))) β§ π β π) β ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
51 | 47, 49, 50 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄))) β§ π β π) β§ π β (β€β₯βπ)) β ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) |
52 | | neqne 2948 |
. . . . . . . . . . 11
β’ (Β¬
(πΉβπ) = π΄ β (πΉβπ) β π΄) |
53 | 51, 52 | impel 507 |
. . . . . . . . . 10
β’
((((βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄))) β§ π β π) β§ π β (β€β₯βπ)) β§ Β¬ (πΉβπ) = π΄) β π₯ β€ (absβ((πΉβπ) β π΄))) |
54 | 53 | ad5ant2345 1371 |
. . . . . . . . 9
β’
((((((π β§ π₯ β β+)
β§ βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) β§ π β (β€β₯βπ)) β§ Β¬ (πΉβπ) = π΄) β π₯ β€ (absβ((πΉβπ) β π΄))) |
55 | 54 | adantllr 718 |
. . . . . . . 8
β’
(((((((π β§ π₯ β β+)
β§ βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β§ Β¬ (πΉβπ) = π΄) β π₯ β€ (absβ((πΉβπ) β π΄))) |
56 | | rspa 3230 |
. . . . . . . . . . . 12
β’
((βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β§ π β (β€β₯βπ)) β (absβ((πΉβπ) β π΄)) < π₯) |
57 | 56 | adantll 713 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β (absβ((πΉβπ) β π΄)) < π₯) |
58 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β πΉ:πβΆβ) |
59 | 48 | adantll 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
60 | 58, 59 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
61 | 60 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
62 | 32 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β π΄ β β) |
63 | 61, 62 | subcld 11517 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β ((πΉβπ) β π΄) β β) |
64 | 63 | abscld 15327 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β (absβ((πΉβπ) β π΄)) β β) |
65 | 64 | adantl3r 749 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β (absβ((πΉβπ) β π΄)) β β) |
66 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
67 | 66 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β π₯ β β+) |
68 | 67 | rpred 12962 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β π₯ β β) |
69 | 65, 68 | ltnled 11307 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β ((absβ((πΉβπ) β π΄)) < π₯ β Β¬ π₯ β€ (absβ((πΉβπ) β π΄)))) |
70 | 57, 69 | mpbid 231 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β Β¬ π₯ β€ (absβ((πΉβπ) β π΄))) |
71 | 70 | adantl3r 749 |
. . . . . . . . 9
β’
((((((π β§ π₯ β β+)
β§ βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β Β¬ π₯ β€ (absβ((πΉβπ) β π΄))) |
72 | 71 | adantr 482 |
. . . . . . . 8
β’
(((((((π β§ π₯ β β+)
β§ βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β§ Β¬ (πΉβπ) = π΄) β Β¬ π₯ β€ (absβ((πΉβπ) β π΄))) |
73 | 55, 72 | condan 817 |
. . . . . . 7
β’
((((((π β§ π₯ β β+)
β§ βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β§ π β (β€β₯βπ)) β (πΉβπ) = π΄) |
74 | 46, 73 | ralrimia 3240 |
. . . . . 6
β’
(((((π β§ π₯ β β+)
β§ βπ β
π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β§ π β π) β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β βπ β (β€β₯βπ)(πΉβπ) = π΄) |
75 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππΉ |
76 | 75, 3, 5, 11 | climuz 44071 |
. . . . . . . . . 10
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) |
77 | 1, 76 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
78 | 77 | simprd 497 |
. . . . . . . 8
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
79 | 78 | r19.21bi 3233 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
80 | 79 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§
βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
81 | 74, 80 | reximddv3 43449 |
. . . . 5
β’ (((π β§ π₯ β β+) β§
βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β βπ β π βπ β (β€β₯βπ)(πΉβπ) = π΄) |
82 | 81 | adantllr 718 |
. . . 4
β’ ((((π β§ Β¬ π΄ β β) β§ π₯ β β+) β§
βπ β π ((πΉβπ) β π΄ β π₯ β€ (absβ((πΉβπ) β π΄)))) β βπ β π βπ β (β€β₯βπ)(πΉβπ) = π΄) |
83 | 39, 82 | rexlimddv2 44150 |
. . 3
β’ ((π β§ Β¬ π΄ β β) β βπ β π βπ β (β€β₯βπ)(πΉβπ) = π΄) |
84 | | nfv 1918 |
. . . . 5
β’
β²π((π β§ Β¬ π΄ β β) β§ π β π) |
85 | | nfra1 3266 |
. . . . 5
β’
β²πβπ β (β€β₯βπ)(πΉβπ) = π΄ |
86 | 84, 85 | nfan 1903 |
. . . 4
β’
β²π(((π β§ Β¬ π΄ β β) β§ π β π) β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) |
87 | 6 | ad3antrrr 729 |
. . . 4
β’ ((((π β§ Β¬ π΄ β β) β§ π β π) β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β πΉ:πβΆβ*) |
88 | | simplr 768 |
. . . 4
β’ ((((π β§ Β¬ π΄ β β) β§ π β π) β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β π β π) |
89 | 5 | uzid3 43756 |
. . . . . . . 8
β’ (π β π β π β (β€β₯βπ)) |
90 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
91 | 90 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) = π΄ β (πΉβπ) = π΄)) |
92 | 91 | rspcva 3578 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β (πΉβπ) = π΄) |
93 | 89, 92 | sylan 581 |
. . . . . . 7
β’ ((π β π β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β (πΉβπ) = π΄) |
94 | 93 | 3adant1 1131 |
. . . . . 6
β’ ((π β§ π β π β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β (πΉβπ) = π΄) |
95 | 6 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
96 | 95 | 3adant3 1133 |
. . . . . 6
β’ ((π β§ π β π β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β (πΉβπ) β
β*) |
97 | 94, 96 | eqeltrrd 2835 |
. . . . 5
β’ ((π β§ π β π β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β π΄ β
β*) |
98 | 97 | ad4ant134 1175 |
. . . 4
β’ ((((π β§ Β¬ π΄ β β) β§ π β π) β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β π΄ β
β*) |
99 | | rspa 3230 |
. . . . 5
β’
((βπ β
(β€β₯βπ)(πΉβπ) = π΄ β§ π β (β€β₯βπ)) β (πΉβπ) = π΄) |
100 | 99 | adantll 713 |
. . . 4
β’
(((((π β§ Β¬
π΄ β β) β§
π β π) β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β§ π β (β€β₯βπ)) β (πΉβπ) = π΄) |
101 | 86, 75, 5, 87, 88, 98, 100 | xlimconst2 44162 |
. . 3
β’ ((((π β§ Β¬ π΄ β β) β§ π β π) β§ βπ β (β€β₯βπ)(πΉβπ) = π΄) β πΉ~~>*π΄) |
102 | 83, 101 | rexlimddv2 44150 |
. 2
β’ ((π β§ Β¬ π΄ β β) β πΉ~~>*π΄) |
103 | 10, 102 | pm2.61dan 812 |
1
β’ (π β πΉ~~>*π΄) |