Step | Hyp | Ref
| Expression |
1 | | metdscnlem.1 |
. . . . . 6
β’ (π β π· β (βMetβπ)) |
2 | | metdscnlem.2 |
. . . . . 6
β’ (π β π β π) |
3 | | metdscn.f |
. . . . . . 7
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
4 | 3 | metdsf 24133 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
5 | 1, 2, 4 | syl2anc 585 |
. . . . 5
β’ (π β πΉ:πβΆ(0[,]+β)) |
6 | | metdscnlem.3 |
. . . . 5
β’ (π β π΄ β π) |
7 | 5, 6 | ffvelcdmd 7031 |
. . . 4
β’ (π β (πΉβπ΄) β (0[,]+β)) |
8 | | eliccxr 13281 |
. . . 4
β’ ((πΉβπ΄) β (0[,]+β) β (πΉβπ΄) β
β*) |
9 | 7, 8 | syl 17 |
. . 3
β’ (π β (πΉβπ΄) β
β*) |
10 | | metdscnlem.4 |
. . . . . 6
β’ (π β π΅ β π) |
11 | 5, 10 | ffvelcdmd 7031 |
. . . . 5
β’ (π β (πΉβπ΅) β (0[,]+β)) |
12 | | eliccxr 13281 |
. . . . 5
β’ ((πΉβπ΅) β (0[,]+β) β (πΉβπ΅) β
β*) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β (πΉβπ΅) β
β*) |
14 | 13 | xnegcld 13148 |
. . 3
β’ (π β
-π(πΉβπ΅) β
β*) |
15 | 9, 14 | xaddcld 13149 |
. 2
β’ (π β ((πΉβπ΄) +π
-π(πΉβπ΅)) β
β*) |
16 | | xmetcl 23606 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
17 | 1, 6, 10, 16 | syl3anc 1372 |
. 2
β’ (π β (π΄π·π΅) β
β*) |
18 | | metdscnlem.5 |
. . 3
β’ (π β π
β
β+) |
19 | 18 | rpxrd 12887 |
. 2
β’ (π β π
β
β*) |
20 | 3 | metdstri 24136 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΄) β€ ((π΄π·π΅) +π (πΉβπ΅))) |
21 | 1, 2, 6, 10, 20 | syl22anc 838 |
. . 3
β’ (π β (πΉβπ΄) β€ ((π΄π·π΅) +π (πΉβπ΅))) |
22 | | elxrge0 13303 |
. . . . . 6
β’ ((πΉβπ΄) β (0[,]+β) β ((πΉβπ΄) β β* β§ 0 β€
(πΉβπ΄))) |
23 | 22 | simprbi 498 |
. . . . 5
β’ ((πΉβπ΄) β (0[,]+β) β 0 β€ (πΉβπ΄)) |
24 | 7, 23 | syl 17 |
. . . 4
β’ (π β 0 β€ (πΉβπ΄)) |
25 | | elxrge0 13303 |
. . . . . . 7
β’ ((πΉβπ΅) β (0[,]+β) β ((πΉβπ΅) β β* β§ 0 β€
(πΉβπ΅))) |
26 | 25 | simprbi 498 |
. . . . . 6
β’ ((πΉβπ΅) β (0[,]+β) β 0 β€ (πΉβπ΅)) |
27 | 11, 26 | syl 17 |
. . . . 5
β’ (π β 0 β€ (πΉβπ΅)) |
28 | | ge0nemnf 13021 |
. . . . 5
β’ (((πΉβπ΅) β β* β§ 0 β€
(πΉβπ΅)) β (πΉβπ΅) β -β) |
29 | 13, 27, 28 | syl2anc 585 |
. . . 4
β’ (π β (πΉβπ΅) β -β) |
30 | | xmetge0 23619 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β 0 β€ (π΄π·π΅)) |
31 | 1, 6, 10, 30 | syl3anc 1372 |
. . . 4
β’ (π β 0 β€ (π΄π·π΅)) |
32 | | xlesubadd 13111 |
. . . 4
β’ ((((πΉβπ΄) β β* β§ (πΉβπ΅) β β* β§ (π΄π·π΅) β β*) β§ (0 β€
(πΉβπ΄) β§ (πΉβπ΅) β -β β§ 0 β€ (π΄π·π΅))) β (((πΉβπ΄) +π
-π(πΉβπ΅)) β€ (π΄π·π΅) β (πΉβπ΄) β€ ((π΄π·π΅) +π (πΉβπ΅)))) |
33 | 9, 13, 17, 24, 29, 31, 32 | syl33anc 1386 |
. . 3
β’ (π β (((πΉβπ΄) +π
-π(πΉβπ΅)) β€ (π΄π·π΅) β (πΉβπ΄) β€ ((π΄π·π΅) +π (πΉβπ΅)))) |
34 | 21, 33 | mpbird 257 |
. 2
β’ (π β ((πΉβπ΄) +π
-π(πΉβπ΅)) β€ (π΄π·π΅)) |
35 | | metdscnlem.6 |
. 2
β’ (π β (π΄π·π΅) < π
) |
36 | 15, 17, 19, 34, 35 | xrlelttrd 13008 |
1
β’ (π β ((πΉβπ΄) +π
-π(πΉβπ΅)) < π
) |