Theorem elxrge0 13438

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 1087	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11265	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11272	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13372	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 688	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13114	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 479	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 558	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 302	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   ∈ wcel 2104   class class class wbr 5147  (class class class)co 7411  0cc0 11112  +∞cpnf 11249  ℝ^*cxr 11251   ≤ cle 11253  [,]cicc 13331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-addrcl 11173  ax-rnegex 11183  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-icc 13335

This theorem is referenced by:  0e0iccpnf  13440  ge0xaddcl  13443  ge0xmulcl  13444  xnn0xrge0  13487  xrge0subm  21186  psmetxrge0  24039  isxmet2d  24053  prdsdsf  24093  prdsxmetlem  24094  comet  24242  stdbdxmet  24244  xrge0gsumle  24569  xrge0tsms  24570  metdsf  24584  metds0  24586  metdstri  24587  metdsre  24589  metdseq0  24590  metdscnlem  24591  metnrmlem1a  24594  xrhmeo  24691  lebnumlem1  24707  xrge0f  25481  itg2const2  25491  itg2uba  25493  itg2mono  25503  itg2gt0  25510  itg2cnlem2  25512  itg2cn  25513  iblss  25554  itgle  25559  itgeqa  25563  ibladdlem  25569  iblabs  25578  iblabsr  25579  iblmulc2  25580  itgsplit  25585  bddmulibl  25588  bddiblnc  25591  xrge0addge  32237  xrge0infss  32240  xrge0addcld  32242  xrge0subcld  32243  xrge00  32454  xrge0tsmsd  32479  esummono  33350  gsumesum  33355  esumsnf  33360  esumrnmpt2  33364  esumpmono  33375  hashf2  33380  measge0  33503  measle0  33504  measssd  33511  measunl  33512  omssubaddlem  33596  omssubadd  33597  carsgsigalem  33612  pmeasmono  33621  sibfinima  33636  prob01  33710  dstrvprob  33768  itg2addnclem  36842  ibladdnclem  36847  iblabsnc  36855  iblmulc2nc  36856  ftc1anclem4  36867  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  xrge0ge0  44355  rrxsphere  47521