Theorem xrge0ge0

Description: A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	xrge0ge0	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to 0\le A$$

Proof

Step	Hyp	Ref	Expression
1		elxrge0	$$⊢A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A\in {ℝ}^{*}\wedge 0\le A\right)$$
2	1	biimpi	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to \left(A\in {ℝ}^{*}\wedge 0\le A\right)$$
3	2	simprd	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to 0\le A$$