Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
neg1z
Next ⟩
znegclb
Metamath Proof Explorer
Ascii
Structured
Theorem
neg1z
Description:
-1 is an integer.
(Contributed by
David A. Wheeler
, 5-Dec-2018)
Ref
Expression
Assertion
neg1z
⊢
- 1 ∈ ℤ
Proof
Step
Hyp
Ref
Expression
1
1nn
⊢
1 ∈ ℕ
2
nnnegz
⊢
( 1 ∈ ℕ → - 1 ∈ ℤ )
3
1
2
ax-mp
⊢
- 1 ∈ ℤ