Theorem elxrge02

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016)

	Ref	Expression
Assertion	elxrge02	$$⊢A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A=0\vee A\in {ℝ}^{+}\vee A=\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		0xr	$$⊢0\in {ℝ}^{*}$$
2		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
3		0lepnf	$$⊢0\le \mathrm{+\infty }$$
4		eliccioo	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0\le \mathrm{+\infty }\right)\to \left(A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A=0\vee A\in \left(0,\mathrm{+\infty }\right)\vee A=\mathrm{+\infty }\right)\right)$$
5	1 2 3 4	mp3an	$$⊢A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A=0\vee A\in \left(0,\mathrm{+\infty }\right)\vee A=\mathrm{+\infty }\right)$$
6		biid	$$⊢A=0\leftrightarrow A=0$$
7		ioorp	$$⊢\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$$
8	7	eleq2i	$$⊢A\in \left(0,\mathrm{+\infty }\right)\leftrightarrow A\in {ℝ}^{+}$$
9		biid	$$⊢A=\mathrm{+\infty }\leftrightarrow A=\mathrm{+\infty }$$
10	6 8 9	3orbi123i	$$⊢\left(A=0\vee A\in \left(0,\mathrm{+\infty }\right)\vee A=\mathrm{+\infty }\right)\leftrightarrow \left(A=0\vee A\in {ℝ}^{+}\vee A=\mathrm{+\infty }\right)$$
11	5 10	bitri	$$⊢A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A=0\vee A\in {ℝ}^{+}\vee A=\mathrm{+\infty }\right)$$