Metamath Proof Explorer


Theorem abs00i

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 NM, 28-Jul-1999)

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

Proof

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