Metamath Proof Explorer


Theorem absne0d

Description: The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of Gleason p. 133. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses abscld.1 ( 𝜑𝐴 ∈ ℂ )
absne0d.2 ( 𝜑𝐴 ≠ 0 )
Assertion absne0d ( 𝜑 → ( abs ‘ 𝐴 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 abscld.1 ( 𝜑𝐴 ∈ ℂ )
2 absne0d.2 ( 𝜑𝐴 ≠ 0 )
3 1 abs00ad ( 𝜑 → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
4 3 necon3bid ( 𝜑 → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
5 2 4 mpbird ( 𝜑 → ( abs ‘ 𝐴 ) ≠ 0 )