Metamath Proof Explorer


Theorem eqnegad

Description: If a complex number equals its own negative, it is zero. One-way deduction form of eqneg . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses eqnegad.1
|- ( ph -> A e. CC )
eqnegad.2
|- ( ph -> A = -u A )
Assertion eqnegad
|- ( ph -> A = 0 )

Proof

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