Metamath Proof Explorer

Theorem xmetrtri

Description: One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Assertion xmetrtri ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→ADC+𝑒−BDC≤ADB

Proof

Step Hyp Ref Expression
1 3ancomb ⊢A∈X∧B∈X∧C∈X↔A∈X∧C∈X∧B∈X
2 xmettri ⊢D∈∞Met⁡X∧A∈X∧C∈X∧B∈X→ADC≤ADB+𝑒BDC
3 1 2 sylan2b ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→ADC≤ADB+𝑒BDC
4 xmetcl ⊢D∈∞Met⁡X∧A∈X∧C∈X→ADC∈ℝ*
5 4 3adant3r2 ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→ADC∈ℝ*
6 xmetcl ⊢D∈∞Met⁡X∧B∈X∧C∈X→BDC∈ℝ*
7 6 3adant3r1 ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→BDC∈ℝ*
8 xmetcl ⊢D∈∞Met⁡X∧A∈X∧B∈X→ADB∈ℝ*
9 8 3adant3r3 ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→ADB∈ℝ*
10 xmetge0 ⊢D∈∞Met⁡X∧A∈X∧C∈X→0≤ADC
11 10 3adant3r2 ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→0≤ADC
12 xmetge0 ⊢D∈∞Met⁡X∧B∈X∧C∈X→0≤BDC
13 12 3adant3r1 ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→0≤BDC
14 ge0nemnf ⊢BDC∈ℝ*∧0≤BDC→BDC≠−∞
15 7 13 14 syl2anc ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→BDC≠−∞
16 xmetge0 ⊢D∈∞Met⁡X∧A∈X∧B∈X→0≤ADB
17 16 3adant3r3 ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→0≤ADB
18 xlesubadd ⊢ADC∈ℝ*∧BDC∈ℝ*∧ADB∈ℝ*∧0≤ADC∧BDC≠−∞∧0≤ADB→ADC+𝑒−BDC≤ADB↔ADC≤ADB+𝑒BDC
19 5 7 9 11 15 17 18 syl33anc ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→ADC+𝑒−BDC≤ADB↔ADC≤ADB+𝑒BDC
20 3 19 mpbird ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→ADC+𝑒−BDC≤ADB