Theorem elxrge0

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		df-3an	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\wedge A\le \mathrm{+\infty }\right)\leftrightarrow \left(\left(A\in {ℝ}^{*}\wedge 0\le A\right)\wedge A\le \mathrm{+\infty }\right)$$
2		0xr	$$⊢0\in {ℝ}^{*}$$
3		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
4		elicc1	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A\in {ℝ}^{*}\wedge 0\le A\wedge A\le \mathrm{+\infty }\right)\right)$$
5	2 3 4	mp2an	$$⊢A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A\in {ℝ}^{*}\wedge 0\le A\wedge A\le \mathrm{+\infty }\right)$$
6		pnfge	$$⊢A\in {ℝ}^{*}\to A\le \mathrm{+\infty }$$
7	6	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\to A\le \mathrm{+\infty }$$
8	7	pm4.71i	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\leftrightarrow \left(\left(A\in {ℝ}^{*}\wedge 0\le A\right)\wedge A\le \mathrm{+\infty }\right)$$
9	1 5 8	3bitr4i	$$⊢A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A\in {ℝ}^{*}\wedge 0\le A\right)$$