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

Theorem rexrd 9061
Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rexrd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
rexrd  |-  ( ph  ->  A  e.  RR* )

Proof of Theorem rexrd
StepHypRef Expression
1 ressxr 9056 . 2  |-  RR  C_  RR*
2 rexrd.1 . 2  |-  ( ph  ->  A  e.  RR )
31, 2sseldi 3283 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   RRcr 8916   RR*cxr 9046
This theorem is referenced by:  rpxr  10545  rpxrd  10575  max0sub  10708  qextltlem  10714  xralrple  10717  xnegcl  10725  xaddf  10736  xmulf  10777  xadddi  10800  supxrre  10832  infmxrre  10840  ixxub  10863  ixxlb  10864  ioo0  10867  ico0  10888  ioc0  10889  iooshf  10915  icoshftf1o  10946  hashnnn0genn0  11548  elicc4abs  12044  caucvgrlem  12387  pcxcl  13155  pcdvdsb  13163  pcaddlem  13178  ramcl2lem  13298  ramlb  13308  0ram  13309  prdsxmetlem  18300  xblss2  18326  blss2  18327  blhalf  18328  metustto  18467  metustexhalf  18470  nmoi  18627  nmoix  18628  nmoi2  18629  nmoleub  18630  qdensere  18669  cnblcld  18674  ioo2blex  18690  tgioo  18692  blcvx  18694  zcld  18709  recld2  18710  iccntr  18717  icccmplem1  18718  reconnlem1  18722  reconnlem2  18723  opnreen  18727  metnrmlem3  18756  cnheibor  18845  lebnumii  18856  nmoleub2lem  18987  lmnn  19081  iscau3  19096  minveclem4  19194  ivthlem1  19209  ivthlem2  19210  ivthlem3  19211  ivth2  19213  ivthle  19214  ivthle2  19215  ivthicc  19216  evthicc  19217  cniccbdd  19219  ovolgelb  19237  ovollb2lem  19245  ovolunlem1  19254  ovoliunlem1  19259  ovoliunlem2  19260  ovoliun  19262  ovolscalem1  19270  ovolicc1  19273  ovolicc2lem4  19277  ovolicc2lem5  19278  ovolicc2  19279  ovolicc  19280  nulmbl2  19292  voliunlem2  19306  ioombl1lem4  19316  ioorcl2  19325  uniioombllem1  19334  uniioombllem2a  19335  uniioombllem3  19338  dyaddisjlem  19348  dyadmaxlem  19350  opnmbllem  19354  volivth  19360  vitalilem4  19364  mbfmulc2lem  19400  mbfmax  19402  mbfposr  19405  ismbf3d  19407  mbfaddlem  19413  mbflimsup  19419  mbfi1fseqlem4  19471  itg2lcl  19480  xrge0f  19484  itg2itg1  19489  itg2const2  19494  itg2seq  19495  itg2uba  19496  itg2lea  19497  itg2mulclem  19499  itg2mulc  19500  itg2splitlem  19501  itg2split  19502  itg2monolem2  19504  itg2monolem3  19505  itg2mono  19506  itg2gt0  19513  itg2cnlem1  19514  itg2cnlem2  19515  itg2cn  19516  iblss  19557  itgle  19562  itgeqa  19566  itgioo  19568  ibladdlem  19572  iblabs  19581  iblabsr  19582  iblmulc2  19583  itgsplit  19588  itgspliticc  19589  itgsplitioo  19590  bddmulibl  19591  ditgcl  19606  ditgswap  19607  ditgsplitlem  19608  dvferm1lem  19729  dvferm2lem  19731  dvferm  19733  rollelem  19734  rolle  19735  cmvth  19736  mvth  19737  dvlip  19738  dvlip2  19740  c1liplem1  19741  c1lip1  19742  dveq0  19745  dvgt0lem1  19747  dvivthlem1  19753  dvivth  19755  lhop1lem  19758  lhop1  19759  lhop2  19760  lhop  19761  dvcnvrelem1  19762  dvcnvre  19764  dvcvx  19765  dvfsumle  19766  dvfsumge  19767  dvfsumabs  19768  dvfsumlem2  19772  dvfsumlem3  19773  dvfsumlem4  19774  dvfsumrlimge0  19775  dvfsumrlim2  19777  ftc1lem1  19780  ftc1lem2  19781  ftc1a  19782  ftc1lem4  19784  ftc2  19789  ftc2ditglem  19790  itgparts  19792  itgsubstlem  19793  itgsubst  19794  degltlem1  19856  deg1ge  19882  coe1mul3  19883  deg1sublt  19894  deg1mul2  19898  deg1tmle  19901  deg1tm  19902  plypf1  19992  taylfvallem1  20134  tayl0  20139  pserulm  20199  psercnlem1  20202  pserdvlem1  20204  pserdvlem2  20205  abelthlem3  20210  abelth  20218  efcvx  20226  logno1  20388  logtayl  20412  xrlimcnp  20668  logfacbnd3  20868  log2sumbnd  21099  pntpbnd2  21142  pntibndlem3  21147  nvlmle  22030  nmooge0  22110  nmoub3i  22116  isblo3i  22144  ubthlem1  22214  minvecolem4  22224  nmopge0  23256  nmfnge0  23272  nmophmi  23376  branmfn  23450  xlt2addrd  23954  xmulcand  23999  xreceu  24000  xdivrec  24005  xaddeq0  24024  fsumrp0cl  24040  cnre2csqlem  24106  tpr2rico  24108  xrge0iifcnv  24117  xrge0iifhom  24121  lmxrge0  24135  esumfsup  24250  esumpcvgval  24258  esumcvg  24266  dya2iocress  24412  dya2iocbrsiga  24413  dya2icobrsiga  24414  dya2icoseg  24415  dya2iocucvr  24422  sxbrsigalem2  24424  orvcgteel  24498  dstrvprob  24502  orvclteel  24503  cvmliftlem6  24750  cvmliftlem7  24751  cvmliftlem8  24752  cvmliftlem9  24753  cvmliftlem10  24754  cvmliftlem13  24756  itg2addnclem  25951  itg2addnclem2  25952  itg2gt0cn  25954  ibladdnclem  25955  iblabsnclem  25962  iblabsnc  25963  iblmulc2nc  25964  bddiblnc  25969  ftc1cnnclem  25972  areacirclem2  25976  areacirclem3  25977  areacirclem6  25981  areacirc  25982  ivthALT  26023  isbnd3  26178  blbnd  26181  prdsbnd  26187  prdsbnd2  26189  cntotbnd  26190  idomrootle  27174  idomodle  27175  rfcnpre3  27366  rfcnpre4  27367  stoweidlem34  27445  stoweidlem52  27463  stirlinglem5  27489
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-v 2895  df-un 3262  df-in 3264  df-ss 3271  df-xr 9051
  Copyright terms: Public domain W3C validator