Theorem elrege0

Description: The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Assertion	elrege0	$$⊢A\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(A\in ℝ\wedge 0\le A\right)$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		elicopnf	$$⊢0\in ℝ\to \left(A\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(A\in ℝ\wedge 0\le A\right)\right)$$
3	1 2	ax-mp	$$⊢A\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(A\in ℝ\wedge 0\le A\right)$$