Theorem absvalsq

Description: Square of value of absolute value function. (Contributed by NM, 16-Jan-2006)

	Ref	Expression
Assertion	absvalsq	|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )

Proof

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