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

Theorem rexrd 9127
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 9122 . 2  |-  RR  C_  RR*
2 rexrd.1 . 2  |-  ( ph  ->  A  e.  RR )
31, 2sseldi 3339 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   RRcr 8982   RR*cxr 9112
This theorem is referenced by:  rpxr  10612  rpxrd  10642  max0sub  10775  qextltlem  10781  xralrple  10784  xnegcl  10792  xaddf  10803  xmulf  10844  xadddi  10867  supxrre  10899  infmxrre  10907  ixxub  10930  ixxlb  10931  ioo0  10934  ico0  10955  ioc0  10956  iooshf  10982  icoshftf1o  11013  hashnnn0genn0  11620  elicc4abs  12116  caucvgrlem  12459  pcxcl  13227  pcdvdsb  13235  pcaddlem  13250  ramcl2lem  13370  ramlb  13380  0ram  13381  prdsxmetlem  18391  xblss2ps  18424  xblss2  18425  blss2ps  18426  blss2  18427  blhalf  18428  metusttoOLD  18580  metustto  18581  metustexhalfOLD  18586  metustexhalf  18587  nmoi  18755  nmoix  18756  nmoi2  18757  nmoleub  18758  qdensere  18797  cnblcld  18802  ioo2blex  18818  tgioo  18820  blcvx  18822  zcld  18837  recld2  18838  iccntr  18845  icccmplem1  18846  reconnlem1  18850  reconnlem2  18851  opnreen  18855  metnrmlem3  18884  cnheibor  18973  lebnumii  18984  nmoleub2lem  19115  lmnn  19209  iscau3  19224  minveclem4  19326  ivthlem1  19341  ivthlem2  19342  ivthlem3  19343  ivth2  19345  ivthle  19346  ivthle2  19347  ivthicc  19348  evthicc  19349  cniccbdd  19351  ovolgelb  19369  ovollb2lem  19377  ovolunlem1  19386  ovoliunlem1  19391  ovoliunlem2  19392  ovoliun  19394  ovolscalem1  19402  ovolicc1  19405  ovolicc2lem4  19409  ovolicc2lem5  19410  ovolicc2  19411  ovolicc  19412  nulmbl2  19424  voliunlem2  19438  ioombl1lem4  19448  ioorcl2  19457  uniioombllem1  19466  uniioombllem2a  19467  uniioombllem3  19470  dyaddisjlem  19480  dyadmaxlem  19482  opnmbllem  19486  volivth  19492  vitalilem4  19496  mbfmulc2lem  19532  mbfmax  19534  mbfposr  19537  ismbf3d  19539  mbfaddlem  19545  mbflimsup  19551  mbfi1fseqlem4  19603  itg2lcl  19612  xrge0f  19616  itg2itg1  19621  itg2const2  19626  itg2seq  19627  itg2uba  19628  itg2lea  19629  itg2mulclem  19631  itg2mulc  19632  itg2splitlem  19633  itg2split  19634  itg2monolem2  19636  itg2monolem3  19637  itg2mono  19638  itg2gt0  19645  itg2cnlem1  19646  itg2cnlem2  19647  itg2cn  19648  iblss  19689  itgle  19694  itgeqa  19698  itgioo  19700  ibladdlem  19704  iblabs  19713  iblabsr  19714  iblmulc2  19715  itgsplit  19720  itgspliticc  19721  itgsplitioo  19722  bddmulibl  19723  ditgcl  19738  ditgswap  19739  ditgsplitlem  19740  dvferm1lem  19861  dvferm2lem  19863  dvferm  19865  rollelem  19866  rolle  19867  cmvth  19868  mvth  19869  dvlip  19870  dvlip2  19872  c1liplem1  19873  c1lip1  19874  dveq0  19877  dvgt0lem1  19879  dvivthlem1  19885  dvivth  19887  lhop1lem  19890  lhop1  19891  lhop2  19892  lhop  19893  dvcnvrelem1  19894  dvcnvre  19896  dvcvx  19897  dvfsumle  19898  dvfsumge  19899  dvfsumabs  19900  dvfsumlem2  19904  dvfsumlem3  19905  dvfsumlem4  19906  dvfsumrlimge0  19907  dvfsumrlim2  19909  ftc1lem1  19912  ftc1lem2  19913  ftc1a  19914  ftc1lem4  19916  ftc2  19921  ftc2ditglem  19922  itgparts  19924  itgsubstlem  19925  itgsubst  19926  degltlem1  19988  deg1ge  20014  coe1mul3  20015  deg1sublt  20026  deg1mul2  20030  deg1tmle  20033  deg1tm  20034  plypf1  20124  taylfvallem1  20266  tayl0  20271  pserulm  20331  psercnlem1  20334  pserdvlem1  20336  pserdvlem2  20337  abelthlem3  20342  abelth  20350  efcvx  20358  logno1  20520  logtayl  20544  xrlimcnp  20800  logfacbnd3  21000  log2sumbnd  21231  pntpbnd2  21274  pntibndlem3  21279  nvlmle  22181  nmooge0  22261  nmoub3i  22267  isblo3i  22295  ubthlem1  22365  minvecolem4  22375  nmopge0  23407  nmfnge0  23423  nmophmi  23527  branmfn  23601  xaddeq0  24112  xlt2addrd  24117  xmulcand  24160  xreceu  24161  xdivrec  24166  fsumrp0cl  24210  cnre2csqlem  24301  tpr2rico  24303  xrge0iifcnv  24312  xrge0iifhom  24316  lmxrge0  24330  esumfsup  24453  esumpcvgval  24461  esumcvg  24469  dya2iocress  24617  dya2iocbrsiga  24618  dya2icobrsiga  24619  dya2icoseg  24620  dya2iocucvr  24627  sxbrsigalem2  24629  orvcgteel  24718  dstrvprob  24722  orvclteel  24723  cvmliftlem6  24970  cvmliftlem7  24971  cvmliftlem8  24972  cvmliftlem9  24973  cvmliftlem10  24974  cvmliftlem13  24976  mblfinlem  26235  mblfinlem2  26236  mblfinlem3  26237  ismblfin  26238  itg2addnclem  26247  itg2addnclem2  26248  itg2gt0cn  26251  ibladdnclem  26252  iblabsnclem  26259  iblabsnc  26260  iblmulc2nc  26261  bddiblnc  26266  ftc1cnnclem  26269  ftc1anclem1  26271  ftc1anclem4  26274  ftc1anclem5  26275  ftc1anclem6  26276  ftc1anclem7  26277  ftc1anclem8  26278  ftc1anc  26279  ftc2nc  26280  areacirclem2  26283  areacirclem3  26284  areacirclem6  26288  areacirc  26289  ivthALT  26330  isbnd3  26485  blbnd  26488  prdsbnd  26494  prdsbnd2  26496  cntotbnd  26497  idomrootle  27480  idomodle  27481  rfcnpre3  27672  rfcnpre4  27673  stoweidlem34  27751  stoweidlem52  27769  stirlinglem5  27795
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-un 3318  df-in 3320  df-ss 3327  df-xr 9117
  Copyright terms: Public domain W3C validator