Theorem elxrge0 13410

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

Assertion

Ref	Expression
elxrge0	⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Proof of Theorem elxrge0

Step	Hyp	Ref	Expression
1		df-3an 1089	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11192	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11199	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13342	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 693	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13081	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 480	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 559	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 303	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5085  (class class class)co 7367  0cc0 11038  +∞cpnf 11176  ℝ^*cxr 11178   ≤ cle 11180  [,]cicc 13301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-icc 13305

This theorem is referenced by:  0e0iccpnf  13412  ge0xaddcl  13415  ge0xmulcl  13416  xnn0xrge0  13459  xrge0subm  21423  psmetxrge0  24278  isxmet2d  24292  prdsdsf  24332  prdsxmetlem  24333  comet  24478  stdbdxmet  24480  xrge0gsumle  24799  xrge0tsms  24800  metdsf  24814  metds0  24816  metdstri  24817  metdsre  24819  metdseq0  24820  metdscnlem  24821  metnrmlem1a  24824  xrhmeo  24913  lebnumlem1  24928  xrge0f  25698  itg2const2  25708  itg2uba  25710  itg2mono  25720  itg2gt0  25727  itg2cnlem2  25729  itg2cn  25730  iblss  25772  itgle  25777  itgeqa  25781  ibladdlem  25787  iblabs  25796  iblabsr  25797  iblmulc2  25798  itgsplit  25803  bddmulibl  25806  bddiblnc  25809  xrge0addge  32831  xrge0infss  32833  xrge0addcld  32835  xrge0subcld  32836  xrge00  33074  xrge0tsmsd  33134  fldextrspundglemul  33823  esummono  34198  gsumesum  34203  esumsnf  34208  esumrnmpt2  34212  esumpmono  34223  hashf2  34228  measge0  34351  measle0  34352  measssd  34359  measunl  34360  omssubaddlem  34443  omssubadd  34444  carsgsigalem  34459  pmeasmono  34468  sibfinima  34483  prob01  34557  dstrvprob  34616  itg2addnclem  37992  ibladdnclem  37997  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  xrge0ge0  45777  rrxsphere  49224