Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . 3
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) |
2 | | cnplimclemr.f |
. . . . . . . 8
β’ (π β πΉ:π΄βΆβ) |
3 | | cnplimclemle.z |
. . . . . . . 8
β’ (π β π β π΄) |
4 | 2, 3 | ffvelcdmd 5653 |
. . . . . . 7
β’ (π β (πΉβπ) β β) |
5 | | cnplimclemr.b |
. . . . . . . 8
β’ (π β π΅ β π΄) |
6 | 2, 5 | ffvelcdmd 5653 |
. . . . . . 7
β’ (π β (πΉβπ΅) β β) |
7 | 4, 6 | subcld 8268 |
. . . . . 6
β’ (π β ((πΉβπ) β (πΉβπ΅)) β β) |
8 | 7 | abscld 11190 |
. . . . 5
β’ (π β (absβ((πΉβπ) β (πΉβπ΅))) β β) |
9 | 8 | adantr 276 |
. . . 4
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (absβ((πΉβπ) β (πΉβπ΅))) β β) |
10 | | cnplimclemle.e |
. . . . . . 7
β’ (π β πΈ β
β+) |
11 | 10 | rphalfcld 9709 |
. . . . . 6
β’ (π β (πΈ / 2) β
β+) |
12 | 11 | rpred 9696 |
. . . . 5
β’ (π β (πΈ / 2) β β) |
13 | 12 | adantr 276 |
. . . 4
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (πΈ / 2) β β) |
14 | 4 | adantr 276 |
. . . . . . 7
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (πΉβπ) β β) |
15 | 1 | adantr 276 |
. . . . . . . . . 10
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) |
16 | | simpll 527 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β π) |
17 | 16, 8 | syl 14 |
. . . . . . . . . . 11
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β (absβ((πΉβπ) β (πΉβπ΅))) β β) |
18 | 16, 12 | syl 14 |
. . . . . . . . . . 11
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β (πΈ / 2) β β) |
19 | | simpr 110 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β π # π΅) |
20 | | cnplimclemle.zd |
. . . . . . . . . . . . 13
β’ (π β (absβ(π β π΅)) < π·) |
21 | 16, 20 | syl 14 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β (absβ(π β π΅)) < π·) |
22 | | cnplimclemle.im |
. . . . . . . . . . . 12
β’ ((π β§ π # π΅ β§ (absβ(π β π΅)) < π·) β (absβ((πΉβπ) β (πΉβπ΅))) < (πΈ / 2)) |
23 | 16, 19, 21, 22 | syl3anc 1238 |
. . . . . . . . . . 11
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β (absβ((πΉβπ) β (πΉβπ΅))) < (πΈ / 2)) |
24 | 17, 18, 23 | ltnsymd 8077 |
. . . . . . . . . 10
β’ (((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β§ π # π΅) β Β¬ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) |
25 | 15, 24 | pm2.65da 661 |
. . . . . . . . 9
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β Β¬ π # π΅) |
26 | | cnplimclemr.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
27 | 26, 3 | sseldd 3157 |
. . . . . . . . . 10
β’ (π β π β β) |
28 | 26, 5 | sseldd 3157 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
29 | 28 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β π΅ β β) |
30 | | apti 8579 |
. . . . . . . . . 10
β’ ((π β β β§ π΅ β β) β (π = π΅ β Β¬ π # π΅)) |
31 | 27, 29, 30 | syl2an2r 595 |
. . . . . . . . 9
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (π = π΅ β Β¬ π # π΅)) |
32 | 25, 31 | mpbird 167 |
. . . . . . . 8
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β π = π΅) |
33 | 32 | fveq2d 5520 |
. . . . . . 7
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (πΉβπ) = (πΉβπ΅)) |
34 | 14, 33 | subeq0bd 8336 |
. . . . . 6
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β ((πΉβπ) β (πΉβπ΅)) = 0) |
35 | 34 | abs00bd 11075 |
. . . . 5
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (absβ((πΉβπ) β (πΉβπ΅))) = 0) |
36 | 11 | adantr 276 |
. . . . . 6
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (πΈ / 2) β
β+) |
37 | 36 | rpgt0d 9699 |
. . . . 5
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β 0 < (πΈ / 2)) |
38 | 35, 37 | eqbrtrd 4026 |
. . . 4
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (absβ((πΉβπ) β (πΉβπ΅))) < (πΈ / 2)) |
39 | 9, 13, 38 | ltnsymd 8077 |
. . 3
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β Β¬ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) |
40 | 1, 39 | pm2.21dd 620 |
. 2
β’ ((π β§ (πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅)))) β (absβ((πΉβπ) β (πΉβπ΅))) < πΈ) |
41 | | simpr 110 |
. 2
β’ ((π β§ (absβ((πΉβπ) β (πΉβπ΅))) < πΈ) β (absβ((πΉβπ) β (πΉβπ΅))) < πΈ) |
42 | | rphalflt 9683 |
. . . 4
β’ (πΈ β β+
β (πΈ / 2) < πΈ) |
43 | 10, 42 | syl 14 |
. . 3
β’ (π β (πΈ / 2) < πΈ) |
44 | 10 | rpred 9696 |
. . . 4
β’ (π β πΈ β β) |
45 | | axltwlin 8025 |
. . . 4
β’ (((πΈ / 2) β β β§ πΈ β β β§
(absβ((πΉβπ) β (πΉβπ΅))) β β) β ((πΈ / 2) < πΈ β ((πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅))) β¨ (absβ((πΉβπ) β (πΉβπ΅))) < πΈ))) |
46 | 12, 44, 8, 45 | syl3anc 1238 |
. . 3
β’ (π β ((πΈ / 2) < πΈ β ((πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅))) β¨ (absβ((πΉβπ) β (πΉβπ΅))) < πΈ))) |
47 | 43, 46 | mpd 13 |
. 2
β’ (π β ((πΈ / 2) < (absβ((πΉβπ) β (πΉβπ΅))) β¨ (absβ((πΉβπ) β (πΉβπ΅))) < πΈ)) |
48 | 40, 41, 47 | mpjaodan 798 |
1
β’ (π β (absβ((πΉβπ) β (πΉβπ΅))) < πΈ) |