This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐷 ∈ ( ∞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 ≤ ( 𝐴 𝐷 𝐵 ) )