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

Theorem rexr 9639
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
rexr  |-  ( A  e.  RR  ->  A  e.  RR* )

Proof of Theorem rexr
StepHypRef Expression
1 ressxr 9637 . 2  |-  RR  C_  RR*
21sseli 3500 1  |-  ( A  e.  RR  ->  A  e.  RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   RRcr 9491   RR*cxr 9627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-xr 9632
This theorem is referenced by:  rexri  9646  lenlt  9663  ltpnf  11331  mnflt  11333  xrltnsym  11343  xrlttr  11346  xrre  11370  xrre3  11372  max1  11386  max2  11388  min1  11389  min2  11390  maxle  11391  lemin  11392  maxlt  11393  ltmin  11394  max0sub  11395  qbtwnxr  11399  xralrple  11404  alrple  11405  xltnegi  11415  rexadd  11431  xaddnemnf  11433  xaddnepnf  11434  xaddcom  11437  xnegdi  11440  xpncan  11443  xnpcan  11444  xleadd1a  11445  xleadd1  11447  xltadd1  11448  xltadd2  11449  xsubge0  11453  rexmul  11463  xadddilem  11486  xadddir  11488  xrsupsslem  11498  xrinfmsslem  11499  xrub  11503  supxrun  11507  supxrunb1  11511  supxrunb2  11512  supxrbnd1  11513  supxrbnd2  11514  xrsup0  11515  supxrbnd  11520  elioo4g  11585  elioc2  11587  elico2  11588  elicc2  11589  iccss  11592  iooshf  11603  iooneg  11640  icoshft  11642  difreicc  11652  hashbnd  12379  sgn1  12888  elicc4abs  13115  limsupgord  13258  pcadd  14267  ramubcl  14395  lt6abl  16700  xrsmcmn  18240  xrs1mnd  18252  xrs10  18253  xrsdsreval  18259  psmetge0  20579  xmetge0  20610  imasdsf1olem  20639  bl2in  20666  blssps  20690  blss  20691  blcld  20771  icopnfcld  21038  iocmnfcld  21039  bl2ioo  21060  blssioo  21063  xrtgioo  21074  xrsblre  21079  iccntr  21089  icccmplem2  21091  icccmp  21093  reconnlem2  21095  xrge0tsms  21102  icoopnst  21202  iocopnst  21203  ovolfioo  21642  ovolicc2lem1  21691  ovolicc2lem5  21695  voliunlem3  21725  icombl1  21736  icombl  21737  iccvolcl  21740  ovolioo  21741  ioovolcl  21742  uniiccdif  21750  volsup2  21777  mbfimasn  21804  ismbf3d  21824  mbfsup  21834  itg2seq  21912  itg2monolem1  21920  itg2monolem2  21921  itg2monolem3  21922  itg2mono  21923  itg2i1fseqle  21924  itg2i1fseq3  21927  itg2addlem  21928  itg2gt0  21930  itg2cnlem2  21932  dvlip2  22159  ply1remlem  22326  abelthlem3  22590  abelth  22598  sincosq2sgn  22653  sincosq3sgn  22654  sinq12ge0  22662  sincos6thpi  22669  sineq0  22675  efif1olem1  22690  efif1olem2  22691  efif1o  22694  eff1o  22697  loglesqrt  22888  basellem1  23110  pntlemo  23548  nmobndi  25394  nmopub2tALT  26532  nmfnleub2  26549  nmopcoadji  26724  rexdiv  27318  xrge0tsmsd  27466  pnfneige0  27597  lmxrge0  27598  hashf2  27758  sxbrsigalem0  27910  orvcgteel  28074  orvclteel  28079  sgnclre  28146  sgnneg  28147  signstfvneq0  28197  mblfinlem2  29657  itg2addnc  29674  itg2gt0cn  29675  iblabsnclem  29683  bddiblnc  29690  ftc1anclem1  29695  ftc1anclem6  29700  ftc1anclem8  29702  areacirclem5  29716  areacirc  29717  ivthALT  29758  blbnd  29914  icodiamlt  30388  iocmbl  30813  ioomidp  31146  icccncfext  31254  volioc  31318  fourierdlem113  31548
  Copyright terms: Public domain W3C validator