This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )