Theorem elxrge0 13385

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 11191	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11198	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13317	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 693	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13056	. . . 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 5100  (class class class)co 7368  0cc0 11038  +∞cpnf 11175  ℝ^*cxr 11177   ≤ cle 11179  [,]cicc 13276

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 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690  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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-icc 13280

This theorem is referenced by:  0e0iccpnf  13387  ge0xaddcl  13390  ge0xmulcl  13391  xnn0xrge0  13434  xrge0subm  21410  psmetxrge0  24269  isxmet2d  24283  prdsdsf  24323  prdsxmetlem  24324  comet  24469  stdbdxmet  24471  xrge0gsumle  24790  xrge0tsms  24791  metdsf  24805  metds0  24807  metdstri  24808  metdsre  24810  metdseq0  24811  metdscnlem  24812  metnrmlem1a  24815  xrhmeo  24912  lebnumlem1  24928  xrge0f  25700  itg2const2  25710  itg2uba  25712  itg2mono  25722  itg2gt0  25729  itg2cnlem2  25731  itg2cn  25732  iblss  25774  itgle  25779  itgeqa  25783  ibladdlem  25789  iblabs  25798  iblabsr  25799  iblmulc2  25800  itgsplit  25805  bddmulibl  25808  bddiblnc  25811  xrge0addge  32848  xrge0infss  32850  xrge0addcld  32852  xrge0subcld  32853  xrge00  33106  xrge0tsmsd  33166  fldextrspundglemul  33856  esummono  34231  gsumesum  34236  esumsnf  34241  esumrnmpt2  34245  esumpmono  34256  hashf2  34261  measge0  34384  measle0  34385  measssd  34392  measunl  34393  omssubaddlem  34476  omssubadd  34477  carsgsigalem  34492  pmeasmono  34501  sibfinima  34516  prob01  34590  dstrvprob  34649  itg2addnclem  37916  ibladdnclem  37921  iblabsnc  37929  iblmulc2nc  37930  ftc1anclem4  37941  ftc1anclem5  37942  ftc1anclem6  37943  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  xrge0ge0  45700  rrxsphere  49102