Database
REAL AND COMPLEX NUMBERS
Integer sets
Nonnegative integers (as a subset of complex numbers)
nn0rei
Next ⟩
nn0cni
Metamath Proof Explorer
Ascii
Unicode
Theorem
nn0rei
Description:
A nonnegative integer is a real number.
(Contributed by
NM
, 14-May-2003)
Ref
Expression
Hypothesis
nn0rei.1
⊢
A
∈
ℕ
0
Assertion
nn0rei
⊢
A
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
nn0rei.1
⊢
A
∈
ℕ
0
2
nn0ssre
⊢
ℕ
0
⊆
ℝ
3
2
1
sselii
⊢
A
∈
ℝ