Metamath Proof Explorer


Theorem absgt0i

Description: The absolute value of a nonzero number is positive. Remark in Apostol p. 363. (Contributed by NM, 1-Oct-1999)

Ref Expression
Hypothesis absvalsqi.1
|- A e. CC
Assertion absgt0i
|- ( A =/= 0 <-> 0 < ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 absvalsqi.1
 |-  A e. CC
2 absgt0
 |-  ( A e. CC -> ( A =/= 0 <-> 0 < ( abs ` A ) ) )
3 1 2 ax-mp
 |-  ( A =/= 0 <-> 0 < ( abs ` A ) )