Metamath Proof Explorer


Theorem negne0bi

Description: A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999)

Ref Expression
Hypothesis negidi.1 A
Assertion negne0bi A 0 A 0

Proof

Step Hyp Ref Expression
1 negidi.1 A
2 negeq0 A A = 0 A = 0
3 1 2 ax-mp A = 0 A = 0
4 3 necon3bii A 0 A 0