Theorem rexrd 9090

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

Step	Hyp	Ref	Expression
1		ressxr 9085	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sseldi 3306	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1721   RRcr 8945   RR*cxr 9075

This theorem is referenced by:  rpxr  10575  rpxrd  10605  max0sub  10738  qextltlem  10744  xralrple  10747  xnegcl  10755  xaddf  10766  xmulf  10807  xadddi  10830  supxrre  10862  infmxrre  10870  ixxub  10893  ixxlb  10894  ioo0  10897  ico0  10918  ioc0  10919  iooshf  10945  icoshftf1o  10976  hashnnn0genn0  11582  elicc4abs  12078  caucvgrlem  12421  pcxcl  13189  pcdvdsb  13197  pcaddlem  13212  ramcl2lem  13332  ramlb  13342  0ram  13343  prdsxmetlem  18351  xblss2ps  18384  xblss2  18385  blss2ps  18386  blss2  18387  blhalf  18388  metusttoOLD  18540  metustto  18541  metustexhalfOLD  18546  metustexhalf  18547  nmoi  18715  nmoix  18716  nmoi2  18717  nmoleub  18718  qdensere  18757  cnblcld  18762  ioo2blex  18778  tgioo  18780  blcvx  18782  zcld  18797  recld2  18798  iccntr  18805  icccmplem1  18806  reconnlem1  18810  reconnlem2  18811  opnreen  18815  metnrmlem3  18844  cnheibor  18933  lebnumii  18944  nmoleub2lem  19075  lmnn  19169  iscau3  19184  minveclem4  19286  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  ivth2  19305  ivthle  19306  ivthle2  19307  ivthicc  19308  evthicc  19309  cniccbdd  19311  ovolgelb  19329  ovollb2lem  19337  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun  19354  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem4  19369  ovolicc2lem5  19370  ovolicc2  19371  ovolicc  19372  nulmbl2  19384  voliunlem2  19398  ioombl1lem4  19408  ioorcl2  19417  uniioombllem1  19426  uniioombllem2a  19427  uniioombllem3  19430  dyaddisjlem  19440  dyadmaxlem  19442  opnmbllem  19446  volivth  19452  vitalilem4  19456  mbfmulc2lem  19492  mbfmax  19494  mbfposr  19497  ismbf3d  19499  mbfaddlem  19505  mbflimsup  19511  mbfi1fseqlem4  19563  itg2lcl  19572  xrge0f  19576  itg2itg1  19581  itg2const2  19586  itg2seq  19587  itg2uba  19588  itg2lea  19589  itg2mulclem  19591  itg2mulc  19592  itg2splitlem  19593  itg2split  19594  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  iblss  19649  itgle  19654  itgeqa  19658  itgioo  19660  ibladdlem  19664  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgsplit  19680  itgspliticc  19681  itgsplitioo  19682  bddmulibl  19683  ditgcl  19698  ditgswap  19699  ditgsplitlem  19700  dvferm1lem  19821  dvferm2lem  19823  dvferm  19825  rollelem  19826  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlip2  19832  c1liplem1  19833  c1lip1  19834  dveq0  19837  dvgt0lem1  19839  dvivthlem1  19845  dvivth  19847  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvcnvrelem1  19854  dvcnvre  19856  dvcvx  19857  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlimge0  19867  dvfsumrlim2  19869  ftc1lem1  19872  ftc1lem2  19873  ftc1a  19874  ftc1lem4  19876  ftc2  19881  ftc2ditglem  19882  itgparts  19884  itgsubstlem  19885  itgsubst  19886  degltlem1  19948  deg1ge  19974  coe1mul3  19975  deg1sublt  19986  deg1mul2  19990  deg1tmle  19993  deg1tm  19994  plypf1  20084  taylfvallem1  20226  tayl0  20231  pserulm  20291  psercnlem1  20294  pserdvlem1  20296  pserdvlem2  20297  abelthlem3  20302  abelth  20310  efcvx  20318  logno1  20480  logtayl  20504  xrlimcnp  20760  logfacbnd3  20960  log2sumbnd  21191  pntpbnd2  21234  pntibndlem3  21239  nvlmle  22141  nmooge0  22221  nmoub3i  22227  isblo3i  22255  ubthlem1  22325  minvecolem4  22335  nmopge0  23367  nmfnge0  23383  nmophmi  23487  branmfn  23561  xaddeq0  24072  xlt2addrd  24077  xmulcand  24120  xreceu  24121  xdivrec  24126  fsumrp0cl  24170  cnre2csqlem  24261  tpr2rico  24263  xrge0iifcnv  24272  xrge0iifhom  24276  lmxrge0  24290  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  dya2iocress  24577  dya2iocbrsiga  24578  dya2icobrsiga  24579  dya2icoseg  24580  dya2iocucvr  24587  sxbrsigalem2  24589  orvcgteel  24678  dstrvprob  24682  orvclteel  24683  cvmliftlem6  24930  cvmliftlem7  24931  cvmliftlem8  24932  cvmliftlem9  24933  cvmliftlem10  24934  cvmliftlem13  24936  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnclem2  26156  itg2gt0cn  26159  ibladdnclem  26160  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  bddiblnc  26174  ftc1cnnclem  26177  areacirclem2  26181  areacirclem3  26182  areacirclem6  26186  areacirc  26187  ivthALT  26228  isbnd3  26383  blbnd  26386  prdsbnd  26392  prdsbnd2  26394  cntotbnd  26395  idomrootle  27379  idomodle  27380  rfcnpre3  27571  rfcnpre4  27572  stoweidlem34  27650  stoweidlem52  27668  stirlinglem5  27694

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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294  df-xr 9080