Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Subtraction
negne0bi
Next ⟩
negrebi
Metamath Proof Explorer
Ascii
Unicode
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