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
|- ( ph -> A e. CC )
absne0d.2
|- ( ph -> A =/= 0 )
Assertion absne0d
|- ( ph -> ( abs ` A ) =/= 0 )

Proof

Step Hyp Ref Expression
1 abscld.1
 |-  ( ph -> A e. CC )
2 absne0d.2
 |-  ( ph -> A =/= 0 )
3 1 abs00ad
 |-  ( ph -> ( ( abs ` A ) = 0 <-> A = 0 ) )
4 3 necon3bid
 |-  ( ph -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
5 2 4 mpbird
 |-  ( ph -> ( abs ` A ) =/= 0 )