Theorem rexrd 9703

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 9697	. 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 1873   RRcr 9551   RR*cxr 9687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3087  df-un 3447  df-in 3449  df-ss 3456  df-xr 9692

This theorem is referenced by:  rpxr  11322  rpxrd  11355  max0sub  11502  qextltlem  11508  xralrple  11511  xnegcl  11519  xaddf  11530  xmulf  11571  xadddi  11594  supxrre  11626  infxrre  11635  infmxrreOLD  11639  ixxub  11669  ixxlb  11670  ixxlbOLD  11671  ioo0  11674  ico0  11695  ioc0  11696  iooshf  11726  icoshftf1o  11768  supicc  11793  supiccub  11794  supicclub  11795  addmodid  12151  hashnnn0genn0  12538  elicc4abs  13388  caucvgrlem  13741  caucvgrlemOLD  13742  fprodge1  14054  pcxcl  14815  pcdvdsb  14823  pcaddlem  14838  ramcl2lem  14967  ramcl2lemOLD  14968  ramlb  14982  0ram  14983  prdsxmetlem  21387  xblss2ps  21420  xblss2  21421  blss2ps  21422  blss2  21423  blhalf  21424  metustto  21572  metustexhalf  21575  nmoi  21737  nmoix  21738  nmoi2  21739  nmoleub  21740  nmoiOLD  21753  nmoixOLD  21754  nmoi2OLD  21755  nmoleubOLD  21756  qdensere  21794  cnblcld  21799  ioo2blex  21816  tgioo  21818  blcvx  21820  zcld  21835  recld2  21836  iccntr  21843  icccmplem1  21844  reconnlem1  21848  reconnlem2  21849  opnreen  21853  metnrmlem3  21882  metnrmlem3OLD  21897  icoopnst  21971  cnheibor  21987  lebnumii  22001  nmoleub2lem  22132  lmnn  22237  iscau3  22252  minveclem4  22378  minveclem4OLD  22390  ivthlem1  22406  ivthlem2  22407  ivthlem3  22408  ivth2  22410  ivthle  22411  ivthle2  22412  ivthicc  22413  evthicc  22414  cniccbdd  22416  ovolgelb  22437  ovollb2lem  22445  ovolunlem1  22454  ovoliunlem1  22459  ovoliunlem2  22460  ovoliun  22462  ovolscalem1  22470  ovolicc1  22473  ovolicc2lem4OLD  22477  ovolicc2lem4  22478  ovolicc2lem5  22479  ovolicc2  22480  ovolicc  22481  nulmbl2  22494  voliunlem2  22508  ioombl1lem4  22518  ioorcl2  22528  uniioombllem1  22542  uniioombllem2a  22543  uniioombllem3  22547  dyaddisjlem  22557  dyadmaxlem  22559  opnmbllem  22563  volivth  22569  vitalilem4  22573  mbfmulc2lem  22607  mbfmax  22609  mbfposr  22612  ismbf3d  22614  mbfaddlem  22620  mbflimsup  22627  mbflimsupOLD  22628  mbfi1fseqlem4  22680  itg2lcl  22689  xrge0f  22693  itg2itg1  22698  itg2const2  22703  itg2seq  22704  itg2uba  22705  itg2lea  22706  itg2mulclem  22708  itg2mulc  22709  itg2splitlem  22710  itg2split  22711  itg2monolem2  22713  itg2monolem3  22714  itg2mono  22715  itg2gt0  22722  itg2cnlem1  22723  itg2cnlem2  22724  itg2cn  22725  iblss  22766  itgle  22771  itgeqa  22775  itgioo  22777  ibladdlem  22781  iblabs  22790  iblabsr  22791  iblmulc2  22792  itgsplit  22797  itgspliticc  22798  itgsplitioo  22799  bddmulibl  22800  ditgcl  22817  ditgswap  22818  ditgsplitlem  22819  dvferm1lem  22940  dvferm2lem  22942  dvferm  22944  rollelem  22945  rolle  22946  cmvth  22947  mvth  22948  dvlip  22949  dvlip2  22951  c1liplem1  22952  c1lip1  22953  dveq0  22956  dvgt0lem1  22958  dvivthlem1  22964  dvivth  22966  lhop1lem  22969  lhop1  22970  lhop2  22971  lhop  22972  dvcnvrelem1  22973  dvcnvre  22975  dvcvx  22976  dvfsumle  22977  dvfsumge  22978  dvfsumabs  22979  dvfsumlem2  22983  dvfsumlem3  22984  dvfsumlem4  22985  dvfsumrlimge0  22986  dvfsumrlim2  22988  ftc1lem1  22991  ftc1lem2  22992  ftc1a  22993  ftc1lem4  22995  ftc2  23000  ftc2ditglem  23001  itgparts  23003  itgsubstlem  23004  itgsubst  23005  degltlem1  23025  deg1ge  23051  coe1mul3  23052  deg1sublt  23063  deg1mul2  23067  deg1tmle  23070  deg1tm  23071  plypf1  23170  taylfvallem1  23316  tayl0  23321  pserulm  23381  psercnlem1  23384  pserdvlem1  23386  pserdvlem2  23387  abelthlem3  23392  abelth  23400  efcvx  23408  logno1  23585  logtayl  23609  xrlimcnp  23898  logfacbnd3  24155  log2sumbnd  24386  pntpbnd2  24429  pntibndlem3  24434  ttgcontlem1  24919  nvlmle  26332  nmooge0  26412  nmoub3i  26418  isblo3i  26446  ubthlem1  26516  minvecolem4  26526  minvecolem4OLD  26536  nmopge0  27568  nmfnge0  27584  nmophmi  27688  branmfn  27762  xaddeq0  28342  xlt2addrd  28350  xmulcand  28403  xreceu  28404  xdivrec  28409  fsumrp0cl  28471  xrge0slmod  28621  cnre2csqlem  28730  tpr2rico  28732  xrge0iifcnv  28753  xrge0iifhom  28757  lmxrge0  28772  esumfsup  28905  esumpcvgval  28913  esumcvg  28921  dya2iocress  29110  dya2iocbrsiga  29111  dya2icobrsiga  29112  dya2icoseg  29113  dya2iocucvr  29120  sxbrsigalem2  29122  omssubaddlem  29141  omssubadd  29142  omssubaddlemOLD  29145  omssubaddOLD  29146  orvcgteel  29314  dstrvprob  29318  orvclteel  29319  sgnmul  29427  sgnsub  29429  sgnmulsgn  29434  sgnmulsgp  29435  signstcl  29468  signstf  29469  signstf0  29471  signstfvn  29472  signsvtn0  29473  signstfvneq0  29475  signsvfn  29485  signsvfpn  29488  signsvfnn  29489  cvmliftlem6  30027  cvmliftlem7  30028  cvmliftlem8  30029  cvmliftlem9  30030  cvmliftlem10  30031  cvmliftlem13  30033  ivthALT  31002  iooelexlt  31735  relowlssretop  31736  relowlpssretop  31737  sin2h  31905  cos2h  31906  tan2h  31907  poimirlem30  31940  poimir  31943  heicant  31945  opnmbllem0  31946  mblfinlem1  31947  mblfinlem2  31948  mblfinlem3  31949  mblfinlem4  31950  ismblfin  31951  dvtanlemOLD  31961  itg2addnclem  31963  itg2addnclem2  31964  itg2gt0cn  31967  ibladdnclem  31968  iblabsnclem  31975  iblabsnc  31976  iblmulc2nc  31977  bddiblnc  31982  ftc1cnnclem  31985  ftc1anclem1  31987  ftc1anclem4  31990  ftc1anclem5  31991  ftc1anclem6  31992  ftc1anclem7  31993  ftc1anclem8  31994  ftc1anc  31995  ftc2nc  31996  areacirclem1  32002  areacirclem5  32006  areacirc  32007  isbnd3  32086  blbnd  32089  prdsbnd  32095  prdsbnd2  32097  cntotbnd  32098  idomrootle  36045  idomodle  36046  itgpowd  36075  imo72b2  36595  cvgdvgrat  36638  radcnvrat  36639  rfcnpre3  37333  rfcnpre4  37334  nnxrd  37342  lefldiveq  37466  lttri5d  37477  supxrgere  37516  supxrgelem  37520  supxrge  37521  xralrple2  37537  gtnelioc  37542  ltnelicc  37549  iooabslt  37551  gtnelicc  37552  eliooshift  37559  iocopn  37576  eliccelioc  37577  iooshift  37578  icoopn  37581  fsumge0cl  37599  limciccioolb  37647  lptioo1  37658  limcicciooub  37663  ltmod  37664  lptre2pt  37666  limsupre  37667  limsupreOLD  37668  limcresiooub  37669  limcresioolb  37670  limcleqr  37671  sinaover2ne0  37689  ioccncflimc  37709  icccncfext  37711  icocncflimc  37713  cncfiooicclem1  37717  cncfiooicc  37718  cncfiooiccre  37719  cncfioobdlem  37720  dvbdfbdioolem1  37746  dvbdfbdioolem2  37747  dvbdfbdioo  37748  ioodvbdlimc1lem1  37749  ioodvbdlimc1lem2  37750  ioodvbdlimc1lem1OLD  37751  ioodvbdlimc1lem2OLD  37752  ioodvbdlimc1  37753  ioodvbdlimc2lem  37754  ioodvbdlimc2lemOLD  37755  ioodvbdlimc2  37756  ditgeqiooicc  37783  iblsplit  37789  itgcoscmulx  37792  ibliooicc  37794  iblspltprt  37796  itgsincmulx  37797  itgsubsticc  37799  itgioocnicc  37800  iblcncfioo  37801  itgspltprt  37802  itgiccshift  37803  stoweidlem34  37841  stoweidlem52  37859  stirlinglem5  37886  dirkercncflem1  37911  dirkercncflem4  37914  fourierdlem4  37919  fourierdlem10  37925  fourierdlem19  37934  fourierdlem20  37935  fourierdlem24  37939  fourierdlem25  37940  fourierdlem26  37941  fourierdlem27  37942  fourierdlem28  37943  fourierdlem31  37946  fourierdlem31OLD  37947  fourierdlem32  37948  fourierdlem33  37949  fourierdlem35  37951  fourierdlem37  37953  fourierdlem40  37956  fourierdlem41  37957  fourierdlem43  37960  fourierdlem44  37961  fourierdlem46  37962  fourierdlem47  37963  fourierdlem48  37964  fourierdlem49  37965  fourierdlem50  37966  fourierdlem51  37967  fourierdlem52  37968  fourierdlem54  37970  fourierdlem57  37973  fourierdlem59  37975  fourierdlem60  37976  fourierdlem61  37977  fourierdlem62  37978  fourierdlem63  37979  fourierdlem64  37980  fourierdlem65  37981  fourierdlem68  37984  fourierdlem69  37985  fourierdlem70  37986  fourierdlem72  37988  fourierdlem73  37989  fourierdlem74  37990  fourierdlem75  37991  fourierdlem76  37992  fourierdlem78  37994  fourierdlem79  37995  fourierdlem81  37997  fourierdlem82  37998  fourierdlem84  38000  fourierdlem89  38005  fourierdlem90  38006  fourierdlem91  38007  fourierdlem92  38008  fourierdlem93  38009  fourierdlem94  38010  fourierdlem97  38013  fourierdlem100  38016  fourierdlem101  38017  fourierdlem102  38018  fourierdlem103  38019  fourierdlem104  38020  fourierdlem107  38023  fourierdlem109  38025  fourierdlem111  38027  fourierdlem112  38028  fourierdlem113  38029  fourierdlem114  38030  sqwvfoura  38038  fouriersw  38041  etransclem23  38068  etransclem46  38091  sge0cl  38137  sge0fsum  38143  sge0iunmptlemre  38171  sge0isum  38183  sge0ad2en  38187  sge0xaddlem1  38189  sge0xaddlem2  38190  omessre  38245  omeiunltfirp  38254  hoissre  38276  hoiprodcl  38279  ovnsubaddlem1  38302  hoiprodcl3  38312  hoidmvcl  38314  hsphoidmvle2  38317  hsphoidmvle  38318  sge0hsphoire  38321  hoidmv1lelem1  38323  hoidmv1lelem2  38324  hoidmv1lelem3  38325  hoidmv1le  38326  hoidmvlelem1  38327  hoidmvlelem2  38328  hoidmvlelem3  38329  hoidmvlelem4  38330  ovnhoilem1  38333  ovnhoilem2  38334  ovnhoi  38335  bgoldbtbnd  38780