Theorem rexrd 9643

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

Syntax hints:   -> wi 4   e. wcel 1767   RRcr 9491   RR*cxr 9627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-xr 9632

This theorem is referenced by:  rpxr  11227  rpxrd  11257  max0sub  11395  qextltlem  11401  xralrple  11404  xnegcl  11412  xaddf  11423  xmulf  11464  xadddi  11487  supxrre  11519  infmxrre  11527  ixxub  11550  ixxlb  11551  ioo0  11554  ico0  11575  ioc0  11576  iooshf  11603  icoshftf1o  11643  supicc  11668  supiccub  11669  supicclub  11670  hashnnn0genn0  12384  elicc4abs  13115  caucvgrlem  13458  pcxcl  14243  pcdvdsb  14251  pcaddlem  14266  ramcl2lem  14386  ramlb  14396  0ram  14397  prdsxmetlem  20634  xblss2ps  20667  xblss2  20668  blss2ps  20669  blss2  20670  blhalf  20671  metusttoOLD  20823  metustto  20824  metustexhalfOLD  20829  metustexhalf  20830  nmoi  20998  nmoix  20999  nmoi2  21000  nmoleub  21001  qdensere  21040  cnblcld  21045  ioo2blex  21062  tgioo  21064  blcvx  21066  zcld  21081  recld2  21082  iccntr  21089  icccmplem1  21090  reconnlem1  21094  reconnlem2  21095  opnreen  21099  metnrmlem3  21128  cnheibor  21218  lebnumii  21229  nmoleub2lem  21360  lmnn  21465  iscau3  21480  minveclem4  21610  ivthlem1  21626  ivthlem2  21627  ivthlem3  21628  ivth2  21630  ivthle  21631  ivthle2  21632  ivthicc  21633  evthicc  21634  cniccbdd  21636  ovolgelb  21654  ovollb2lem  21662  ovolunlem1  21671  ovoliunlem1  21676  ovoliunlem2  21677  ovoliun  21679  ovolscalem1  21687  ovolicc1  21690  ovolicc2lem4  21694  ovolicc2lem5  21695  ovolicc2  21696  ovolicc  21697  nulmbl2  21710  voliunlem2  21724  ioombl1lem4  21734  ioorcl2  21744  uniioombllem1  21753  uniioombllem2a  21754  uniioombllem3  21757  dyaddisjlem  21767  dyadmaxlem  21769  opnmbllem  21773  volivth  21779  vitalilem4  21783  mbfmulc2lem  21817  mbfmax  21819  mbfposr  21822  ismbf3d  21824  mbfaddlem  21830  mbflimsup  21836  mbfi1fseqlem4  21888  itg2lcl  21897  xrge0f  21901  itg2itg1  21906  itg2const2  21911  itg2seq  21912  itg2uba  21913  itg2lea  21914  itg2mulclem  21916  itg2mulc  21917  itg2splitlem  21918  itg2split  21919  itg2monolem2  21921  itg2monolem3  21922  itg2mono  21923  itg2gt0  21930  itg2cnlem1  21931  itg2cnlem2  21932  itg2cn  21933  iblss  21974  itgle  21979  itgeqa  21983  itgioo  21985  ibladdlem  21989  iblabs  21998  iblabsr  21999  iblmulc2  22000  itgsplit  22005  itgspliticc  22006  itgsplitioo  22007  bddmulibl  22008  ditgcl  22025  ditgswap  22026  ditgsplitlem  22027  dvferm1lem  22148  dvferm2lem  22150  dvferm  22152  rollelem  22153  rolle  22154  cmvth  22155  mvth  22156  dvlip  22157  dvlip2  22159  c1liplem1  22160  c1lip1  22161  dveq0  22164  dvgt0lem1  22166  dvivthlem1  22172  dvivth  22174  lhop1lem  22177  lhop1  22178  lhop2  22179  lhop  22180  dvcnvrelem1  22181  dvcnvre  22183  dvcvx  22184  dvfsumle  22185  dvfsumge  22186  dvfsumabs  22187  dvfsumlem2  22191  dvfsumlem3  22192  dvfsumlem4  22193  dvfsumrlimge0  22194  dvfsumrlim2  22196  ftc1lem1  22199  ftc1lem2  22200  ftc1a  22201  ftc1lem4  22203  ftc2  22208  ftc2ditglem  22209  itgparts  22211  itgsubstlem  22212  itgsubst  22213  degltlem1  22235  deg1ge  22262  coe1mul3  22263  deg1sublt  22274  deg1mul2  22278  deg1tmle  22281  deg1tm  22282  plypf1  22372  taylfvallem1  22514  tayl0  22519  pserulm  22579  psercnlem1  22582  pserdvlem1  22584  pserdvlem2  22585  abelthlem3  22590  abelth  22598  efcvx  22606  logno1  22773  logtayl  22797  xrlimcnp  23054  logfacbnd3  23254  log2sumbnd  23485  pntpbnd2  23528  pntibndlem3  23533  ttgcontlem1  23892  nvlmle  25306  nmooge0  25386  nmoub3i  25392  isblo3i  25420  ubthlem1  25490  minvecolem4  25500  nmopge0  26534  nmfnge0  26550  nmophmi  26654  branmfn  26728  xaddeq0  27269  xlt2addrd  27274  xmulcand  27313  xreceu  27314  xdivrec  27319  fsumrp0cl  27375  xrge0slmod  27525  cnre2csqlem  27556  tpr2rico  27558  xrge0iifcnv  27579  xrge0iifhom  27583  lmxrge0  27598  esumfsup  27744  esumpcvgval  27752  esumcvg  27760  dya2iocress  27913  dya2iocbrsiga  27914  dya2icobrsiga  27915  dya2icoseg  27916  dya2iocucvr  27923  sxbrsigalem2  27925  orvcgteel  28074  dstrvprob  28078  orvclteel  28079  sgnmul  28149  sgnmulrp2  28150  sgnsub  28151  sgnmulsgn  28156  sgnmulsgp  28157  signstcl  28190  signstf  28191  signstf0  28193  signstfvn  28194  signsvtn0  28195  signstfvneq0  28197  signsvfn  28207  signsvfpn  28210  signsvfnn  28211  cvmliftlem6  28403  cvmliftlem7  28404  cvmliftlem8  28405  cvmliftlem9  28406  cvmliftlem10  28407  cvmliftlem13  28409  sin2h  29650  cos2h  29651  tan2h  29652  heicant  29654  opnmbllem0  29655  mblfinlem1  29656  mblfinlem2  29657  mblfinlem3  29658  mblfinlem4  29659  ismblfin  29660  dvtanlem  29669  itg2addnclem  29671  itg2addnclem2  29672  itg2gt0cn  29675  ibladdnclem  29676  iblabsnclem  29683  iblabsnc  29684  iblmulc2nc  29685  bddiblnc  29690  ftc1cnnclem  29693  ftc1anclem1  29695  ftc1anclem4  29698  ftc1anclem5  29699  ftc1anclem6  29700  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703  ftc2nc  29704  areacirclem1  29712  areacirclem5  29716  areacirc  29717  ivthALT  29758  isbnd3  29911  blbnd  29914  prdsbnd  29920  prdsbnd2  29922  cntotbnd  29923  idomrootle  30785  idomodle  30786  itgpowd  30815  rfcnpre3  31014  rfcnpre4  31015  nnxrd  31025  lefldiveq  31087  lttri5d  31104  gtnelioc  31115  ltnelicc  31122  iooabslt  31124  gtnelicc  31125  eliooshift  31133  iocopn  31152  eliccelioc  31153  iooshift  31154  icoopn  31157  limciccioolb  31191  lptioo1  31202  limcicciooub  31207  ltmod  31208  lptre2pt  31210  limsupre  31211  limcresiooub  31212  limcresioolb  31213  limcleqr  31214  sinaover2ne0  31232  ioccncflimc  31252  icccncfext  31254  icocncflimc  31256  cncfiooicclem1  31260  cncfiooicc  31261  cncfiooiccre  31262  cncfioobdlem  31263  dvbdfbdioolem1  31286  dvbdfbdioolem2  31287  dvbdfbdioo  31288  ioodvbdlimc1lem1  31289  ioodvbdlimc1lem2  31290  ioodvbdlimc1  31291  ioodvbdlimc2lem  31292  ioodvbdlimc2  31293  ditgeqiooicc  31306  iblsplit  31312  itgcoscmulx  31315  ibliooicc  31317  iblspltprt  31319  itgsincmulx  31320  itgsubsticc  31322  itgioocnicc  31323  iblcncfioo  31324  itgspltprt  31325  itgiccshift  31326  stoweidlem34  31362  stoweidlem52  31380  stirlinglem5  31406  dirkercncflem1  31431  dirkercncflem4  31434  fourierdlem4  31439  fourierdlem6  31441  fourierdlem10  31445  fourierdlem19  31454  fourierdlem20  31455  fourierdlem24  31459  fourierdlem25  31460  fourierdlem26  31461  fourierdlem27  31462  fourierdlem28  31463  fourierdlem31  31466  fourierdlem32  31467  fourierdlem33  31468  fourierdlem35  31470  fourierdlem37  31472  fourierdlem40  31475  fourierdlem41  31476  fourierdlem43  31478  fourierdlem44  31479  fourierdlem45  31480  fourierdlem46  31481  fourierdlem47  31482  fourierdlem48  31483  fourierdlem49  31484  fourierdlem50  31485  fourierdlem51  31486  fourierdlem52  31487  fourierdlem54  31489  fourierdlem56  31491  fourierdlem57  31492  fourierdlem59  31494  fourierdlem60  31495  fourierdlem61  31496  fourierdlem62  31497  fourierdlem63  31498  fourierdlem64  31499  fourierdlem65  31500  fourierdlem68  31503  fourierdlem69  31504  fourierdlem70  31505  fourierdlem72  31507  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem78  31513  fourierdlem79  31514  fourierdlem81  31516  fourierdlem82  31517  fourierdlem84  31519  fourierdlem89  31524  fourierdlem90  31525  fourierdlem91  31526  fourierdlem92  31527  fourierdlem93  31528  fourierdlem94  31529  fourierdlem97  31532  fourierdlem100  31535  fourierdlem101  31536  fourierdlem102  31537  fourierdlem103  31538  fourierdlem104  31539  fourierdlem107  31542  fourierdlem109  31544  fourierdlem111  31546  fourierdlem112  31547  fourierdlem113  31548  fourierdlem114  31549  sqwvfoura  31557  fouriersw  31560