Theorem abscl

Description: Real closure of absolute value. (Contributed by NM, 3-Oct-1999)

	Ref	Expression
Assertion	abscl	|- ( A e. CC -> ( abs ` A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		absval	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
2		cjmulrcl	|- ( A e. CC -> ( A x. ( * ` A ) ) e. RR )
3		cjmulge0	|- ( A e. CC -> 0 <_ ( A x. ( * ` A ) ) )
4		resqrtcl	|- ( ( ( A x. ( * ` A ) ) e. RR /\ 0 <_ ( A x. ( * ` A ) ) ) -> ( sqrt ` ( A x. ( * ` A ) ) ) e. RR )
5	2 3 4	syl2anc	|- ( A e. CC -> ( sqrt ` ( A x. ( * ` A ) ) ) e. RR )
6	1 5	eqeltrd	|- ( A e. CC -> ( abs ` A ) e. RR )