Metamath Proof Explorer


Theorem eqnegd

Description: A complex number equals its negative iff it is zero. Deduction form of eqneg . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypothesis eqnegd.1
|- ( ph -> A e. CC )
Assertion eqnegd
|- ( ph -> ( A = -u A <-> A = 0 ) )

Proof

Step Hyp Ref Expression
1 eqnegd.1
 |-  ( ph -> A e. CC )
2 eqneg
 |-  ( A e. CC -> ( A = -u A <-> A = 0 ) )
3 1 2 syl
 |-  ( ph -> ( A = -u A <-> A = 0 ) )