Database
REAL AND COMPLEX NUMBERS
Integer sets
Nonnegative integers (as a subset of complex numbers)
nn0cn
Next ⟩
nn0rei
Metamath Proof Explorer
Ascii
Structured
Theorem
nn0cn
Description:
A nonnegative integer is a complex number.
(Contributed by
NM
, 9-May-2004)
Ref
Expression
Assertion
nn0cn
⊢
(
𝐴
∈ ℕ
_{0}
→
𝐴
∈ ℂ )
Proof
Step
Hyp
Ref
Expression
1
nn0sscn
⊢
ℕ
_{0}
⊆ ℂ
2
1
sseli
⊢
(
𝐴
∈ ℕ
_{0}
→
𝐴
∈ ℂ )