Metamath Proof Explorer

Theorem xmetgt0

Description: The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmetgt0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A ≠ B ↔ 0 < A D B

Proof

Step Hyp Ref Expression
1 xmetge0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B
2 1 biantrud ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ 0 ↔ A D B ≤ 0 ∧ 0 ≤ A D B
3 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
4 0xr ⊢ 0 ∈ ℝ *
5 xrletri3 ⊢ A D B ∈ ℝ * ∧ 0 ∈ ℝ * → A D B = 0 ↔ A D B ≤ 0 ∧ 0 ≤ A D B
6 3 4 5 sylancl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A D B ≤ 0 ∧ 0 ≤ A D B
7 2 6 bitr4d ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ 0 ↔ A D B = 0
8 xrlenlt ⊢ A D B ∈ ℝ * ∧ 0 ∈ ℝ * → A D B ≤ 0 ↔ ¬ 0 < A D B
9 3 4 8 sylancl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ 0 ↔ ¬ 0 < A D B
10 xmeteq0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B = 0 ↔ A = B
11 7 9 10 3bitr3d ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → ¬ 0 < A D B ↔ A = B
12 11 necon1abid ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A ≠ B ↔ 0 < A D B