abssubrp

Description: The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	abssubrp	$⊢ (A \in ℂ \land B \in ℂ \land A \neq B) \to \|A - B\| \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
2	1	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land A \neq B) \to A - B \in ℂ$
3		simp1	$⊢ (A \in ℂ \land B \in ℂ \land A \neq B) \to A \in ℂ$
4		simp2	$⊢ (A \in ℂ \land B \in ℂ \land A \neq B) \to B \in ℂ$
5		simp3	$⊢ (A \in ℂ \land B \in ℂ \land A \neq B) \to A \neq B$
6	3 4 5	subne0d	$⊢ (A \in ℂ \land B \in ℂ \land A \neq B) \to A - B \neq 0$
7	2 6	absrpcld	$⊢ (A \in ℂ \land B \in ℂ \land A \neq B) \to \|A - B\| \in ℝ^{+}$

Metamath Proof Explorer