xmetgt0

Description: The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xmetgt0	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (A \neq B \leftrightarrow 0 < A D B)$

Step	Hyp	Ref	Expression
1		xmetge0	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to 0 \leq A D B$
2	1	biantrud	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (A D B \leq 0 \leftrightarrow (A D B \leq 0 \land 0 \leq A D B))$
3		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B \in ℝ^{*}$
4		0xr	$⊢ 0 \in ℝ^{*}$
5		xrletri3	$⊢ (A D B \in ℝ^{} \land 0 \in ℝ^{}) \to (A D B = 0 \leftrightarrow (A D B \leq 0 \land 0 \leq A D B))$
6	3 4 5	sylancl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (A D B = 0 \leftrightarrow (A D B \leq 0 \land 0 \leq A D B))$
7	2 6	bitr4d	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (A D B \leq 0 \leftrightarrow A D B = 0)$
8		xrlenlt	$⊢ (A D B \in ℝ^{} \land 0 \in ℝ^{}) \to (A D B \leq 0 \leftrightarrow \neg 0 < A D B)$
9	3 4 8	sylancl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (A D B \leq 0 \leftrightarrow \neg 0 < A D B)$
10		xmeteq0	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (A D B = 0 \leftrightarrow A = B)$
11	7 9 10	3bitr3d	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (\neg 0 < A D B \leftrightarrow A = B)$
12	11	necon1abid	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to (A \neq B \leftrightarrow 0 < A D B)$

Metamath Proof Explorer