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

Theorem rexr 8877
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 8876 . 2  |-  RR  C_  RR*
21sseli 3176 1  |-  ( A  e.  RR  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   RRcr 8736   RR*cxr 8866
This theorem is referenced by:  rexri  8884  lenlt  8901  ltpnf  10463  mnflt  10464  xrltnsym  10471  xrlttr  10474  xrre  10498  xrre3  10500  max1  10514  max2  10516  min1  10517  min2  10518  maxle  10519  lemin  10520  maxlt  10521  ltmin  10522  max0sub  10523  qbtwnxr  10527  xralrple  10532  alrple  10533  xltnegi  10543  rexadd  10559  xaddnemnf  10561  xaddnepnf  10562  xaddcom  10565  xnegdi  10568  xpncan  10571  xnpcan  10572  xleadd1a  10573  xleadd1  10575  xltadd1  10576  xltadd2  10577  xsubge0  10581  rexmul  10591  xmulid1  10599  xmulid2  10600  xmulm1  10601  xadddilem  10614  xadddir  10616  x2times  10619  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrun  10634  supxrunb1  10638  supxrunb2  10639  supxrbnd1  10640  supxrbnd2  10641  xrsup0  10642  supxrbnd  10647  elioo4g  10711  elioc2  10713  elico2  10714  elicc2  10715  iccss  10718  iooshf  10728  iooneg  10756  icoshft  10758  difreicc  10767  hashbnd  11343  elicc4abs  11803  limsupgord  11946  pcadd  12937  ramubcl  13065  lt6abl  15181  xrsmcmn  16397  xrs1mnd  16409  xrs10  16410  xrsdsreval  16416  leordtval2  16942  xmetge0  17909  imasdsf1olem  17937  bl2in  17957  blss  17972  blcld  18051  nmoid  18251  icopnfcld  18277  iocmnfcld  18278  bl2ioo  18298  blssioo  18301  xrtgioo  18312  xrsblre  18317  iccntr  18326  icccmplem2  18328  icccmp  18330  reconnlem2  18332  xrge0tsms  18339  metnrmlem1a  18362  metnrmlem1  18363  icoopnst  18437  iocopnst  18438  icopnfcnv  18440  icopnfhmeo  18441  iccpnfcnv  18442  iccpnfhmeo  18443  oprpiece1res1  18449  ovolfioo  18827  ovolicc2lem1  18876  ovolicc2lem5  18880  voliunlem3  18909  icombl1  18920  icombl  18921  iccvolcl  18924  ovolioo  18925  uniiccdif  18933  volsup2  18960  mbfimasn  18989  ismbf3d  19009  mbfsup  19019  itg2seq  19097  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq3  19112  itg2addlem  19113  itg2gt0  19115  itg2cnlem2  19117  dvlip2  19342  ply1remlem  19548  abelthlem3  19809  abelth  19817  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sinq12ge0  19876  sincos6thpi  19883  sineq0  19889  cosordlem  19893  tanord1  19899  tanord  19900  efif1olem1  19904  efif1olem2  19905  efif1o  19908  eff1o  19911  logf1o2  19997  dvlog2lem  19999  efopnlem2  20004  loglesqr  20098  isosctrlem1  20118  atantan  20219  basellem1  20318  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  pntibndlem1  20738  pntibnd  20742  pntlemc  20744  pntlemo  20756  pnt  20763  nmobndi  21353  nmopub2tALT  22489  nmfnleub2  22506  nmopun  22594  nmoptrii  22674  nmopcoi  22675  nmopcoadji  22681  pjnmopi  22728  rexdiv  23109  xdivrec  23110  xrre3FL  23251  xlt2addrd  23253  xrge0iifiso  23317  xrge0iifhom  23319  pnfneige0  23374  lmxrge0  23375  xrge0tsmsd  23382  hashf2  23452  hasheuni  23453  prob01  23616  orvcgteel  23668  orvclteel  23673  areacirclem6  24930  areacirc  24931  truni1  25505  cbci  25508  icccon2  25700  icccon4  25702  ivthALT  26258  blbnd  26511  icodiamlt  26905  rfcnpre3  27704  rfcnpre4  27705  ioovolcl  27742  stoweidlem13  27762  stoweidlem34  27783  stoweidlem52  27801  sgn1  28249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-xr 8871
  Copyright terms: Public domain W3C validator