Theorem xmetge0

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

	Ref	Expression
Assertion	xmetge0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2		simp2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
3		simp3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
4		xmettri2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
5	1 2 3 3 4	syl13anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
6		2re	⊢ 2 ∈ ℝ
7		rexr	⊢ ( 2 ∈ ℝ → 2 ∈ ℝ* )
8		xmul01	⊢ ( 2 ∈ ℝ* → ( 2 ·e 0 ) = 0 )
9	6 7 8	mp2b	⊢ ( 2 ·e 0 ) = 0
10		xmet0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 0 )
11	10	3adant2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐵 ) = 0 )
12	9 11	eqtr4id	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 2 ·e 0 ) = ( 𝐵 𝐷 𝐵 ) )
13		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
14		x2times	⊢ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* → ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
15	13 14	syl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) )
16	5 12 15	3brtr4d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 2 ·e 0 ) ≤ ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) )
17		0xr	⊢ 0 ∈ ℝ*
18		2rp	⊢ 2 ∈ ℝ+
19	18	a1i	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 2 ∈ ℝ+ )
20		xlemul2	⊢ ( ( 0 ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ 2 ∈ ℝ+ ) → ( 0 ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 2 ·e 0 ) ≤ ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) ) )
21	17 13 19 20	mp3an2i	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 0 ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 2 ·e 0 ) ≤ ( 2 ·e ( 𝐴 𝐷 𝐵 ) ) ) )
22	16 21	mpbird	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )