# Metamath Proof Explorer

## 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]↔\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)↔\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]↔\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]↔\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)↔\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]↔\left({A}\in {ℝ}^{*}\wedge 0\le {A}\right)$