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 ) |
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 ) |