Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
nn0zd
Next ⟩
nnzd
Metamath Proof Explorer
Ascii
Unicode
Theorem
nn0zd
Description:
A positive integer is an integer.
(Contributed by
Mario Carneiro
, 28-May-2016)
Ref
Expression
Hypothesis
nn0zd.1
⊢
φ
→
A
∈
ℕ
0
Assertion
nn0zd
⊢
φ
→
A
∈
ℤ
Proof
Step
Hyp
Ref
Expression
1
nn0zd.1
⊢
φ
→
A
∈
ℕ
0
2
nn0ssz
⊢
ℕ
0
⊆
ℤ
3
2
1
sseldi
⊢
φ
→
A
∈
ℤ