Step | Hyp | Ref
| Expression |
1 | | climxrre.m |
. . . . 5
β’ (π β π β β€) |
2 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ +β β β)
β§ -β β β) β π β β€) |
3 | | climxrre.z |
. . . 4
β’ π =
(β€β₯βπ) |
4 | | climxrre.f |
. . . . 5
β’ (π β πΉ:πβΆβ*) |
5 | 4 | ad2antrr 725 |
. . . 4
β’ (((π β§ +β β β)
β§ -β β β) β πΉ:πβΆβ*) |
6 | | climxrre.c |
. . . . 5
β’ (π β πΉ β π΄) |
7 | 6 | ad2antrr 725 |
. . . 4
β’ (((π β§ +β β β)
β§ -β β β) β πΉ β π΄) |
8 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ +β β β)
β +β β β) |
9 | | climxrre.a |
. . . . . . . . . 10
β’ (π β π΄ β β) |
10 | 9 | recnd 11190 |
. . . . . . . . 9
β’ (π β π΄ β β) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ +β β β)
β π΄ β
β) |
12 | 8, 11 | subcld 11519 |
. . . . . . 7
β’ ((π β§ +β β β)
β (+β β π΄)
β β) |
13 | | renepnf 11210 |
. . . . . . . . . . 11
β’ (π΄ β β β π΄ β +β) |
14 | 13 | necomd 3000 |
. . . . . . . . . 10
β’ (π΄ β β β +β
β π΄) |
15 | 9, 14 | syl 17 |
. . . . . . . . 9
β’ (π β +β β π΄) |
16 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π β§ +β β β)
β +β β π΄) |
17 | 8, 11, 16 | subne0d 11528 |
. . . . . . 7
β’ ((π β§ +β β β)
β (+β β π΄)
β 0) |
18 | 12, 17 | absrpcld 15340 |
. . . . . 6
β’ ((π β§ +β β β)
β (absβ(+β β π΄)) β
β+) |
19 | 18 | adantr 482 |
. . . . 5
β’ (((π β§ +β β β)
β§ -β β β) β (absβ(+β β π΄)) β
β+) |
20 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ -β β β)
β -β β β) |
21 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ -β β β)
β π΄ β
β) |
22 | 20, 21 | subcld 11519 |
. . . . . . 7
β’ ((π β§ -β β β)
β (-β β π΄)
β β) |
23 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ -β β β)
β π΄ β
β) |
24 | | renemnf 11211 |
. . . . . . . . . 10
β’ (π΄ β β β π΄ β -β) |
25 | 24 | necomd 3000 |
. . . . . . . . 9
β’ (π΄ β β β -β
β π΄) |
26 | 23, 25 | syl 17 |
. . . . . . . 8
β’ ((π β§ -β β β)
β -β β π΄) |
27 | 20, 21, 26 | subne0d 11528 |
. . . . . . 7
β’ ((π β§ -β β β)
β (-β β π΄)
β 0) |
28 | 22, 27 | absrpcld 15340 |
. . . . . 6
β’ ((π β§ -β β β)
β (absβ(-β β π΄)) β
β+) |
29 | 28 | adantlr 714 |
. . . . 5
β’ (((π β§ +β β β)
β§ -β β β) β (absβ(-β β π΄)) β
β+) |
30 | 19, 29 | ifcld 4537 |
. . . 4
β’ (((π β§ +β β β)
β§ -β β β) β if((absβ(+β β π΄)) β€ (absβ(-β
β π΄)),
(absβ(+β β π΄)), (absβ(-β β π΄))) β
β+) |
31 | 19 | rpred 12964 |
. . . . . 6
β’ (((π β§ +β β β)
β§ -β β β) β (absβ(+β β π΄)) β
β) |
32 | 29 | rpred 12964 |
. . . . . 6
β’ (((π β§ +β β β)
β§ -β β β) β (absβ(-β β π΄)) β
β) |
33 | 31, 32 | min1d 43781 |
. . . . 5
β’ (((π β§ +β β β)
β§ -β β β) β if((absβ(+β β π΄)) β€ (absβ(-β
β π΄)),
(absβ(+β β π΄)), (absβ(-β β π΄))) β€ (absβ(+β
β π΄))) |
34 | 33 | adantr 482 |
. . . 4
β’ ((((π β§ +β β β)
β§ -β β β) β§ +β β β) β
if((absβ(+β β π΄)) β€ (absβ(-β β π΄)), (absβ(+β β
π΄)), (absβ(-β
β π΄))) β€
(absβ(+β β π΄))) |
35 | 31, 32 | min2d 43782 |
. . . . 5
β’ (((π β§ +β β β)
β§ -β β β) β if((absβ(+β β π΄)) β€ (absβ(-β
β π΄)),
(absβ(+β β π΄)), (absβ(-β β π΄))) β€ (absβ(-β
β π΄))) |
36 | 35 | adantr 482 |
. . . 4
β’ ((((π β§ +β β β)
β§ -β β β) β§ -β β β) β
if((absβ(+β β π΄)) β€ (absβ(-β β π΄)), (absβ(+β β
π΄)), (absβ(-β
β π΄))) β€
(absβ(-β β π΄))) |
37 | 2, 3, 5, 7, 30, 34, 36 | climxrrelem 44064 |
. . 3
β’ (((π β§ +β β β)
β§ -β β β) β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
38 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ +β β β)
β§ Β¬ -β β β) β π β β€) |
39 | 4 | ad2antrr 725 |
. . . 4
β’ (((π β§ +β β β)
β§ Β¬ -β β β) β πΉ:πβΆβ*) |
40 | 6 | ad2antrr 725 |
. . . 4
β’ (((π β§ +β β β)
β§ Β¬ -β β β) β πΉ β π΄) |
41 | 18 | adantr 482 |
. . . 4
β’ (((π β§ +β β β)
β§ Β¬ -β β β) β (absβ(+β β π΄)) β
β+) |
42 | 18 | rpred 12964 |
. . . . . 6
β’ ((π β§ +β β β)
β (absβ(+β β π΄)) β β) |
43 | 42 | leidd 11728 |
. . . . 5
β’ ((π β§ +β β β)
β (absβ(+β β π΄)) β€ (absβ(+β β π΄))) |
44 | 43 | ad2antrr 725 |
. . . 4
β’ ((((π β§ +β β β)
β§ Β¬ -β β β) β§ +β β β) β
(absβ(+β β π΄)) β€ (absβ(+β β π΄))) |
45 | | pm2.21 123 |
. . . . . 6
β’ (Β¬
-β β β β (-β β β β
(absβ(+β β π΄)) β€ (absβ(-β β π΄)))) |
46 | 45 | imp 408 |
. . . . 5
β’ ((Β¬
-β β β β§ -β β β) β
(absβ(+β β π΄)) β€ (absβ(-β β π΄))) |
47 | 46 | adantll 713 |
. . . 4
β’ ((((π β§ +β β β)
β§ Β¬ -β β β) β§ -β β β) β
(absβ(+β β π΄)) β€ (absβ(-β β π΄))) |
48 | 38, 3, 39, 40, 41, 44, 47 | climxrrelem 44064 |
. . 3
β’ (((π β§ +β β β)
β§ Β¬ -β β β) β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
49 | 37, 48 | pm2.61dan 812 |
. 2
β’ ((π β§ +β β β)
β βπ β
π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
50 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ Β¬ +β β
β) β§ -β β β) β π β β€) |
51 | 4 | ad2antrr 725 |
. . . 4
β’ (((π β§ Β¬ +β β
β) β§ -β β β) β πΉ:πβΆβ*) |
52 | 6 | ad2antrr 725 |
. . . 4
β’ (((π β§ Β¬ +β β
β) β§ -β β β) β πΉ β π΄) |
53 | 28 | adantlr 714 |
. . . 4
β’ (((π β§ Β¬ +β β
β) β§ -β β β) β (absβ(-β β
π΄)) β
β+) |
54 | | pm2.21 123 |
. . . . . 6
β’ (Β¬
+β β β β (+β β β β
(absβ(-β β π΄)) β€ (absβ(+β β π΄)))) |
55 | 54 | imp 408 |
. . . . 5
β’ ((Β¬
+β β β β§ +β β β) β
(absβ(-β β π΄)) β€ (absβ(+β β π΄))) |
56 | 55 | ad4ant24 753 |
. . . 4
β’ ((((π β§ Β¬ +β β
β) β§ -β β β) β§ +β β β) β
(absβ(-β β π΄)) β€ (absβ(+β β π΄))) |
57 | 28 | rpred 12964 |
. . . . . 6
β’ ((π β§ -β β β)
β (absβ(-β β π΄)) β β) |
58 | 57 | leidd 11728 |
. . . . 5
β’ ((π β§ -β β β)
β (absβ(-β β π΄)) β€ (absβ(-β β π΄))) |
59 | 58 | ad4ant13 750 |
. . . 4
β’ ((((π β§ Β¬ +β β
β) β§ -β β β) β§ -β β β) β
(absβ(-β β π΄)) β€ (absβ(-β β π΄))) |
60 | 50, 3, 51, 52, 53, 56, 59 | climxrrelem 44064 |
. . 3
β’ (((π β§ Β¬ +β β
β) β§ -β β β) β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
61 | | nfv 1918 |
. . . . . . 7
β’
β²π((π β§ Β¬ +β β
β) β§ Β¬ -β β β) |
62 | | nfv 1918 |
. . . . . . . 8
β’
β²π π β π |
63 | | nfra1 3270 |
. . . . . . . 8
β’
β²πβπ β (β€β₯βπ)(πΉβπ) β β |
64 | 62, 63 | nfan 1903 |
. . . . . . 7
β’
β²π(π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β) |
65 | 61, 64 | nfan 1903 |
. . . . . 6
β’
β²π(((π β§ Β¬ +β β
β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) |
66 | | simp-4l 782 |
. . . . . . . 8
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β π) |
67 | 3 | uztrn2 12789 |
. . . . . . . . . 10
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
68 | 67 | adantlr 714 |
. . . . . . . . 9
β’ (((π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β) β§ π β (β€β₯βπ)) β π β π) |
69 | 68 | adantll 713 |
. . . . . . . 8
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β π β π) |
70 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β π) |
71 | 4 | fdmd 6684 |
. . . . . . . . . 10
β’ (π β dom πΉ = π) |
72 | 71 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β dom πΉ = π) |
73 | 70, 72 | eleqtrrd 2841 |
. . . . . . . 8
β’ ((π β§ π β π) β π β dom πΉ) |
74 | 66, 69, 73 | syl2anc 585 |
. . . . . . 7
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β π β dom πΉ) |
75 | 4 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
76 | 66, 69, 75 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β (πΉβπ) β
β*) |
77 | | rspa 3234 |
. . . . . . . . . . 11
β’
((βπ β
(β€β₯βπ)(πΉβπ) β β β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
78 | 77 | adantll 713 |
. . . . . . . . . 10
β’ (((π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
79 | 78 | adantll 713 |
. . . . . . . . 9
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
80 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β Β¬ -β β
β) |
81 | | nelne2 3043 |
. . . . . . . . 9
β’ (((πΉβπ) β β β§ Β¬ -β β
β) β (πΉβπ) β -β) |
82 | 79, 80, 81 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β (πΉβπ) β -β) |
83 | | simp-4r 783 |
. . . . . . . . 9
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β Β¬ +β β
β) |
84 | | nelne2 3043 |
. . . . . . . . 9
β’ (((πΉβπ) β β β§ Β¬ +β β
β) β (πΉβπ) β +β) |
85 | 79, 83, 84 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β (πΉβπ) β +β) |
86 | 76, 82, 85 | xrred 43673 |
. . . . . . 7
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
87 | 74, 86 | jca 513 |
. . . . . 6
β’
(((((π β§ Β¬
+β β β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β (π β dom πΉ β§ (πΉβπ) β β)) |
88 | 65, 87 | ralrimia 3244 |
. . . . 5
β’ ((((π β§ Β¬ +β β
β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β)) |
89 | 4 | ffund 6677 |
. . . . . . 7
β’ (π β Fun πΉ) |
90 | | ffvresb 7077 |
. . . . . . 7
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
91 | 89, 90 | syl 17 |
. . . . . 6
β’ (π β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
92 | 91 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ Β¬ +β β
β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β ((πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ β
βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β))) |
93 | 88, 92 | mpbird 257 |
. . . 4
β’ ((((π β§ Β¬ +β β
β) β§ Β¬ -β β β) β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
94 | | r19.26 3115 |
. . . . . . . . 9
β’
(βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < 1) β (βπ β
(β€β₯βπ)(πΉβπ) β β β§ βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < 1)) |
95 | 94 | simplbi 499 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < 1) β βπ β (β€β₯βπ)(πΉβπ) β β) |
96 | 95 | ad2antll 728 |
. . . . . . 7
β’ ((π β§ (π β β€ β§ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < 1))) β βπ β
(β€β₯βπ)(πΉβπ) β β) |
97 | | breq2 5114 |
. . . . . . . . . 10
β’ (π₯ = 1 β ((absβ((πΉβπ) β π΄)) < π₯ β (absβ((πΉβπ) β π΄)) < 1)) |
98 | 97 | anbi2d 630 |
. . . . . . . . 9
β’ (π₯ = 1 β (((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < 1))) |
99 | 98 | rexralbidv 3215 |
. . . . . . . 8
β’ (π₯ = 1 β (βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < 1))) |
100 | 3 | fvexi 6861 |
. . . . . . . . . . . . 13
β’ π β V |
101 | 100 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π β V) |
102 | 4, 101 | fexd 7182 |
. . . . . . . . . . 11
β’ (π β πΉ β V) |
103 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β (πΉβπ) = (πΉβπ)) |
104 | 102, 103 | clim 15383 |
. . . . . . . . . 10
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)))) |
105 | 6, 104 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
106 | 105 | simprd 497 |
. . . . . . . 8
β’ (π β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
107 | | 1rp 12926 |
. . . . . . . . 9
β’ 1 β
β+ |
108 | 107 | a1i 11 |
. . . . . . . 8
β’ (π β 1 β
β+) |
109 | 99, 106, 108 | rspcdva 3585 |
. . . . . . 7
β’ (π β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < 1)) |
110 | 96, 109 | reximddv 3169 |
. . . . . 6
β’ (π β βπ β β€ βπ β (β€β₯βπ)(πΉβπ) β β) |
111 | 3 | rexuz3 15240 |
. . . . . . 7
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)(πΉβπ) β β β βπ β β€ βπ β
(β€β₯βπ)(πΉβπ) β β)) |
112 | 1, 111 | syl 17 |
. . . . . 6
β’ (π β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β β β βπ β β€ βπ β
(β€β₯βπ)(πΉβπ) β β)) |
113 | 110, 112 | mpbird 257 |
. . . . 5
β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β β) |
114 | 113 | ad2antrr 725 |
. . . 4
β’ (((π β§ Β¬ +β β
β) β§ Β¬ -β β β) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β β) |
115 | 93, 114 | reximddv 3169 |
. . 3
β’ (((π β§ Β¬ +β β
β) β§ Β¬ -β β β) β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
116 | 60, 115 | pm2.61dan 812 |
. 2
β’ ((π β§ Β¬ +β β
β) β βπ
β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
117 | 49, 116 | pm2.61dan 812 |
1
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |