Theorem rge0ssre

Description: Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018) (Proof shortened by AV, 8-Sep-2019)

	Ref	Expression
Assertion	rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		elrege0	$$⊢x\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(x\in ℝ\wedge 0\le x\right)$$
2	1	simplbi	$$⊢x\in \left[0,\mathrm{+\infty }\right)\to x\in ℝ$$
3	2	ssriv	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$