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 e. CC
Assertion negne0bi 
|- ( A =/= 0 <-> -u A =/= 0 )

Proof

Step Hyp Ref Expression
1 negidi.1 
 |-  A e. CC
2 negeq0 
 |-  ( A e. CC -> ( A = 0 <-> -u A = 0 ) )
3 1 2 ax-mp 
 |-  ( A = 0 <-> -u A = 0 )
4 3 necon3bii 
 |-  ( A =/= 0 <-> -u A =/= 0 )