xmetge0

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

		Ref	Expression
	Assertion	xmetge0	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to 0 \leq A D B$

Proof

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

Metamath Proof Explorer

Theorem xmetge0

Proof