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 → A D C + 𝑒 − B D C ≤ A D B

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 → A D C ≤ A D B + 𝑒 B D C
3 1 2 sylan2b ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C ≤ A D B + 𝑒 B D C
4 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ C ∈ X → A D C ∈ ℝ *
5 4 3adant3r2 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C ∈ ℝ *
6 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ X ∧ C ∈ X → B D C ∈ ℝ *
7 6 3adant3r1 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D C ∈ ℝ *
8 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
9 8 3adant3r3 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ∈ ℝ *
10 xmetge0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ C ∈ X → 0 ≤ A D C
11 10 3adant3r2 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → 0 ≤ A D C
12 xmetge0 ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ X ∧ C ∈ X → 0 ≤ B D C
13 12 3adant3r1 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → 0 ≤ B D C
14 ge0nemnf ⊢ B D C ∈ ℝ * ∧ 0 ≤ B D C → B D C ≠ −∞
15 7 13 14 syl2anc ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D C ≠ −∞
16 xmetge0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B
17 16 3adant3r3 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → 0 ≤ A D B
18 xlesubadd ⊢ A D C ∈ ℝ * ∧ B D C ∈ ℝ * ∧ A D B ∈ ℝ * ∧ 0 ≤ A D C ∧ B D C ≠ −∞ ∧ 0 ≤ A D B → A D C + 𝑒 − B D C ≤ A D B ↔ A D C ≤ A D B + 𝑒 B D C
19 5 7 9 11 15 17 18 syl33anc ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C + 𝑒 − B D C ≤ A D B ↔ A D C ≤ A D B + 𝑒 B D C
20 3 19 mpbird ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C + 𝑒 − B D C ≤ A D B