Theorem rexrd 9632

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

Syntax hints:   -> wi 4   e. wcel 1823   RRcr 9480   RR*cxr 9616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475  df-xr 9621

This theorem is referenced by:  rpxr  11228  rpxrd  11260  max0sub  11398  qextltlem  11404  xralrple  11407  xnegcl  11415  xaddf  11426  xmulf  11467  xadddi  11490  supxrre  11522  infmxrre  11530  ixxub  11553  ixxlb  11554  ioo0  11557  ico0  11578  ioc0  11579  iooshf  11606  icoshftf1o  11646  supicc  11671  supiccub  11672  supicclub  11673  hashnnn0genn0  12398  elicc4abs  13234  caucvgrlem  13577  pcxcl  14468  pcdvdsb  14476  pcaddlem  14491  ramcl2lem  14611  ramlb  14621  0ram  14622  prdsxmetlem  21037  xblss2ps  21070  xblss2  21071  blss2ps  21072  blss2  21073  blhalf  21074  metusttoOLD  21226  metustto  21227  metustexhalfOLD  21232  metustexhalf  21233  nmoi  21401  nmoix  21402  nmoi2  21403  nmoleub  21404  qdensere  21443  cnblcld  21448  ioo2blex  21465  tgioo  21467  blcvx  21469  zcld  21484  recld2  21485  iccntr  21492  icccmplem1  21493  reconnlem1  21497  reconnlem2  21498  opnreen  21502  metnrmlem3  21531  icoopnst  21605  cnheibor  21621  lebnumii  21632  nmoleub2lem  21763  lmnn  21868  iscau3  21883  minveclem4  22013  ivthlem1  22029  ivthlem2  22030  ivthlem3  22031  ivth2  22033  ivthle  22034  ivthle2  22035  ivthicc  22036  evthicc  22037  cniccbdd  22039  ovolgelb  22057  ovollb2lem  22065  ovolunlem1  22074  ovoliunlem1  22079  ovoliunlem2  22080  ovoliun  22082  ovolscalem1  22090  ovolicc1  22093  ovolicc2lem4  22097  ovolicc2lem5  22098  ovolicc2  22099  ovolicc  22100  nulmbl2  22113  voliunlem2  22127  ioombl1lem4  22137  ioorcl2  22147  uniioombllem1  22156  uniioombllem2a  22157  uniioombllem3  22160  dyaddisjlem  22170  dyadmaxlem  22172  opnmbllem  22176  volivth  22182  vitalilem4  22186  mbfmulc2lem  22220  mbfmax  22222  mbfposr  22225  ismbf3d  22227  mbfaddlem  22233  mbflimsup  22239  mbfi1fseqlem4  22291  itg2lcl  22300  xrge0f  22304  itg2itg1  22309  itg2const2  22314  itg2seq  22315  itg2uba  22316  itg2lea  22317  itg2mulclem  22319  itg2mulc  22320  itg2splitlem  22321  itg2split  22322  itg2monolem2  22324  itg2monolem3  22325  itg2mono  22326  itg2gt0  22333  itg2cnlem1  22334  itg2cnlem2  22335  itg2cn  22336  iblss  22377  itgle  22382  itgeqa  22386  itgioo  22388  ibladdlem  22392  iblabs  22401  iblabsr  22402  iblmulc2  22403  itgsplit  22408  itgspliticc  22409  itgsplitioo  22410  bddmulibl  22411  ditgcl  22428  ditgswap  22429  ditgsplitlem  22430  dvferm1lem  22551  dvferm2lem  22553  dvferm  22555  rollelem  22556  rolle  22557  cmvth  22558  mvth  22559  dvlip  22560  dvlip2  22562  c1liplem1  22563  c1lip1  22564  dveq0  22567  dvgt0lem1  22569  dvivthlem1  22575  dvivth  22577  lhop1lem  22580  lhop1  22581  lhop2  22582  lhop  22583  dvcnvrelem1  22584  dvcnvre  22586  dvcvx  22587  dvfsumle  22588  dvfsumge  22589  dvfsumabs  22590  dvfsumlem2  22594  dvfsumlem3  22595  dvfsumlem4  22596  dvfsumrlimge0  22597  dvfsumrlim2  22599  ftc1lem1  22602  ftc1lem2  22603  ftc1a  22604  ftc1lem4  22606  ftc2  22611  ftc2ditglem  22612  itgparts  22614  itgsubstlem  22615  itgsubst  22616  degltlem1  22638  deg1ge  22665  coe1mul3  22666  deg1sublt  22677  deg1mul2  22681  deg1tmle  22684  deg1tm  22685  plypf1  22775  taylfvallem1  22918  tayl0  22923  pserulm  22983  psercnlem1  22986  pserdvlem1  22988  pserdvlem2  22989  abelthlem3  22994  abelth  23002  efcvx  23010  logno1  23185  logtayl  23209  xrlimcnp  23496  logfacbnd3  23696  log2sumbnd  23927  pntpbnd2  23970  pntibndlem3  23975  ttgcontlem1  24390  nvlmle  25800  nmooge0  25880  nmoub3i  25886  isblo3i  25914  ubthlem1  25984  minvecolem4  25994  nmopge0  27028  nmfnge0  27044  nmophmi  27148  branmfn  27222  xaddeq0  27804  xlt2addrd  27809  xmulcand  27851  xreceu  27852  xdivrec  27857  fsumrp0cl  27919  xrge0slmod  28069  cnre2csqlem  28127  tpr2rico  28129  xrge0iifcnv  28150  xrge0iifhom  28154  lmxrge0  28169  esumfsup  28299  esumpcvgval  28307  esumcvg  28315  dya2iocress  28482  dya2iocbrsiga  28483  dya2icobrsiga  28484  dya2icoseg  28485  dya2iocucvr  28492  sxbrsigalem2  28494  omssubaddlem  28507  omssubadd  28508  orvcgteel  28670  dstrvprob  28674  orvclteel  28675  sgnmul  28745  sgnsub  28747  sgnmulsgn  28752  sgnmulsgp  28753  signstcl  28786  signstf  28787  signstf0  28789  signstfvn  28790  signsvtn0  28791  signstfvneq0  28793  signsvfn  28803  signsvfpn  28806  signsvfnn  28807  cvmliftlem6  28999  cvmliftlem7  29000  cvmliftlem8  29001  cvmliftlem9  29002  cvmliftlem10  29003  cvmliftlem13  29005  sin2h  30285  cos2h  30286  tan2h  30287  heicant  30289  opnmbllem0  30290  mblfinlem1  30291  mblfinlem2  30292  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  dvtanlem  30304  itg2addnclem  30306  itg2addnclem2  30307  itg2gt0cn  30310  ibladdnclem  30311  iblabsnclem  30318  iblabsnc  30319  iblmulc2nc  30320  bddiblnc  30325  ftc1cnnclem  30328  ftc1anclem1  30330  ftc1anclem4  30333  ftc1anclem5  30334  ftc1anclem6  30335  ftc1anclem7  30336  ftc1anclem8  30337  ftc1anc  30338  ftc2nc  30339  areacirclem1  30347  areacirclem5  30351  areacirc  30352  ivthALT  30393  isbnd3  30520  blbnd  30523  prdsbnd  30529  prdsbnd2  30531  cntotbnd  30532  idomrootle  31393  idomodle  31394  itgpowd  31423  cvgdvgrat  31435  radcnvrat  31436  rfcnpre3  31648  rfcnpre4  31649  nnxrd  31659  lefldiveq  31722  lttri5d  31738  gtnelioc  31762  ltnelicc  31769  iooabslt  31771  gtnelicc  31772  eliooshift  31780  iocopn  31799  eliccelioc  31800  iooshift  31801  icoopn  31804  fprodge1  31837  limciccioolb  31866  lptioo1  31877  limcicciooub  31882  ltmod  31883  lptre2pt  31885  limsupre  31886  limcresiooub  31887  limcresioolb  31888  limcleqr  31889  sinaover2ne0  31907  ioccncflimc  31927  icccncfext  31929  icocncflimc  31931  cncfiooicclem1  31935  cncfiooicc  31936  cncfiooiccre  31937  cncfioobdlem  31938  dvbdfbdioolem1  31964  dvbdfbdioolem2  31965  dvbdfbdioo  31966  ioodvbdlimc1lem1  31967  ioodvbdlimc1lem2  31968  ioodvbdlimc1  31969  ioodvbdlimc2lem  31970  ioodvbdlimc2  31971  ditgeqiooicc  31998  iblsplit  32004  itgcoscmulx  32007  ibliooicc  32009  iblspltprt  32011  itgsincmulx  32012  itgsubsticc  32014  itgioocnicc  32015  iblcncfioo  32016  itgspltprt  32017  itgiccshift  32018  stoweidlem34  32055  stoweidlem52  32073  stirlinglem5  32099  dirkercncflem1  32124  dirkercncflem4  32127  fourierdlem4  32132  fourierdlem10  32138  fourierdlem19  32147  fourierdlem20  32148  fourierdlem24  32152  fourierdlem25  32153  fourierdlem26  32154  fourierdlem27  32155  fourierdlem28  32156  fourierdlem31  32159  fourierdlem32  32160  fourierdlem33  32161  fourierdlem35  32163  fourierdlem37  32165  fourierdlem40  32168  fourierdlem41  32169  fourierdlem43  32171  fourierdlem44  32172  fourierdlem46  32174  fourierdlem47  32175  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem52  32180  fourierdlem54  32182  fourierdlem57  32185  fourierdlem59  32187  fourierdlem60  32188  fourierdlem61  32189  fourierdlem62  32190  fourierdlem63  32191  fourierdlem64  32192  fourierdlem65  32193  fourierdlem68  32196  fourierdlem69  32197  fourierdlem70  32198  fourierdlem72  32200  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem78  32206  fourierdlem79  32207  fourierdlem81  32209  fourierdlem82  32210  fourierdlem84  32212  fourierdlem89  32217  fourierdlem90  32218  fourierdlem91  32219  fourierdlem92  32220  fourierdlem93  32221  fourierdlem94  32222  fourierdlem97  32225  fourierdlem100  32228  fourierdlem101  32229  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem107  32235  fourierdlem109  32237  fourierdlem111  32239  fourierdlem112  32240  fourierdlem113  32241  fourierdlem114  32242  sqwvfoura  32250  fouriersw  32253  etransclem23  32279  etransclem46  32302  imo72b2  38445