Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
neg1ne0
Next ⟩
neg1lt0
Metamath Proof Explorer
Ascii
Structured
Theorem
neg1ne0
Description:
-1 is nonzero.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
neg1ne0
⊢
- 1 ≠ 0
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1 ∈ ℂ
2
ax-1ne0
⊢
1 ≠ 0
3
1
2
negne0i
⊢
- 1 ≠ 0