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

Theorem elxrge0 11039
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 939 . 2  |-  ( ( A  e.  RR*  /\  0  <_  A  /\  A  <_  +oo )  <->  ( ( A  e.  RR*  /\  0  <_  A )  /\  A  <_  +oo ) )
2 0xr 9162 . . 3  |-  0  e.  RR*
3 pnfxr 10744 . . 3  |-  +oo  e.  RR*
4 elicc1 10991 . . 3  |-  ( ( 0  e.  RR*  /\  +oo  e.  RR* )  ->  ( A  e.  ( 0 [,]  +oo )  <->  ( A  e.  RR*  /\  0  <_  A  /\  A  <_  +oo )
) )
52, 3, 4mp2an 655 . 2  |-  ( A  e.  ( 0 [,] 
+oo )  <->  ( A  e.  RR*  /\  0  <_  A  /\  A  <_  +oo )
)
6 pnfge 10758 . . . 4  |-  ( A  e.  RR*  ->  A  <_  +oo )
76adantr 453 . . 3  |-  ( ( A  e.  RR*  /\  0  <_  A )  ->  A  <_  +oo )
87pm4.71i 615 . 2  |-  ( ( A  e.  RR*  /\  0  <_  A )  <->  ( ( A  e.  RR*  /\  0  <_  A )  /\  A  <_  +oo ) )
91, 5, 83bitr4i 270 1  |-  ( A  e.  ( 0 [,] 
+oo )  <->  ( A  e.  RR*  /\  0  <_  A ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    /\ w3a 937    e. wcel 1727   class class class wbr 4237  (class class class)co 6110   0cc0 9021    +oocpnf 9148   RR*cxr 9150    <_ cle 9152   [,]cicc 10950
This theorem is referenced by:  ge0xaddcl  11042  ge0xmulcl  11043  xrge0subm  16770  psmetxrge0  18375  isxmet2d  18388  prdsdsf  18428  prdsxmetlem  18429  comet  18574  stdbdxmet  18576  xrge0gsumle  18895  xrge0tsms  18896  metdsf  18909  metds0  18911  metdstri  18912  metdsre  18914  metdseq0  18915  metdscnlem  18916  metnrmlem1a  18919  metnrmlem1  18920  xrhmeo  19002  lebnumlem1  19017  xrge0f  19652  itg2const2  19662  itg2uba  19664  itg2splitlem  19669  itg2split  19670  itg2monolem1  19671  itg2monolem2  19672  itg2monolem3  19673  itg2mono  19674  itg2i1fseqle  19675  itg2i1fseq3  19678  itg2addlem  19679  itg2gt0  19681  itg2cnlem2  19683  itg2cn  19684  iblss  19725  itgle  19730  itgeqa  19734  ibladdlem  19740  iblabs  19749  iblabsr  19750  iblmulc2  19751  itgsplit  19756  bddmulibl  19759  xrge00  24239  xrge0tsmsd  24254  esummono  24481  gsumesum  24482  esumsn  24487  esumpmono  24500  hashf2  24505  measge0  24592  measle0  24593  measssd  24600  measunl  24601  prob01  24702  dstrvprob  24760  itg2addnclem  26294  itg2addnc  26297  itg2gt0cn  26298  ibladdnclem  26299  iblabsnc  26307  iblmulc2nc  26308  bddiblnc  26313  ftc1anclem4  26321  ftc1anclem5  26322  ftc1anclem6  26323  ftc1anclem7  26324  ftc1anclem8  26325  ftc1anc  26326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-cnex 9077  ax-resscn 9078  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-i2m1 9089  ax-1ne0 9090  ax-rnegex 9092  ax-rrecex 9093  ax-cnre 9094
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-sbc 3168  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-id 4527  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-iota 5447  df-fun 5485  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-pnf 9153  df-mnf 9154  df-xr 9155  df-ltxr 9156  df-le 9157  df-icc 10954
  Copyright terms: Public domain W3C validator