Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . 4
β’
β²π(π β§ π β π) |
2 | | nfra1 3266 |
. . . 4
β’
β²πβπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π) |
3 | 1, 2 | nfan 1903 |
. . 3
β’
β²π((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) |
4 | | simplll 774 |
. . . 4
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) β§ π β (β€β₯βπ)) β π) |
5 | | climisp.z |
. . . . . 6
β’ π =
(β€β₯βπ) |
6 | 5 | uztrn2 12790 |
. . . . 5
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
7 | 6 | ad4ant24 753 |
. . . 4
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) β§ π β (β€β₯βπ)) β π β π) |
8 | | rspa 3230 |
. . . . . 6
β’
((βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π) β§ π β (β€β₯βπ)) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) |
9 | 8 | simprd 497 |
. . . . 5
β’
((βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π) β§ π β (β€β₯βπ)) β (absβ((πΉβπ) β π΄)) < π) |
10 | 9 | adantll 713 |
. . . 4
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) β§ π β (β€β₯βπ)) β (absβ((πΉβπ) β π΄)) < π) |
11 | | simpl3 1194 |
. . . . 5
β’ (((π β§ π β π β§ (absβ((πΉβπ) β π΄)) < π) β§ Β¬ (πΉβπ) = π΄) β (absβ((πΉβπ) β π΄)) < π) |
12 | | neqne 2948 |
. . . . . . 7
β’ (Β¬
(πΉβπ) = π΄ β (πΉβπ) β π΄) |
13 | | climisp.x |
. . . . . . . . . 10
β’ (π β π β
β+) |
14 | 13 | rpred 12965 |
. . . . . . . . 9
β’ (π β π β β) |
15 | 14 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (πΉβπ) β π΄) β π β β) |
16 | | climisp.f |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ) |
17 | 16 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) β β) |
18 | | climisp.c |
. . . . . . . . . . . . . 14
β’ (π β πΉ β π΄) |
19 | 5 | fvexi 6860 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β π β V) |
21 | 16, 20 | fexd 7181 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ β V) |
22 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β€) β (πΉβπ) = (πΉβπ)) |
23 | 21, 22 | clim 15385 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)))) |
24 | 18, 23 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
25 | 24 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
26 | 25 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π΄ β β) |
27 | 17, 26 | subcld 11520 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((πΉβπ) β π΄) β β) |
28 | 27 | abscld 15330 |
. . . . . . . . 9
β’ ((π β§ π β π) β (absβ((πΉβπ) β π΄)) β β) |
29 | 28 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (πΉβπ) β π΄) β (absβ((πΉβπ) β π΄)) β β) |
30 | | climisp.l |
. . . . . . . . 9
β’ ((π β§ π β π β§ (πΉβπ) β π΄) β π β€ (absβ((πΉβπ) β π΄))) |
31 | 30 | 3expa 1119 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (πΉβπ) β π΄) β π β€ (absβ((πΉβπ) β π΄))) |
32 | 15, 29, 31 | lensymd 11314 |
. . . . . . 7
β’ (((π β§ π β π) β§ (πΉβπ) β π΄) β Β¬ (absβ((πΉβπ) β π΄)) < π) |
33 | 12, 32 | sylan2 594 |
. . . . . 6
β’ (((π β§ π β π) β§ Β¬ (πΉβπ) = π΄) β Β¬ (absβ((πΉβπ) β π΄)) < π) |
34 | 33 | 3adantl3 1169 |
. . . . 5
β’ (((π β§ π β π β§ (absβ((πΉβπ) β π΄)) < π) β§ Β¬ (πΉβπ) = π΄) β Β¬ (absβ((πΉβπ) β π΄)) < π) |
35 | 11, 34 | condan 817 |
. . . 4
β’ ((π β§ π β π β§ (absβ((πΉβπ) β π΄)) < π) β (πΉβπ) = π΄) |
36 | 4, 7, 10, 35 | syl3anc 1372 |
. . 3
β’ ((((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) β§ π β (β€β₯βπ)) β (πΉβπ) = π΄) |
37 | 3, 36 | ralrimia 3240 |
. 2
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) β βπ β (β€β₯βπ)(πΉβπ) = π΄) |
38 | | breq2 5113 |
. . . . . 6
β’ (π₯ = π β ((absβ((πΉβπ) β π΄)) < π₯ β (absβ((πΉβπ) β π΄)) < π)) |
39 | 38 | anbi2d 630 |
. . . . 5
β’ (π₯ = π β (((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π))) |
40 | 39 | rexralbidv 3211 |
. . . 4
β’ (π₯ = π β (βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π))) |
41 | 24 | simprd 497 |
. . . 4
β’ (π β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
42 | 40, 41, 13 | rspcdva 3584 |
. . 3
β’ (π β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) |
43 | | climisp.m |
. . . 4
β’ (π β π β β€) |
44 | 5 | rexuz3 15242 |
. . . 4
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π))) |
45 | 43, 44 | syl 17 |
. . 3
β’ (π β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π))) |
46 | 42, 45 | mpbird 257 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π)) |
47 | 37, 46 | reximddv3 43453 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) = π΄) |