Theorem elxrge0 13302

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 11135	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11142	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13236	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 690	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 12979	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 482	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 561	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 303	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1087   ∈ wcel 2106   class class class wbr 5103  (class class class)co 7349  0cc0 10984  +∞cpnf 11119  ℝ^*cxr 11121   ≤ cle 11123  [,]cicc 13195

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-cnex 11040  ax-resscn 11041  ax-1cn 11042  ax-addrcl 11045  ax-rnegex 11055  ax-cnre 11057

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-id 5528  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-iota 6443  df-fun 6493  df-fv 6499  df-ov 7352  df-oprab 7353  df-mpo 7354  df-pnf 11124  df-mnf 11125  df-xr 11126  df-ltxr 11127  df-le 11128  df-icc 13199

This theorem is referenced by:  0e0iccpnf  13304  ge0xaddcl  13307  ge0xmulcl  13308  xnn0xrge0  13351  xrge0subm  20752  psmetxrge0  23579  isxmet2d  23593  prdsdsf  23633  prdsxmetlem  23634  comet  23782  stdbdxmet  23784  xrge0gsumle  24109  xrge0tsms  24110  metdsf  24124  metds0  24126  metdstri  24127  metdsre  24129  metdseq0  24130  metdscnlem  24131  metnrmlem1a  24134  xrhmeo  24222  lebnumlem1  24237  xrge0f  25009  itg2const2  25019  itg2uba  25021  itg2mono  25031  itg2gt0  25038  itg2cnlem2  25040  itg2cn  25041  iblss  25082  itgle  25087  itgeqa  25091  ibladdlem  25097  iblabs  25106  iblabsr  25107  iblmulc2  25108  itgsplit  25113  bddmulibl  25116  bddiblnc  25119  xrge0addge  31434  xrge0infss  31437  xrge0addcld  31439  xrge0subcld  31440  xrge00  31649  xrge0tsmsd  31671  esummono  32387  gsumesum  32392  esumsnf  32397  esumrnmpt2  32401  esumpmono  32412  hashf2  32417  measge0  32540  measle0  32541  measssd  32548  measunl  32549  omssubaddlem  32633  omssubadd  32634  carsgsigalem  32649  pmeasmono  32658  sibfinima  32673  prob01  32747  dstrvprob  32805  itg2addnclem  35988  ibladdnclem  35993  iblabsnc  36001  iblmulc2nc  36002  ftc1anclem4  36013  ftc1anclem5  36014  ftc1anclem6  36015  ftc1anclem7  36016  ftc1anclem8  36017  ftc1anc  36018  xrge0ge0  43277  rrxsphere  46516