Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
nnz
Next ⟩
nn0z
Metamath Proof Explorer
Ascii
Structured
Theorem
nnz
Description:
A positive integer is an integer.
(Contributed by
NM
, 9-May-2004)
Ref
Expression
Assertion
nnz
⊢
(
𝑁
∈ ℕ →
𝑁
∈ ℤ )
Proof
Step
Hyp
Ref
Expression
1
nnssz
⊢
ℕ ⊆ ℤ
2
1
sseli
⊢
(
𝑁
∈ ℕ →
𝑁
∈ ℤ )