Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
nnssz
Next ⟩
nn0ssz
Metamath Proof Explorer
Ascii
Structured
Theorem
nnssz
Description:
Positive integers are a subset of integers.
(Contributed by
NM
, 9-Jan-2002)
Ref
Expression
Assertion
nnssz
⊢
ℕ ⊆ ℤ
Proof
Step
Hyp
Ref
Expression
1
nnz
⊢
(
𝑥
∈ ℕ →
𝑥
∈ ℤ )
2
1
ssriv
⊢
ℕ ⊆ ℤ