Metamath Proof Explorer

Theorem absneg

Description: Absolute value of the negative. (Contributed by NM, 27-Feb-2005)

Ref Expression
Assertion absneg 
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 cjneg 
 |-  ( A e. CC -> ( * ` -u A ) = -u ( * ` A ) )
2 1 oveq2d 
 |-  ( A e. CC -> ( -u A x. ( * ` -u A ) ) = ( -u A x. -u ( * ` A ) ) )
3 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
4 mul2neg 
 |-  ( ( A e. CC /\ ( * ` A ) e. CC ) -> ( -u A x. -u ( * ` A ) ) = ( A x. ( * ` A ) ) )
5 3 4 mpdan 
 |-  ( A e. CC -> ( -u A x. -u ( * ` A ) ) = ( A x. ( * ` A ) ) )
6 2 5 eqtrd 
 |-  ( A e. CC -> ( -u A x. ( * ` -u A ) ) = ( A x. ( * ` A ) ) )
7 6 fveq2d 
 |-  ( A e. CC -> ( sqrt ` ( -u A x. ( * ` -u A ) ) ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
8 negcl 
 |-  ( A e. CC -> -u A e. CC )
9 absval 
 |-  ( -u A e. CC -> ( abs ` -u A ) = ( sqrt ` ( -u A x. ( * ` -u A ) ) ) )
10 8 9 syl 
 |-  ( A e. CC -> ( abs ` -u A ) = ( sqrt ` ( -u A x. ( * ` -u A ) ) ) )
11 absval 
 |-  ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
12 7 10 11 3eqtr4d 
 |-  ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )