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 𝐴 ∈ ℂ
Assertion absgt0i ( 𝐴 ≠ 0 ↔ 0 < ( abs ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 absvalsqi.1 𝐴 ∈ ℂ
2 absgt0 ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 ↔ 0 < ( abs ‘ 𝐴 ) ) )
3 1 2 ax-mp ( 𝐴 ≠ 0 ↔ 0 < ( abs ‘ 𝐴 ) )