# Metamath Proof Explorer

## 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]↔\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]↔\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]↔\left({A}=0\vee {A}\in \left(0,\mathrm{+\infty }\right)\vee {A}=\mathrm{+\infty }\right)$
6 biid ${⊢}{A}=0↔{A}=0$
7 ioorp ${⊢}\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$
8 7 eleq2i ${⊢}{A}\in \left(0,\mathrm{+\infty }\right)↔{A}\in {ℝ}^{+}$
9 biid ${⊢}{A}=\mathrm{+\infty }↔{A}=\mathrm{+\infty }$
10 6 8 9 3orbi123i ${⊢}\left({A}=0\vee {A}\in \left(0,\mathrm{+\infty }\right)\vee {A}=\mathrm{+\infty }\right)↔\left({A}=0\vee {A}\in {ℝ}^{+}\vee {A}=\mathrm{+\infty }\right)$
11 5 10 bitri ${⊢}{A}\in \left[0,\mathrm{+\infty }\right]↔\left({A}=0\vee {A}\in {ℝ}^{+}\vee {A}=\mathrm{+\infty }\right)$