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

Theorem rexrd 8897
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 8892 . 2  |-  RR  C_  RR*
2 rexrd.1 . 2  |-  ( ph  ->  A  e.  RR )
31, 2sseldi 3191 1  |-  ( ph  ->  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:  rpxr  10377  rpxrd  10407  max0sub  10539  qextltlem  10545  xralrple  10548  xnegcl  10556  xaddf  10567  xmulf  10608  xadddi  10631  supxrre  10662  infmxrre  10670  ixxub  10693  ixxlb  10694  ioo0  10697  ico0  10718  ioc0  10719  iooshf  10744  icoshftf1o  10775  elicc4abs  11819  caucvgrlem  12161  pcxcl  12929  pcdvdsb  12937  pcaddlem  12952  ramcl2lem  13072  ramlb  13082  0ram  13083  prdsxmetlem  17948  xblss2  17974  blss2  17975  blhalf  17976  nmoi  18253  nmoix  18254  nmoi2  18255  nmoleub  18256  qdensere  18295  cnblcld  18300  ioo2blex  18316  tgioo  18318  blcvx  18320  zcld  18335  recld2  18336  iccntr  18342  icccmplem1  18343  reconnlem1  18347  reconnlem2  18348  opnreen  18352  metnrmlem3  18381  cnheibor  18469  lebnumii  18480  nmoleub2lem  18611  lmnn  18705  iscau3  18720  minveclem4  18812  ivthlem1  18827  ivthlem2  18828  ivthlem3  18829  ivth2  18831  ivthle  18832  ivthle2  18833  ivthicc  18834  evthicc  18835  cniccbdd  18837  ovolgelb  18855  ovollb2lem  18863  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovoliun  18880  ovolscalem1  18888  ovolicc1  18891  ovolicc2lem4  18895  ovolicc2lem5  18896  ovolicc2  18897  ovolicc  18898  nulmbl2  18910  voliunlem2  18924  ioombl1lem4  18934  ioorcl2  18943  uniioombllem1  18952  uniioombllem2a  18953  uniioombllem3  18956  dyaddisjlem  18966  dyadmaxlem  18968  opnmbllem  18972  volivth  18978  vitalilem4  18982  mbfmulc2lem  19018  mbfmax  19020  mbfposr  19023  ismbf3d  19025  mbfaddlem  19031  mbflimsup  19037  mbfi1fseqlem4  19089  itg2lcl  19098  xrge0f  19102  itg2itg1  19107  itg2const2  19112  itg2seq  19113  itg2uba  19114  itg2lea  19115  itg2mulclem  19117  itg2mulc  19118  itg2splitlem  19119  itg2split  19120  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  iblss  19175  itgle  19180  itgeqa  19184  itgioo  19186  ibladdlem  19190  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgsplit  19206  itgspliticc  19207  itgsplitioo  19208  bddmulibl  19209  ditgcl  19224  ditgswap  19225  ditgsplitlem  19226  dvferm1lem  19347  dvferm2lem  19349  dvferm  19351  rollelem  19352  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlip2  19358  c1liplem1  19359  c1lip1  19360  dveq0  19363  dvgt0lem1  19365  dvivthlem1  19371  dvivth  19373  lhop1lem  19376  lhop1  19377  lhop2  19378  lhop  19379  dvcnvrelem1  19380  dvcnvre  19382  dvcvx  19383  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlimge0  19393  dvfsumrlim2  19395  ftc1lem1  19398  ftc1lem2  19399  ftc1a  19400  ftc1lem4  19402  ftc2  19407  ftc2ditglem  19408  itgparts  19410  itgsubstlem  19411  itgsubst  19412  degltlem1  19474  deg1ge  19500  coe1mul3  19501  deg1sublt  19512  deg1mul2  19516  deg1tmle  19519  deg1tm  19520  plypf1  19610  taylfvallem1  19752  tayl0  19757  pserulm  19814  psercnlem1  19817  pserdvlem1  19819  pserdvlem2  19820  abelthlem3  19825  abelth  19833  efcvx  19841  logno1  19999  logtayl  20023  xrlimcnp  20279  logfacbnd3  20478  log2sumbnd  20709  pntpbnd2  20752  pntibndlem3  20757  nvlmle  21281  nmooge0  21361  nmoub3i  21367  isblo3i  21395  ubthlem1  21465  minvecolem4  21475  nmopge0  22507  nmfnge0  22523  nmophmi  22627  branmfn  22701  xmulcand  23120  xreceu  23121  xdivrec  23126  xlt2addrd  23268  cnre2csqlem  23309  cnre2csqima  23310  tpr2rico  23311  xaddeq0  23319  xrge0iifhom  23334  fsumrp0cl  23349  lmxrge0  23390  esumpcvgval  23461  esumcvg  23469  dya2iocress  23592  dya2iocbrsiga  23593  dya2iocseg  23594  orvcgteel  23683  orvclteel  23688  cvmliftlem6  23836  cvmliftlem7  23837  cvmliftlem8  23838  cvmliftlem9  23839  cvmliftlem10  23840  cvmliftlem13  23842  itg2addnclem  25003  itg2addnclem2  25004  itg2gt0cn  25006  ibladdnclem  25007  iblabsnclem  25014  iblabsnc  25015  iblmulc2nc  25016  bddiblnc  25021  ftc1cnnclem  25024  areacirclem2  25028  areacirclem3  25029  areacirclem6  25033  areacirc  25034  truni1  25608  truni3  25610  cbci  25611  iintlem1  25713  icccon3  25804  ivthALT  26361  isbnd3  26611  blbnd  26614  prdsbnd  26620  prdsbnd2  26622  cntotbnd  26623  idomrootle  27614  idomodle  27615  stirlinglem5  27930
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