Metamath Proof Explorer


Theorem xmetge0

Description: The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmetge0 D ∞Met X A X B X 0 A D B

Proof

Step Hyp Ref Expression
1 simp1 D ∞Met X A X B X D ∞Met X
2 simp2 D ∞Met X A X B X A X
3 simp3 D ∞Met X A X B X B X
4 xmettri2 D ∞Met X A X B X B X B D B A D B + 𝑒 A D B
5 1 2 3 3 4 syl13anc D ∞Met 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 xmet0 D ∞Met X B X B D B = 0
11 10 3adant2 D ∞Met X A X B X B D B = 0
12 9 11 eqtr4id D ∞Met X A X B X 2 𝑒 0 = B D B
13 xmetcl D ∞Met 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 ∞Met X A X B X 2 𝑒 A D B = A D B + 𝑒 A D B
16 5 12 15 3brtr4d D ∞Met X A X B X 2 𝑒 0 2 𝑒 A D B
17 0xr 0 *
18 2rp 2 +
19 18 a1i D ∞Met 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 ∞Met X A X B X 0 A D B 2 𝑒 0 2 𝑒 A D B
22 16 21 mpbird D ∞Met X A X B X 0 A D B