Database
REAL AND COMPLEX NUMBERS
Integer sets
Positive integers (as a subset of complex numbers)
nncnd
Next ⟩
peano2nnd
Metamath Proof Explorer
Ascii
Unicode
Theorem
nncnd
Description:
A positive integer is a complex number.
(Contributed by
Mario Carneiro
, 27-May-2016)
Ref
Expression
Hypothesis
nnred.1
⊢
φ
→
A
∈
ℕ
Assertion
nncnd
⊢
φ
→
A
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
nnred.1
⊢
φ
→
A
∈
ℕ
2
nnsscn
⊢
ℕ
⊆
ℂ
3
2
1
sseldi
⊢
φ
→
A
∈
ℂ