Theorem nn0ssge0

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

	Ref	Expression
Assertion	nn0ssge0	$$⊢{\mathbb{N}}_0\subseteq \left[0,\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0rp0	$$⊢n\in {\mathbb{N}}_0\to n\in \left[0,\mathrm{+\infty }\right)$$
2	1	ssriv	$$⊢{\mathbb{N}}_0\subseteq \left[0,\mathrm{+\infty }\right)$$