Theorem absresq

Description: Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006)

	Ref	Expression
Assertion	absresq	|- ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		cjre	|- ( A e. RR -> ( * ` A ) = A )
2	1	oveq2d	|- ( A e. RR -> ( A x. ( * ` A ) ) = ( A x. A ) )
3		recn	|- ( A e. RR -> A e. CC )
4		absvalsq	|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
5	3 4	syl	|- ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
6	3	sqvald	|- ( A e. RR -> ( A ^ 2 ) = ( A x. A ) )
7	2 5 6	3eqtr4d	|- ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )