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	|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> ( abs ` ( A - B ) ) e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		subcl	|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2	1	3adant3	|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> ( A - B ) e. CC )
3		simp1	|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> A e. CC )
4		simp2	|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> B e. CC )
5		simp3	|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> A =/= B )
6	3 4 5	subne0d	|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> ( A - B ) =/= 0 )
7	2 6	absrpcld	|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> ( abs ` ( A - B ) ) e. RR+ )