Metamath Proof Explorer


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 ∈ ℝ