Metamath Proof Explorer

Theorem absgt0

Description: The absolute value of a nonzero number is positive. (Contributed by NM, 1-Oct-1999) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion absgt0 
|- ( A e. CC -> ( A =/= 0 <-> 0 < ( abs ` A ) ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( A e. CC -> 0 e. RR )
2 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
3 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
4 1 2 3 leltned 
 |-  ( A e. CC -> ( 0 < ( abs ` A ) <-> ( abs ` A ) =/= 0 ) )
5 abs00 
 |-  ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )
6 5 necon3bid 
 |-  ( A e. CC -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
7 4 6 bitr2d 
 |-  ( A e. CC -> ( A =/= 0 <-> 0 < ( abs ` A ) ) )