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

Theorem elxrge0 11687
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 984 . 2  |-  ( ( A  e.  RR*  /\  0  <_  A  /\  A  <_ +oo )  <->  ( ( A  e.  RR*  /\  0  <_  A )  /\  A  <_ +oo ) )
2 0xr 9633 . . 3  |-  0  e.  RR*
3 pnfxr 11358 . . 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 676 . 2  |-  ( A  e.  ( 0 [,] +oo )  <->  ( A  e. 
RR*  /\  0  <_  A  /\  A  <_ +oo )
)
6 pnfge 11378 . . . 4  |-  ( A  e.  RR*  ->  A  <_ +oo )
76adantr 466 . . 3  |-  ( ( A  e.  RR*  /\  0  <_  A )  ->  A  <_ +oo )
87pm4.71i 636 . 2  |-  ( ( A  e.  RR*  /\  0  <_  A )  <->  ( ( A  e.  RR*  /\  0  <_  A )  /\  A  <_ +oo ) )
91, 5, 83bitr4i 280 1  |-  ( A  e.  ( 0 [,] +oo )  <->  ( A  e. 
RR*  /\  0  <_  A ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    /\ w3a 982    e. wcel 1872   class class class wbr 4361  (class class class)co 6244   0cc0 9485   +oocpnf 9618   RR*cxr 9620    <_ cle 9622   [,]cicc 11584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-i2m1 9553  ax-1ne0 9554  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-iota 5503  df-fun 5541  df-fv 5547  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-icc 11588
This theorem is referenced by:  0e0iccpnf  11689  ge0xaddcl  11692  ge0xmulcl  11693  xrge0subm  18947  psmetxrge0  21266  isxmet2d  21279  prdsdsf  21319  prdsxmetlem  21320  comet  21465  stdbdxmet  21467  xrge0gsumle  21788  xrge0tsms  21789  metdsf  21802  metds0  21804  metdstri  21805  metdsre  21807  metdseq0  21808  metdscnlem  21809  metnrmlem1a  21812  metnrmlem1  21813  metdsfOLD  21817  metds0OLD  21819  metdstriOLD  21820  metdsreOLD  21822  metdseq0OLD  21823  metdscnlemOLD  21824  metnrmlem1aOLD  21827  metnrmlem1OLD  21828  xrhmeo  21911  lebnumlem1  21926  lebnumlem1OLD  21929  xrge0f  22626  itg2const2  22636  itg2uba  22638  itg2mono  22648  itg2gt0  22655  itg2cnlem2  22657  itg2cn  22658  iblss  22699  itgle  22704  itgeqa  22708  ibladdlem  22714  iblabs  22723  iblabsr  22724  iblmulc2  22725  itgsplit  22730  bddmulibl  22733  xrge0addge  28282  xrge0infss  28285  xrge0infssOLD  28286  xrge0addcld  28289  xrge0subcld  28290  xrge00  28394  xrge0tsmsd  28495  esummono  28822  gsumesum  28827  esumsnf  28832  esumrnmpt2  28836  esumpmono  28847  hashf2  28852  measge0  28976  measle0  28977  measssd  28984  measunl  28985  omssubaddlem  29074  omssubadd  29075  omssubaddlemOLD  29078  omssubaddOLD  29079  carsgsigalem  29094  pmeasmono  29104  sibfinima  29119  prob01  29193  dstrvprob  29251  itg2addnclem  31900  ibladdnclem  31905  iblabsnc  31913  iblmulc2nc  31914  bddiblnc  31919  ftc1anclem4  31927  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  xrge0ge0  37467
  Copyright terms: Public domain W3C validator