Theorem 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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
3		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ℂ )
4		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ℂ )
5		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
6	3 4 5	subne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 − 𝐵 ) ≠ 0 )
7	2 6	absrpcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ+ )