Metamath Proof Explorer


Theorem subne0ad

Description: If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d . Contrapositive of subeq0bd . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses negidd.1 φ A
pncand.2 φ B
subne0ad.3 φ A B 0
Assertion subne0ad φ A B

Proof

Step Hyp Ref Expression
1 negidd.1 φ A
2 pncand.2 φ B
3 subne0ad.3 φ A B 0
4 1 2 subeq0ad φ A B = 0 A = B
5 4 necon3bid φ A B 0 A B
6 3 5 mpbid φ A B