Metamath Proof Explorer

Theorem sqneg

Description: The square of the negative of a number. (Contributed by NM, 15-Jan-2006)

Ref Expression
Assertion sqneg 
|- ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )

Proof

Step Hyp Ref Expression
1 mul2neg 
 |-  ( ( A e. CC /\ A e. CC ) -> ( -u A x. -u A ) = ( A x. A ) )
2 1 anidms 
 |-  ( A e. CC -> ( -u A x. -u A ) = ( A x. A ) )
3 negcl 
 |-  ( A e. CC -> -u A e. CC )
4 sqval 
 |-  ( -u A e. CC -> ( -u A ^ 2 ) = ( -u A x. -u A ) )
5 3 4 syl 
 |-  ( A e. CC -> ( -u A ^ 2 ) = ( -u A x. -u A ) )
6 sqval 
 |-  ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
7 2 5 6 3eqtr4d 
 |-  ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )