Description: The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 . Generalization of neg11d . (Contributed by David Moews, 28-Feb-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | negidd.1 | |- ( ph -> A e. CC ) |
|
| neg11ad.2 | |- ( ph -> B e. CC ) |
||
| Assertion | neg11ad | |- ( ph -> ( -u A = -u B <-> A = B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | negidd.1 | |- ( ph -> A e. CC ) |
|
| 2 | neg11ad.2 | |- ( ph -> B e. CC ) |
|
| 3 | neg11 | |- ( ( A e. CC /\ B e. CC ) -> ( -u A = -u B <-> A = B ) ) |
|
| 4 | 1 2 3 | syl2anc | |- ( ph -> ( -u A = -u B <-> A = B ) ) |