Theorem absrpcl

Description: The absolute value of a nonzero number is a positive real. (Contributed by FL, 27-Dec-2007) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	absrpcl	|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		absval	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
2	1	adantr	|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
3		simpl	|- ( ( A e. CC /\ A =/= 0 ) -> A e. CC )
4	3	cjmulrcld	|- ( ( A e. CC /\ A =/= 0 ) -> ( A x. ( * ` A ) ) e. RR )
5	3	cjmulge0d	|- ( ( A e. CC /\ A =/= 0 ) -> 0 <_ ( A x. ( * ` A ) ) )
6	3	cjcld	|- ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) e. CC )
7		simpr	|- ( ( A e. CC /\ A =/= 0 ) -> A =/= 0 )
8	3 7	cjne0d	|- ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) =/= 0 )
9	3 6 7 8	mulne0d	|- ( ( A e. CC /\ A =/= 0 ) -> ( A x. ( * ` A ) ) =/= 0 )
10	4 5 9	ne0gt0d	|- ( ( A e. CC /\ A =/= 0 ) -> 0 < ( A x. ( * ` A ) ) )
11	4 10	elrpd	|- ( ( A e. CC /\ A =/= 0 ) -> ( A x. ( * ` A ) ) e. RR+ )
12		rpsqrtcl	|- ( ( A x. ( * ` A ) ) e. RR+ -> ( sqrt ` ( A x. ( * ` A ) ) ) e. RR+ )
13	11 12	syl	|- ( ( A e. CC /\ A =/= 0 ) -> ( sqrt ` ( A x. ( * ` A ) ) ) e. RR+ )
14	2 13	eqeltrd	|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )