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

Theorem rexr 8893
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 8892 . 2  |-  RR  C_  RR*
21sseli 3189 1  |-  ( A  e.  RR  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   RRcr 8752   RR*cxr 8882
This theorem is referenced by:  rexri  8900  lenlt  8917  ltpnf  10479  mnflt  10480  xrltnsym  10487  xrlttr  10490  xrre  10514  xrre3  10516  max1  10530  max2  10532  min1  10533  min2  10534  maxle  10535  lemin  10536  maxlt  10537  ltmin  10538  max0sub  10539  qbtwnxr  10543  xralrple  10548  alrple  10549  xltnegi  10559  rexadd  10575  xaddnemnf  10577  xaddnepnf  10578  xaddcom  10581  xnegdi  10584  xpncan  10587  xnpcan  10588  xleadd1a  10589  xleadd1  10591  xltadd1  10592  xltadd2  10593  xsubge0  10597  rexmul  10607  xmulid1  10615  xmulid2  10616  xmulm1  10617  xadddilem  10630  xadddir  10632  x2times  10635  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrun  10650  supxrunb1  10654  supxrunb2  10655  supxrbnd1  10656  supxrbnd2  10657  xrsup0  10658  supxrbnd  10663  elioo4g  10727  elioc2  10729  elico2  10730  elicc2  10731  iccss  10734  iooshf  10744  iooneg  10772  icoshft  10774  difreicc  10783  hashbnd  11359  elicc4abs  11819  limsupgord  11962  pcadd  12953  ramubcl  13081  lt6abl  15197  xrsmcmn  16413  xrs1mnd  16425  xrs10  16426  xrsdsreval  16432  leordtval2  16958  xmetge0  17925  imasdsf1olem  17953  bl2in  17973  blss  17988  blcld  18067  nmoid  18267  icopnfcld  18293  iocmnfcld  18294  bl2ioo  18314  blssioo  18317  xrtgioo  18328  xrsblre  18333  iccntr  18342  icccmplem2  18344  icccmp  18346  reconnlem2  18348  xrge0tsms  18355  metnrmlem1a  18378  metnrmlem1  18379  icoopnst  18453  iocopnst  18454  icopnfcnv  18456  icopnfhmeo  18457  iccpnfcnv  18458  iccpnfhmeo  18459  oprpiece1res1  18465  ovolfioo  18843  ovolicc2lem1  18892  ovolicc2lem5  18896  voliunlem3  18925  icombl1  18936  icombl  18937  iccvolcl  18940  ovolioo  18941  uniiccdif  18949  volsup2  18976  mbfimasn  19005  ismbf3d  19025  mbfsup  19035  itg2seq  19113  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq3  19128  itg2addlem  19129  itg2gt0  19131  itg2cnlem2  19133  dvlip2  19358  ply1remlem  19564  abelthlem3  19825  abelth  19833  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sinq12ge0  19892  sincos6thpi  19899  sineq0  19905  cosordlem  19909  tanord1  19915  tanord  19916  efif1olem1  19920  efif1olem2  19921  efif1o  19924  eff1o  19927  logf1o2  20013  dvlog2lem  20015  efopnlem2  20020  loglesqr  20114  isosctrlem1  20134  atantan  20235  basellem1  20334  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  pntibndlem1  20754  pntibnd  20758  pntlemc  20760  pntlemo  20772  pnt  20779  nmobndi  21369  nmopub2tALT  22505  nmfnleub2  22522  nmopun  22610  nmoptrii  22690  nmopcoi  22691  nmopcoadji  22697  pjnmopi  22744  rexdiv  23125  xdivrec  23126  xrre3FL  23266  xlt2addrd  23268  xrge0iifiso  23332  xrge0iifhom  23334  pnfneige0  23389  lmxrge0  23390  xrge0tsmsd  23397  hashf2  23467  hasheuni  23468  prob01  23631  orvcgteel  23683  orvclteel  23688  itg2gt0cn  25005  iblabsnclem  25013  bddiblnc  25020  areacirclem6  25032  areacirc  25033  truni1  25607  cbci  25610  icccon2  25802  icccon4  25804  ivthALT  26360  blbnd  26613  icodiamlt  27007  rfcnpre3  27806  rfcnpre4  27807  ioovolcl  27844  stoweidlem13  27864  stoweidlem34  27885  stoweidlem52  27903  sgn1  28502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-xr 8887
  Copyright terms: Public domain W3C validator