Theorem elxrge0 13454

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 1099	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11222	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11229	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13386	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 702	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13125	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 484	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 567	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 305	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   ∈ wcel 2141   class class class wbr 5097  (class class class)co 7390  0cc0 11066  +∞cpnf 11206  ℝ^*cxr 11208   ≤ cle 11210  [,]cicc 13345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123  ax-1cn 11124  ax-addrcl 11127  ax-rnegex 11137  ax-cnre 11139

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6471  df-fun 6517  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-icc 13349

This theorem is referenced by:  0e0iccpnf  13456  ge0xaddcl  13459  ge0xmulcl  13460  xnn0xrge0  13503  xrge0subm  21482  psmetxrge0  24360  isxmet2d  24374  prdsdsf  24414  prdsxmetlem  24415  comet  24560  stdbdxmet  24562  xrge0gsumle  24881  xrge0tsms  24882  metdsf  24896  metds0  24898  metdstri  24899  metdsre  24901  metdseq0  24902  metdscnlem  24903  metnrmlem1a  24906  xrhmeo  24995  lebnumlem1  25010  xrge0f  25780  itg2const2  25790  itg2uba  25792  itg2mono  25802  itg2gt0  25809  itg2cnlem2  25811  itg2cn  25812  iblss  25854  itgle  25859  itgeqa  25863  ibladdlem  25869  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgsplit  25885  bddmulibl  25888  bddiblnc  25891  xrge0addge  32920  xrge0infss  32922  xrge0addcld  32924  xrge0subcld  32925  xrge00  33152  xrge0tsmsd  33213  fldextrspundglemul  33936  esummono  34311  gsumesum  34316  esumsnf  34321  esumrnmpt2  34325  esumpmono  34336  hashf2  34341  measge0  34464  measle0  34465  measssd  34472  measunl  34473  omssubaddlem  34556  omssubadd  34557  carsgsigalem  34572  pmeasmono  34581  sibfinima  34596  prob01  34670  dstrvprob  34729  itg2addnclem  38130  ibladdnclem  38135  iblabsnc  38143  iblmulc2nc  38144  ftc1anclem4  38155  ftc1anclem5  38156  ftc1anclem6  38157  ftc1anclem7  38158  ftc1anclem8  38159  ftc1anc  38160  xrge0ge0  45883  rrxsphere  49330