Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²ππ |
2 | | nfv 1918 |
. . . . . 6
β’
β²π π β π |
3 | | nfra1 3266 |
. . . . . 6
β’
β²πβπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·) |
4 | 2, 3 | nfan 1903 |
. . . . 5
β’
β²π(π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) |
5 | 1, 4 | nfan 1903 |
. . . 4
β’
β²π(π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) |
6 | | climxrrelem.z |
. . . . . . . . 9
β’ π =
(β€β₯βπ) |
7 | 6 | uztrn2 12790 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
8 | 7 | adantll 713 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
9 | | climxrrelem.f |
. . . . . . . . 9
β’ (π β πΉ:πβΆβ*) |
10 | 9 | fdmd 6683 |
. . . . . . . 8
β’ (π β dom πΉ = π) |
11 | 10 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β dom πΉ = π) |
12 | 8, 11 | eleqtrrd 2837 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β dom πΉ) |
13 | 12 | adantlrr 720 |
. . . . 5
β’ (((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β§ π β (β€β₯βπ)) β π β dom πΉ) |
14 | | simpll 766 |
. . . . . 6
β’ (((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β§ π β (β€β₯βπ)) β π) |
15 | 8 | adantlrr 720 |
. . . . . 6
β’ (((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β§ π β (β€β₯βπ)) β π β π) |
16 | | rspa 3230 |
. . . . . . . 8
β’
((βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·) β§ π β (β€β₯βπ)) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) |
17 | 16 | adantll 713 |
. . . . . . 7
β’ (((π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ π β (β€β₯βπ)) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) |
18 | 17 | adantll 713 |
. . . . . 6
β’ (((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β§ π β (β€β₯βπ)) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) |
19 | 9 | ffvelcdmda 7039 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
20 | 19 | 3adant3 1133 |
. . . . . . 7
β’ ((π β§ π β π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β (πΉβπ) β
β*) |
21 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = -β) β π) |
22 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β β§ (πΉβπ) = -β) β (πΉβπ) = -β) |
23 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β β§ (πΉβπ) = -β) β (πΉβπ) β β) |
24 | 22, 23 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ (((πΉβπ) β β β§ (πΉβπ) = -β) β -β β
β) |
25 | 24 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = -β) β -β β
β) |
26 | | climxrrelem.n |
. . . . . . . . . . . 12
β’ ((π β§ -β β β)
β π· β€
(absβ(-β β π΄))) |
27 | 21, 25, 26 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = -β) β π· β€ (absβ(-β β π΄))) |
28 | 27 | adantlrr 720 |
. . . . . . . . . 10
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = -β) β π· β€ (absβ(-β β π΄))) |
29 | | fvoveq1 7384 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) = -β β (absβ((πΉβπ) β π΄)) = (absβ(-β β π΄))) |
30 | 29 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((absβ((πΉβπ) β π΄)) < π· β§ (πΉβπ) = -β) β (absβ((πΉβπ) β π΄)) = (absβ(-β β π΄))) |
31 | | simpl 484 |
. . . . . . . . . . . . . 14
β’
(((absβ((πΉβπ) β π΄)) < π· β§ (πΉβπ) = -β) β (absβ((πΉβπ) β π΄)) < π·) |
32 | 30, 31 | eqbrtrrd 5133 |
. . . . . . . . . . . . 13
β’
(((absβ((πΉβπ) β π΄)) < π· β§ (πΉβπ) = -β) β (absβ(-β
β π΄)) < π·) |
33 | 32 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ (absβ((πΉβπ) β π΄)) < π·) β§ (πΉβπ) = -β) β (absβ(-β
β π΄)) < π·) |
34 | 33 | adantlrl 719 |
. . . . . . . . . . 11
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = -β) β (absβ(-β
β π΄)) < π·) |
35 | | climxrrelem.c |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ β π΄) |
36 | 6 | fvexi 6860 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β V |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β V) |
38 | 9, 37 | fexd 7181 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ β V) |
39 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β€) β (πΉβπ) = (πΉβπ)) |
40 | 38, 39 | clim 15385 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)))) |
41 | 35, 40 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
42 | 41 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β β) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = -β) β π΄ β β) |
44 | 25, 43 | subcld 11520 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = -β) β (-β β π΄) β
β) |
45 | 44 | abscld 15330 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = -β) β (absβ(-β
β π΄)) β
β) |
46 | 45 | adantlrr 720 |
. . . . . . . . . . . 12
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = -β) β (absβ(-β
β π΄)) β
β) |
47 | | climxrrelem.d |
. . . . . . . . . . . . . 14
β’ (π β π· β
β+) |
48 | 47 | rpred 12965 |
. . . . . . . . . . . . 13
β’ (π β π· β β) |
49 | 48 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = -β) β π· β β) |
50 | 46, 49 | ltnled 11310 |
. . . . . . . . . . 11
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = -β) β ((absβ(-β
β π΄)) < π· β Β¬ π· β€ (absβ(-β β π΄)))) |
51 | 34, 50 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = -β) β Β¬ π· β€ (absβ(-β β π΄))) |
52 | 28, 51 | pm2.65da 816 |
. . . . . . . . 9
β’ ((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β Β¬ (πΉβπ) = -β) |
53 | 52 | 3adant2 1132 |
. . . . . . . 8
β’ ((π β§ π β π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β Β¬ (πΉβπ) = -β) |
54 | 53 | neqned 2947 |
. . . . . . 7
β’ ((π β§ π β π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β (πΉβπ) β -β) |
55 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = +β) β π) |
56 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β β§ (πΉβπ) = +β) β (πΉβπ) = +β) |
57 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β β§ (πΉβπ) = +β) β (πΉβπ) β β) |
58 | 56, 57 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ (((πΉβπ) β β β§ (πΉβπ) = +β) β +β β
β) |
59 | 58 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = +β) β +β β
β) |
60 | | climxrrelem.p |
. . . . . . . . . . . 12
β’ ((π β§ +β β β)
β π· β€
(absβ(+β β π΄))) |
61 | 55, 59, 60 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = +β) β π· β€ (absβ(+β β π΄))) |
62 | 61 | adantlrr 720 |
. . . . . . . . . 10
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = +β) β π· β€ (absβ(+β β π΄))) |
63 | | fvoveq1 7384 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) = +β β (absβ((πΉβπ) β π΄)) = (absβ(+β β π΄))) |
64 | 63 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((absβ((πΉβπ) β π΄)) < π· β§ (πΉβπ) = +β) β (absβ((πΉβπ) β π΄)) = (absβ(+β β π΄))) |
65 | | simpl 484 |
. . . . . . . . . . . . . 14
β’
(((absβ((πΉβπ) β π΄)) < π· β§ (πΉβπ) = +β) β (absβ((πΉβπ) β π΄)) < π·) |
66 | 64, 65 | eqbrtrrd 5133 |
. . . . . . . . . . . . 13
β’
(((absβ((πΉβπ) β π΄)) < π· β§ (πΉβπ) = +β) β (absβ(+β
β π΄)) < π·) |
67 | 66 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ (absβ((πΉβπ) β π΄)) < π·) β§ (πΉβπ) = +β) β (absβ(+β
β π΄)) < π·) |
68 | 67 | adantlrl 719 |
. . . . . . . . . . 11
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = +β) β (absβ(+β
β π΄)) < π·) |
69 | 42 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = +β) β π΄ β β) |
70 | 59, 69 | subcld 11520 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = +β) β (+β β π΄) β
β) |
71 | 70 | abscld 15330 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΉβπ) β β) β§ (πΉβπ) = +β) β (absβ(+β
β π΄)) β
β) |
72 | 71 | adantlrr 720 |
. . . . . . . . . . . 12
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = +β) β (absβ(+β
β π΄)) β
β) |
73 | 48 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = +β) β π· β β) |
74 | 72, 73 | ltnled 11310 |
. . . . . . . . . . 11
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = +β) β ((absβ(+β
β π΄)) < π· β Β¬ π· β€ (absβ(+β β π΄)))) |
75 | 68, 74 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β§ (πΉβπ) = +β) β Β¬ π· β€ (absβ(+β β π΄))) |
76 | 62, 75 | pm2.65da 816 |
. . . . . . . . 9
β’ ((π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β Β¬ (πΉβπ) = +β) |
77 | 76 | 3adant2 1132 |
. . . . . . . 8
β’ ((π β§ π β π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β Β¬ (πΉβπ) = +β) |
78 | 77 | neqned 2947 |
. . . . . . 7
β’ ((π β§ π β π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β (πΉβπ) β +β) |
79 | 20, 54, 78 | xrred 43690 |
. . . . . 6
β’ ((π β§ π β π β§ ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) β (πΉβπ) β β) |
80 | 14, 15, 18, 79 | syl3anc 1372 |
. . . . 5
β’ (((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
81 | 13, 80 | jca 513 |
. . . 4
β’ (((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β§ π β (β€β₯βπ)) β (π β dom πΉ β§ (πΉβπ) β β)) |
82 | 5, 81 | ralrimia 3240 |
. . 3
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β)) |
83 | 9 | ffund 6676 |
. . . . 5
β’ (π β Fun πΉ) |
84 | | ffvresb 7076 |
. . . . 5
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
85 | 83, 84 | syl 17 |
. . . 4
β’ (π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
86 | 85 | adantr 482 |
. . 3
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
87 | 82, 86 | mpbird 257 |
. 2
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
88 | | breq2 5113 |
. . . . . 6
β’ (π₯ = π· β ((absβ((πΉβπ) β π΄)) < π₯ β (absβ((πΉβπ) β π΄)) < π·)) |
89 | 88 | anbi2d 630 |
. . . . 5
β’ (π₯ = π· β (((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) |
90 | 89 | rexralbidv 3211 |
. . . 4
β’ (π₯ = π· β (βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) |
91 | 41 | simprd 497 |
. . . 4
β’ (π β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
92 | 90, 91, 47 | rspcdva 3584 |
. . 3
β’ (π β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) |
93 | | climxrrelem.m |
. . . 4
β’ (π β π β β€) |
94 | 6 | rexuz3 15242 |
. . . 4
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) |
95 | 93, 94 | syl 17 |
. . 3
β’ (π β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·))) |
96 | 92, 95 | mpbird 257 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π·)) |
97 | 87, 96 | reximddv 3165 |
1
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |