Theorem nn0rp0

Description: A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020)

	Ref	Expression
Assertion	nn0rp0	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
3		elrege0	⊢ ( 𝑁 ∈ ( 0 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) )
4	1 2 3	sylanbrc	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 [,) +∞ ) )