# 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 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 0\le {A}{D}{B}$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
2 simp2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}\in {X}$
3 simp3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}\in {X}$
4 xmettri2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {B}\in {X}\right)\right)\to {B}{D}{B}\le \left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{B}\right)$
5 1 2 3 3 4 syl13anc ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}{D}{B}\le \left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{B}\right)$
6 xmet0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {B}\in {X}\right)\to {B}{D}{B}=0$
7 6 3adant2 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {B}{D}{B}=0$
8 2re ${⊢}2\in ℝ$
9 rexr ${⊢}2\in ℝ\to 2\in {ℝ}^{*}$
10 xmul01 ${⊢}2\in {ℝ}^{*}\to 2{\cdot }_{𝑒}0=0$
11 8 9 10 mp2b ${⊢}2{\cdot }_{𝑒}0=0$
12 7 11 syl6reqr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 2{\cdot }_{𝑒}0={B}{D}{B}$
13 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}\in {ℝ}^{*}$
14 x2times ${⊢}{A}{D}{B}\in {ℝ}^{*}\to 2{\cdot }_{𝑒}\left({A}{D}{B}\right)=\left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{B}\right)$
15 13 14 syl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 2{\cdot }_{𝑒}\left({A}{D}{B}\right)=\left({A}{D}{B}\right){+}_{𝑒}\left({A}{D}{B}\right)$
16 5 12 15 3brtr4d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 2{\cdot }_{𝑒}0\le 2{\cdot }_{𝑒}\left({A}{D}{B}\right)$
17 0xr ${⊢}0\in {ℝ}^{*}$
18 2rp ${⊢}2\in {ℝ}^{+}$
19 18 a1i ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 2\in {ℝ}^{+}$
20 xlemul2 ${⊢}\left(0\in {ℝ}^{*}\wedge {A}{D}{B}\in {ℝ}^{*}\wedge 2\in {ℝ}^{+}\right)\to \left(0\le {A}{D}{B}↔2{\cdot }_{𝑒}0\le 2{\cdot }_{𝑒}\left({A}{D}{B}\right)\right)$
21 17 13 19 20 mp3an2i ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left(0\le {A}{D}{B}↔2{\cdot }_{𝑒}0\le 2{\cdot }_{𝑒}\left({A}{D}{B}\right)\right)$
22 16 21 mpbird ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 0\le {A}{D}{B}$