Theorem nn0ssge0

Description: Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	nn0ssge0	⊢ ℕ0 ⊆ ( 0 [,) +∞ )

Proof

Step	Hyp	Ref	Expression
1		nn0rp0	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ( 0 [,) +∞ ) )
2	1	ssriv	⊢ ℕ0 ⊆ ( 0 [,) +∞ )