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≤ADB

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→BDB≤ADB+𝑒ADB
5 1 2 3 3 4 syl13anc ⊢D∈PsMet⁡X∧A∈X∧B∈X→BDB≤ADB+𝑒ADB
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→BDB=0
11 10 3adant2 ⊢D∈PsMet⁡X∧A∈X∧B∈X→BDB=0
12 9 11 eqtr4id ⊢D∈PsMet⁡X∧A∈X∧B∈X→2⋅𝑒0=BDB
13 psmetcl ⊢D∈PsMet⁡X∧A∈X∧B∈X→ADB∈ℝ*
14 x2times ⊢ADB∈ℝ*→2⋅𝑒ADB=ADB+𝑒ADB
15 13 14 syl ⊢D∈PsMet⁡X∧A∈X∧B∈X→2⋅𝑒ADB=ADB+𝑒ADB
16 5 12 15 3brtr4d ⊢D∈PsMet⁡X∧A∈X∧B∈X→2⋅𝑒0≤2⋅𝑒ADB
17 0xr ⊢0∈ℝ*
18 2rp ⊢2∈ℝ+
19 18 a1i ⊢D∈PsMet⁡X∧A∈X∧B∈X→2∈ℝ+
20 xlemul2 ⊢0∈ℝ*∧ADB∈ℝ*∧2∈ℝ+→0≤ADB↔2⋅𝑒0≤2⋅𝑒ADB
21 17 13 19 20 mp3an2i ⊢D∈PsMet⁡X∧A∈X∧B∈X→0≤ADB↔2⋅𝑒0≤2⋅𝑒ADB
22 16 21 mpbird ⊢D∈PsMet⁡X∧A∈X∧B∈X→0≤ADB