Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π· β (Metβπ)) |
2 | | simpr2 1005 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΅ β π) |
3 | | simpr3 1006 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β πΆ β π) |
4 | | simpr1 1004 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΄ β π) |
5 | | mettri 14100 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΅ β π β§ πΆ β π β§ π΄ β π)) β (π΅π·πΆ) β€ ((π΅π·π΄) + (π΄π·πΆ))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1250 |
. . . 4
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·πΆ) β€ ((π΅π·π΄) + (π΄π·πΆ))) |
7 | | metcl 14080 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β β) |
8 | 1, 4, 2, 7 | syl3anc 1248 |
. . . . . 6
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β β) |
9 | 8 | recnd 7999 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β β) |
10 | | metcl 14080 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ π΄ β π β§ πΆ β π) β (π΄π·πΆ) β β) |
11 | 1, 4, 3, 10 | syl3anc 1248 |
. . . . . 6
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·πΆ) β β) |
12 | 11 | recnd 7999 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·πΆ) β β) |
13 | | metsym 14098 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ π΅ β π β§ π΄ β π) β (π΅π·π΄) = (π΄π·π΅)) |
14 | 1, 2, 4, 13 | syl3anc 1248 |
. . . . . 6
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·π΄) = (π΄π·π΅)) |
15 | 14 | oveq1d 5903 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΅π·π΄) + (π΄π·πΆ)) = ((π΄π·π΅) + (π΄π·πΆ))) |
16 | 9, 12, 15 | comraddd 8127 |
. . . 4
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΅π·π΄) + (π΄π·πΆ)) = ((π΄π·πΆ) + (π΄π·π΅))) |
17 | 6, 16 | breqtrd 4041 |
. . 3
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·πΆ) β€ ((π΄π·πΆ) + (π΄π·π΅))) |
18 | | metcl 14080 |
. . . . 5
β’ ((π· β (Metβπ) β§ π΅ β π β§ πΆ β π) β (π΅π·πΆ) β β) |
19 | 1, 2, 3, 18 | syl3anc 1248 |
. . . 4
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·πΆ) β β) |
20 | 19, 8, 11 | lesubaddd 8512 |
. . 3
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (((π΅π·πΆ) β (π΄π·π΅)) β€ (π΄π·πΆ) β (π΅π·πΆ) β€ ((π΄π·πΆ) + (π΄π·π΅)))) |
21 | 17, 20 | mpbird 167 |
. 2
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΅π·πΆ) β (π΄π·π΅)) β€ (π΄π·πΆ)) |
22 | | mettri 14100 |
. . . 4
β’ ((π· β (Metβπ) β§ (π΄ β π β§ πΆ β π β§ π΅ β π)) β (π΄π·πΆ) β€ ((π΄π·π΅) + (π΅π·πΆ))) |
23 | 1, 4, 3, 2, 22 | syl13anc 1250 |
. . 3
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·πΆ) β€ ((π΄π·π΅) + (π΅π·πΆ))) |
24 | 19 | recnd 7999 |
. . . 4
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·πΆ) β β) |
25 | 9, 24 | addcomd 8121 |
. . 3
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅) + (π΅π·πΆ)) = ((π΅π·πΆ) + (π΄π·π΅))) |
26 | 23, 25 | breqtrd 4041 |
. 2
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·πΆ) β€ ((π΅π·πΆ) + (π΄π·π΅))) |
27 | 11, 19, 8 | absdifled 11201 |
. 2
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((absβ((π΄π·πΆ) β (π΅π·πΆ))) β€ (π΄π·π΅) β (((π΅π·πΆ) β (π΄π·π΅)) β€ (π΄π·πΆ) β§ (π΄π·πΆ) β€ ((π΅π·πΆ) + (π΄π·π΅))))) |
28 | 21, 26, 27 | mpbir2and 945 |
1
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (absβ((π΄π·πΆ) β (π΅π·πΆ))) β€ (π΄π·π΅)) |