Step | Hyp | Ref
| Expression |
1 | | xmetdcn2.2 |
. . . . 5
β’ πΆ =
(distββ*π ) |
2 | 1 | xrsxmet 24195 |
. . . 4
β’ πΆ β
(βMetββ*) |
3 | 2 | a1i 11 |
. . 3
β’ (π β πΆ β
(βMetββ*)) |
4 | | metdcn.d |
. . . 4
β’ (π β π· β (βMetβπ)) |
5 | | metdcn.a |
. . . 4
β’ (π β π΄ β π) |
6 | | metdcn.b |
. . . 4
β’ (π β π΅ β π) |
7 | | xmetcl 23707 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
8 | 4, 5, 6, 7 | syl3anc 1372 |
. . 3
β’ (π β (π΄π·π΅) β
β*) |
9 | | metdcn.y |
. . . 4
β’ (π β π β π) |
10 | | metdcn.z |
. . . 4
β’ (π β π β π) |
11 | | xmetcl 23707 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β (ππ·π) β
β*) |
12 | 4, 9, 10, 11 | syl3anc 1372 |
. . 3
β’ (π β (ππ·π) β
β*) |
13 | | xmetcl 23707 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΅ β π) β (ππ·π΅) β
β*) |
14 | 4, 9, 6, 13 | syl3anc 1372 |
. . . . 5
β’ (π β (ππ·π΅) β
β*) |
15 | | metdcn.r |
. . . . . . 7
β’ (π β π
β
β+) |
16 | 15 | rphalfcld 12977 |
. . . . . 6
β’ (π β (π
/ 2) β
β+) |
17 | 16 | rpred 12965 |
. . . . 5
β’ (π β (π
/ 2) β β) |
18 | | xmetcl 23707 |
. . . . . . 7
β’ ((πΆ β
(βMetββ*) β§ (π΄π·π΅) β β* β§ (ππ·π΅) β β*) β ((π΄π·π΅)πΆ(ππ·π΅)) β
β*) |
19 | 3, 8, 14, 18 | syl3anc 1372 |
. . . . . 6
β’ (π β ((π΄π·π΅)πΆ(ππ·π΅)) β
β*) |
20 | 16 | rpxrd 12966 |
. . . . . 6
β’ (π β (π
/ 2) β
β*) |
21 | | xmetcl 23707 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π β π) β (π΄π·π) β
β*) |
22 | 4, 5, 9, 21 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΄π·π) β
β*) |
23 | 1 | xmetrtri2 23732 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π β π β§ π΅ β π)) β ((π΄π·π΅)πΆ(ππ·π΅)) β€ (π΄π·π)) |
24 | 4, 5, 9, 6, 23 | syl13anc 1373 |
. . . . . . 7
β’ (π β ((π΄π·π΅)πΆ(ππ·π΅)) β€ (π΄π·π)) |
25 | | metdcn.4 |
. . . . . . 7
β’ (π β (π΄π·π) < (π
/ 2)) |
26 | 19, 22, 20, 24, 25 | xrlelttrd 13088 |
. . . . . 6
β’ (π β ((π΄π·π΅)πΆ(ππ·π΅)) < (π
/ 2)) |
27 | 19, 20, 26 | xrltled 13078 |
. . . . 5
β’ (π β ((π΄π·π΅)πΆ(ππ·π΅)) β€ (π
/ 2)) |
28 | | xmetlecl 23722 |
. . . . 5
β’ ((πΆ β
(βMetββ*) β§ ((π΄π·π΅) β β* β§ (ππ·π΅) β β*) β§ ((π
/ 2) β β β§
((π΄π·π΅)πΆ(ππ·π΅)) β€ (π
/ 2))) β ((π΄π·π΅)πΆ(ππ·π΅)) β β) |
29 | 3, 8, 14, 17, 27, 28 | syl122anc 1380 |
. . . 4
β’ (π β ((π΄π·π΅)πΆ(ππ·π΅)) β β) |
30 | | xmetcl 23707 |
. . . . . . 7
β’ ((πΆ β
(βMetββ*) β§ (ππ·π΅) β β* β§ (ππ·π) β β*) β ((ππ·π΅)πΆ(ππ·π)) β
β*) |
31 | 3, 14, 12, 30 | syl3anc 1372 |
. . . . . 6
β’ (π β ((ππ·π΅)πΆ(ππ·π)) β
β*) |
32 | | xmetcl 23707 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π΅ β π β§ π β π) β (π΅π·π) β
β*) |
33 | 4, 6, 10, 32 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΅π·π) β
β*) |
34 | | xmetsym 23723 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π β§ π΅ β π) β (ππ·π΅) = (π΅π·π)) |
35 | 4, 9, 6, 34 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (ππ·π΅) = (π΅π·π)) |
36 | | xmetsym 23723 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β (ππ·π) = (ππ·π)) |
37 | 4, 9, 10, 36 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (ππ·π) = (ππ·π)) |
38 | 35, 37 | oveq12d 7379 |
. . . . . . . 8
β’ (π β ((ππ·π΅)πΆ(ππ·π)) = ((π΅π·π)πΆ(ππ·π))) |
39 | 1 | xmetrtri2 23732 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ (π΅ β π β§ π β π β§ π β π)) β ((π΅π·π)πΆ(ππ·π)) β€ (π΅π·π)) |
40 | 4, 6, 10, 9, 39 | syl13anc 1373 |
. . . . . . . 8
β’ (π β ((π΅π·π)πΆ(ππ·π)) β€ (π΅π·π)) |
41 | 38, 40 | eqbrtrd 5131 |
. . . . . . 7
β’ (π β ((ππ·π΅)πΆ(ππ·π)) β€ (π΅π·π)) |
42 | | metdcn.5 |
. . . . . . 7
β’ (π β (π΅π·π) < (π
/ 2)) |
43 | 31, 33, 20, 41, 42 | xrlelttrd 13088 |
. . . . . 6
β’ (π β ((ππ·π΅)πΆ(ππ·π)) < (π
/ 2)) |
44 | 31, 20, 43 | xrltled 13078 |
. . . . 5
β’ (π β ((ππ·π΅)πΆ(ππ·π)) β€ (π
/ 2)) |
45 | | xmetlecl 23722 |
. . . . 5
β’ ((πΆ β
(βMetββ*) β§ ((ππ·π΅) β β* β§ (ππ·π) β β*) β§ ((π
/ 2) β β β§
((ππ·π΅)πΆ(ππ·π)) β€ (π
/ 2))) β ((ππ·π΅)πΆ(ππ·π)) β β) |
46 | 3, 14, 12, 17, 44, 45 | syl122anc 1380 |
. . . 4
β’ (π β ((ππ·π΅)πΆ(ππ·π)) β β) |
47 | 29, 46 | readdcld 11192 |
. . 3
β’ (π β (((π΄π·π΅)πΆ(ππ·π΅)) + ((ππ·π΅)πΆ(ππ·π))) β β) |
48 | | xmettri 23727 |
. . . . 5
β’ ((πΆ β
(βMetββ*) β§ ((π΄π·π΅) β β* β§ (ππ·π) β β* β§ (ππ·π΅) β β*)) β
((π΄π·π΅)πΆ(ππ·π)) β€ (((π΄π·π΅)πΆ(ππ·π΅)) +π ((ππ·π΅)πΆ(ππ·π)))) |
49 | 3, 8, 12, 14, 48 | syl13anc 1373 |
. . . 4
β’ (π β ((π΄π·π΅)πΆ(ππ·π)) β€ (((π΄π·π΅)πΆ(ππ·π΅)) +π ((ππ·π΅)πΆ(ππ·π)))) |
50 | 29, 46 | rexaddd 13162 |
. . . 4
β’ (π β (((π΄π·π΅)πΆ(ππ·π΅)) +π ((ππ·π΅)πΆ(ππ·π))) = (((π΄π·π΅)πΆ(ππ·π΅)) + ((ππ·π΅)πΆ(ππ·π)))) |
51 | 49, 50 | breqtrd 5135 |
. . 3
β’ (π β ((π΄π·π΅)πΆ(ππ·π)) β€ (((π΄π·π΅)πΆ(ππ·π΅)) + ((ππ·π΅)πΆ(ππ·π)))) |
52 | | xmetlecl 23722 |
. . 3
β’ ((πΆ β
(βMetββ*) β§ ((π΄π·π΅) β β* β§ (ππ·π) β β*) β§
((((π΄π·π΅)πΆ(ππ·π΅)) + ((ππ·π΅)πΆ(ππ·π))) β β β§ ((π΄π·π΅)πΆ(ππ·π)) β€ (((π΄π·π΅)πΆ(ππ·π΅)) + ((ππ·π΅)πΆ(ππ·π))))) β ((π΄π·π΅)πΆ(ππ·π)) β β) |
53 | 3, 8, 12, 47, 51, 52 | syl122anc 1380 |
. 2
β’ (π β ((π΄π·π΅)πΆ(ππ·π)) β β) |
54 | 15 | rpred 12965 |
. 2
β’ (π β π
β β) |
55 | 29, 46, 54, 26, 43 | lt2halvesd 12409 |
. 2
β’ (π β (((π΄π·π΅)πΆ(ππ·π΅)) + ((ππ·π΅)πΆ(ππ·π))) < π
) |
56 | 53, 47, 54, 51, 55 | lelttrd 11321 |
1
β’ (π β ((π΄π·π΅)πΆ(ππ·π)) < π
) |