Metamath Proof Explorer

Theorem absge0

Description: Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion absge0 
|- ( A e. CC -> 0 <_ ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 cjmulrcl 
 |-  ( A e. CC -> ( A x. ( * ` A ) ) e. RR )
2 cjmulge0 
 |-  ( A e. CC -> 0 <_ ( A x. ( * ` A ) ) )
3 sqrtge0 
 |-  ( ( ( A x. ( * ` A ) ) e. RR /\ 0 <_ ( A x. ( * ` A ) ) ) -> 0 <_ ( sqrt ` ( A x. ( * ` A ) ) ) )
4 1 2 3 syl2anc 
 |-  ( A e. CC -> 0 <_ ( sqrt ` ( A x. ( * ` A ) ) ) )
5 absval 
 |-  ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
6 4 5 breqtrrd 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )