MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elxrge0 Structured version   Unicode version

Theorem elxrge0 11683
Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
Assertion
Ref Expression
elxrge0  |-  ( A  e.  ( 0 [,] +oo )  <->  ( A  e. 
RR*  /\  0  <_  A ) )

Proof of Theorem elxrge0
StepHypRef Expression
1 df-3an 976 . 2  |-  ( ( A  e.  RR*  /\  0  <_  A  /\  A  <_ +oo )  <->  ( ( A  e.  RR*  /\  0  <_  A )  /\  A  <_ +oo ) )
2 0xr 9670 . . 3  |-  0  e.  RR*
3 pnfxr 11374 . . 3  |- +oo  e.  RR*
4 elicc1 11626 . . 3  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR* )  ->  ( A  e.  ( 0 [,] +oo )  <->  ( A  e.  RR*  /\  0  <_  A  /\  A  <_ +oo )
) )
52, 3, 4mp2an 670 . 2  |-  ( A  e.  ( 0 [,] +oo )  <->  ( A  e. 
RR*  /\  0  <_  A  /\  A  <_ +oo )
)
6 pnfge 11392 . . . 4  |-  ( A  e.  RR*  ->  A  <_ +oo )
76adantr 463 . . 3  |-  ( ( A  e.  RR*  /\  0  <_  A )  ->  A  <_ +oo )
87pm4.71i 630 . 2  |-  ( ( A  e.  RR*  /\  0  <_  A )  <->  ( ( A  e.  RR*  /\  0  <_  A )  /\  A  <_ +oo ) )
91, 5, 83bitr4i 277 1  |-  ( A  e.  ( 0 [,] +oo )  <->  ( A  e. 
RR*  /\  0  <_  A ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    /\ w3a 974    e. wcel 1842   class class class wbr 4395  (class class class)co 6278   0cc0 9522   +oocpnf 9655   RR*cxr 9657    <_ cle 9659   [,]cicc 11585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-i2m1 9590  ax-1ne0 9591  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-iota 5533  df-fun 5571  df-fv 5577  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-icc 11589
This theorem is referenced by:  0e0iccpnf  11685  ge0xaddcl  11688  ge0xmulcl  11689  xrge0subm  18779  psmetxrge0  21109  isxmet2d  21122  prdsdsf  21162  prdsxmetlem  21163  comet  21308  stdbdxmet  21310  xrge0gsumle  21630  xrge0tsms  21631  metdsf  21644  metds0  21646  metdstri  21647  metdsre  21649  metdseq0  21650  metdscnlem  21651  metnrmlem1a  21654  metnrmlem1  21655  xrhmeo  21738  lebnumlem1  21753  xrge0f  22430  itg2const2  22440  itg2uba  22442  itg2mono  22452  itg2gt0  22459  itg2cnlem2  22461  itg2cn  22462  iblss  22503  itgle  22508  itgeqa  22512  ibladdlem  22518  iblabs  22527  iblabsr  22528  iblmulc2  22529  itgsplit  22534  bddmulibl  22537  xrge0addge  28019  xrge0infss  28022  xrge0addcld  28024  xrge0subcld  28025  xrge00  28126  xrge0tsmsd  28228  esummono  28501  gsumesum  28506  esumsnf  28511  esumrnmpt2  28515  esumpmono  28526  hashf2  28531  measge0  28655  measle0  28656  measssd  28663  measunl  28664  omssubaddlem  28747  omssubadd  28748  carsgsigalem  28763  pmeasmono  28772  sibfinima  28787  prob01  28858  dstrvprob  28916  itg2addnclem  31439  ibladdnclem  31444  iblabsnc  31452  iblmulc2nc  31453  bddiblnc  31458  ftc1anclem4  31466  ftc1anclem5  31467  ftc1anclem6  31468  ftc1anclem7  31469  ftc1anclem8  31470  ftc1anc  31471
  Copyright terms: Public domain W3C validator