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