Theorem rexrd 9689

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 9683	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sseldi 3468	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1870   RRcr 9537   RR*cxr 9673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-in 3449  df-ss 3456  df-xr 9678

This theorem is referenced by:  rpxr  11309  rpxrd  11342  max0sub  11489  qextltlem  11495  xralrple  11498  xnegcl  11506  xaddf  11517  xmulf  11558  xadddi  11581  supxrre  11613  infxrre  11622  infmxrreOLD  11626  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  ioo0  11661  ico0  11682  ioc0  11683  iooshf  11713  icoshftf1o  11753  supicc  11778  supiccub  11779  supicclub  11780  addmodid  12136  hashnnn0genn0  12523  elicc4abs  13361  caucvgrlem  13714  caucvgrlemOLD  13715  fprodge1  14027  pcxcl  14773  pcdvdsb  14781  pcaddlem  14796  ramcl2lem  14925  ramcl2lemOLD  14926  ramlb  14940  0ram  14941  prdsxmetlem  21314  xblss2ps  21347  xblss2  21348  blss2ps  21349  blss2  21350  blhalf  21351  metustto  21499  metustexhalf  21502  nmoi  21660  nmoix  21661  nmoi2  21662  nmoleub  21663  qdensere  21701  cnblcld  21706  ioo2blex  21723  tgioo  21725  blcvx  21727  zcld  21742  recld2  21743  iccntr  21750  icccmplem1  21751  reconnlem1  21755  reconnlem2  21756  opnreen  21760  metnrmlem3  21789  icoopnst  21863  cnheibor  21879  lebnumii  21890  nmoleub2lem  22021  lmnn  22126  iscau3  22141  minveclem4  22267  ivthlem1  22283  ivthlem2  22284  ivthlem3  22285  ivth2  22287  ivthle  22288  ivthle2  22289  ivthicc  22290  evthicc  22291  cniccbdd  22293  ovolgelb  22311  ovollb2lem  22319  ovolunlem1  22328  ovoliunlem1  22333  ovoliunlem2  22334  ovoliun  22336  ovolscalem1  22344  ovolicc1  22347  ovolicc2lem4  22351  ovolicc2lem5  22352  ovolicc2  22353  ovolicc  22354  nulmbl2  22367  voliunlem2  22381  ioombl1lem4  22391  ioorcl2  22401  uniioombllem1  22415  uniioombllem2a  22416  uniioombllem3  22420  dyaddisjlem  22430  dyadmaxlem  22432  opnmbllem  22436  volivth  22442  vitalilem4  22446  mbfmulc2lem  22480  mbfmax  22482  mbfposr  22485  ismbf3d  22487  mbfaddlem  22493  mbflimsup  22500  mbflimsupOLD  22501  mbfi1fseqlem4  22553  itg2lcl  22562  xrge0f  22566  itg2itg1  22571  itg2const2  22576  itg2seq  22577  itg2uba  22578  itg2lea  22579  itg2mulclem  22581  itg2mulc  22582  itg2splitlem  22583  itg2split  22584  itg2monolem2  22586  itg2monolem3  22587  itg2mono  22588  itg2gt0  22595  itg2cnlem1  22596  itg2cnlem2  22597  itg2cn  22598  iblss  22639  itgle  22644  itgeqa  22648  itgioo  22650  ibladdlem  22654  iblabs  22663  iblabsr  22664  iblmulc2  22665  itgsplit  22670  itgspliticc  22671  itgsplitioo  22672  bddmulibl  22673  ditgcl  22690  ditgswap  22691  ditgsplitlem  22692  dvferm1lem  22813  dvferm2lem  22815  dvferm  22817  rollelem  22818  rolle  22819  cmvth  22820  mvth  22821  dvlip  22822  dvlip2  22824  c1liplem1  22825  c1lip1  22826  dveq0  22829  dvgt0lem1  22831  dvivthlem1  22837  dvivth  22839  lhop1lem  22842  lhop1  22843  lhop2  22844  lhop  22845  dvcnvrelem1  22846  dvcnvre  22848  dvcvx  22849  dvfsumle  22850  dvfsumge  22851  dvfsumabs  22852  dvfsumlem2  22856  dvfsumlem3  22857  dvfsumlem4  22858  dvfsumrlimge0  22859  dvfsumrlim2  22861  ftc1lem1  22864  ftc1lem2  22865  ftc1a  22866  ftc1lem4  22868  ftc2  22873  ftc2ditglem  22874  itgparts  22876  itgsubstlem  22877  itgsubst  22878  degltlem1  22898  deg1ge  22924  coe1mul3  22925  deg1sublt  22936  deg1mul2  22940  deg1tmle  22943  deg1tm  22944  plypf1  23034  taylfvallem1  23177  tayl0  23182  pserulm  23242  psercnlem1  23245  pserdvlem1  23247  pserdvlem2  23248  abelthlem3  23253  abelth  23261  efcvx  23269  logno1  23446  logtayl  23470  xrlimcnp  23759  logfacbnd3  24014  log2sumbnd  24245  pntpbnd2  24288  pntibndlem3  24293  ttgcontlem1  24761  nvlmle  26173  nmooge0  26253  nmoub3i  26259  isblo3i  26287  ubthlem1  26357  minvecolem4  26367  nmopge0  27399  nmfnge0  27415  nmophmi  27519  branmfn  27593  xaddeq0  28173  xlt2addrd  28179  xmulcand  28228  xreceu  28229  xdivrec  28234  fsumrp0cl  28296  xrge0slmod  28446  cnre2csqlem  28555  tpr2rico  28557  xrge0iifcnv  28578  xrge0iifhom  28582  lmxrge0  28597  esumfsup  28730  esumpcvgval  28738  esumcvg  28746  dya2iocress  28935  dya2iocbrsiga  28936  dya2icobrsiga  28937  dya2icoseg  28938  dya2iocucvr  28945  sxbrsigalem2  28947  omssubaddlem  28960  omssubadd  28961  orvcgteel  29126  dstrvprob  29130  orvclteel  29131  sgnmul  29201  sgnsub  29203  sgnmulsgn  29208  sgnmulsgp  29209  signstcl  29242  signstf  29243  signstf0  29245  signstfvn  29246  signsvtn0  29247  signstfvneq0  29249  signsvfn  29259  signsvfpn  29262  signsvfnn  29263  cvmliftlem6  29801  cvmliftlem7  29802  cvmliftlem8  29803  cvmliftlem9  29804  cvmliftlem10  29805  cvmliftlem13  29807  ivthALT  30776  iooelexlt  31499  relowlssretop  31500  relowlpssretop  31501  sin2h  31639  cos2h  31640  tan2h  31641  poimirlem30  31674  poimir  31677  heicant  31679  opnmbllem0  31680  mblfinlem1  31681  mblfinlem2  31682  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  dvtanlemOLD  31695  itg2addnclem  31697  itg2addnclem2  31698  itg2gt0cn  31701  ibladdnclem  31702  iblabsnclem  31709  iblabsnc  31710  iblmulc2nc  31711  bddiblnc  31716  ftc1cnnclem  31719  ftc1anclem1  31721  ftc1anclem4  31724  ftc1anclem5  31725  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  ftc2nc  31730  areacirclem1  31736  areacirclem5  31740  areacirc  31741  isbnd3  31820  blbnd  31823  prdsbnd  31829  prdsbnd2  31831  cntotbnd  31832  idomrootle  35768  idomodle  35769  itgpowd  35798  imo72b2  36256  cvgdvgrat  36299  radcnvrat  36300  rfcnpre3  36994  rfcnpre4  36995  nnxrd  37003  lefldiveq  37115  lttri5d  37126  supxrgere  37165  supxrgelem  37169  supxrge  37170  gtnelioc  37172  ltnelicc  37179  iooabslt  37181  gtnelicc  37182  eliooshift  37189  iocopn  37206  eliccelioc  37207  iooshift  37208  icoopn  37211  fsumge0cl  37227  limciccioolb  37273  lptioo1  37284  limcicciooub  37289  ltmod  37290  lptre2pt  37292  limsupre  37293  limsupreOLD  37294  limcresiooub  37295  limcresioolb  37296  limcleqr  37297  sinaover2ne0  37315  ioccncflimc  37335  icccncfext  37337  icocncflimc  37339  cncfiooicclem1  37343  cncfiooicc  37344  cncfiooiccre  37345  cncfioobdlem  37346  dvbdfbdioolem1  37372  dvbdfbdioolem2  37373  dvbdfbdioo  37374  ioodvbdlimc1lem1  37375  ioodvbdlimc1lem2  37376  ioodvbdlimc1  37377  ioodvbdlimc2lem  37378  ioodvbdlimc2  37379  ditgeqiooicc  37406  iblsplit  37412  itgcoscmulx  37415  ibliooicc  37417  iblspltprt  37419  itgsincmulx  37420  itgsubsticc  37422  itgioocnicc  37423  iblcncfioo  37424  itgspltprt  37425  itgiccshift  37426  stoweidlem34  37464  stoweidlem52  37482  stirlinglem5  37509  dirkercncflem1  37534  dirkercncflem4  37537  fourierdlem4  37542  fourierdlem10  37548  fourierdlem19  37557  fourierdlem20  37558  fourierdlem24  37562  fourierdlem25  37563  fourierdlem26  37564  fourierdlem27  37565  fourierdlem28  37566  fourierdlem31  37569  fourierdlem32  37570  fourierdlem33  37571  fourierdlem35  37573  fourierdlem37  37575  fourierdlem40  37578  fourierdlem41  37579  fourierdlem43  37581  fourierdlem44  37582  fourierdlem46  37584  fourierdlem47  37585  fourierdlem48  37586  fourierdlem49  37587  fourierdlem50  37588  fourierdlem51  37589  fourierdlem52  37590  fourierdlem54  37592  fourierdlem57  37595  fourierdlem59  37597  fourierdlem60  37598  fourierdlem61  37599  fourierdlem62  37600  fourierdlem63  37601  fourierdlem64  37602  fourierdlem65  37603  fourierdlem68  37606  fourierdlem69  37607  fourierdlem70  37608  fourierdlem72  37610  fourierdlem73  37611  fourierdlem74  37612  fourierdlem75  37613  fourierdlem76  37614  fourierdlem78  37616  fourierdlem79  37617  fourierdlem81  37619  fourierdlem82  37620  fourierdlem84  37622  fourierdlem89  37627  fourierdlem90  37628  fourierdlem91  37629  fourierdlem92  37630  fourierdlem93  37631  fourierdlem94  37632  fourierdlem97  37635  fourierdlem100  37638  fourierdlem101  37639  fourierdlem102  37640  fourierdlem103  37641  fourierdlem104  37642  fourierdlem107  37645  fourierdlem109  37647  fourierdlem111  37649  fourierdlem112  37650  fourierdlem113  37651  fourierdlem114  37652  sqwvfoura  37660  fouriersw  37663  etransclem23  37689  etransclem46  37712  sge0cl  37757  sge0fsum  37763  sge0iunmptlemre  37791  omessre  37840  omeiunltfirp  37849  bgoldbtbnd  38303