Theorem nn0rp0

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
2		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
3		elrege0	$$⊢N\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(N\in ℝ\wedge 0\le N\right)$$
4	1 2 3	sylanbrc	$$⊢N\in {\mathbb{N}}_0\to N\in \left[0,\mathrm{+\infty }\right)$$