Metamath Proof Explorer

Theorem psmetge0

Description: The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetge0 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → D ∈ PsMet ⁡ X
2 simp2 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A ∈ X
3 simp3 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B ∈ X
4 psmettri2 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ B ∈ X → B D B ≤ A D B + 𝑒 A D B
5 1 2 3 3 4 syl13anc ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D B ≤ A D B + 𝑒 A D B
6 2re ⊢ 2 ∈ ℝ
7 rexr ⊢ 2 ∈ ℝ → 2 ∈ ℝ *
8 xmul01 ⊢ 2 ∈ ℝ * → 2 ⋅ 𝑒 0 = 0
9 6 7 8 mp2b ⊢ 2 ⋅ 𝑒 0 = 0
10 psmet0 ⊢ D ∈ PsMet ⁡ X ∧ B ∈ X → B D B = 0
11 10 3adant2 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → B D B = 0
12 9 11 eqtr4id ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 2 ⋅ 𝑒 0 = B D B
13 psmetcl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
14 x2times ⊢ A D B ∈ ℝ * → 2 ⋅ 𝑒 A D B = A D B + 𝑒 A D B
15 13 14 syl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 2 ⋅ 𝑒 A D B = A D B + 𝑒 A D B
16 5 12 15 3brtr4d ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 2 ⋅ 𝑒 0 ≤ 2 ⋅ 𝑒 A D B
17 0xr ⊢ 0 ∈ ℝ *
18 2rp ⊢ 2 ∈ ℝ +
19 18 a1i ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 2 ∈ ℝ +
20 xlemul2 ⊢ 0 ∈ ℝ * ∧ A D B ∈ ℝ * ∧ 2 ∈ ℝ + → 0 ≤ A D B ↔ 2 ⋅ 𝑒 0 ≤ 2 ⋅ 𝑒 A D B
21 17 13 19 20 mp3an2i ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B ↔ 2 ⋅ 𝑒 0 ≤ 2 ⋅ 𝑒 A D B
22 16 21 mpbird ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B