Metamath Proof Explorer

Theorem abs00ad

Description: A complex number is zero iff its absolute value is zero. Deduction form of abs00 . (Contributed by David Moews, 28-Feb-2017)

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

Proof

Step Hyp Ref Expression
1 abs00ad.1 
 |-  ( ph -> A e. CC )
2 abs00 
 |-  ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )
3 1 2 syl 
 |-  ( ph -> ( ( abs ` A ) = 0 <-> A = 0 ) )