Metamath Proof Explorer

Theorem absidm

Description: The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
2 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
3 absid 
 |-  ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
4 1 2 3 syl2anc 
 |-  ( A e. CC -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )