Theorem rexrd 11225

Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rexrd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
rexrd	⊢ (𝜑 → 𝐴 ∈ ℝ*)

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 11219	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sselid 3932	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11065  ℝ^*cxr 11208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919  df-xr 11213

This theorem is referenced by:  xnn0xr  12552  rpxr  12996  rpxrd  13031  max0sub  13192  qextltlem  13198  xralrple  13201  xnegcl  13209  xaddf  13220  xnn0lem1lt  13240  xnn0lenn0nn0  13241  xmulf  13268  xadddi  13291  xrub  13308  supxrre  13323  infxrre  13333  ixxub  13363  ixxlb  13364  ioo0  13367  ico0  13388  ioc0  13389  iooshf  13423  icoshftf1o  13471  supicc  13498  supiccub  13499  supicclub  13500  xnn0xrge0  13503  ssfzunsn  13568  addmodid  13925  hashnnn0genn0  14349  hashunsnggt  14400  sgnsub  15109  sgnmul  15110  sgnmulsgn  15112  elicc4abs  15337  caucvgrlem  15690  fprodge1  16015  pcxcl  16887  pcdvdsb  16895  pcaddlem  16914  ramcl2lem  17035  ramlb  17045  0ram  17046  setsstruct  17202  prdsxmetlem  24415  xblss2ps  24448  xblss2  24449  blss2ps  24450  blss2  24451  blhalf  24452  metustto  24600  metustexhalf  24603  nmoi  24775  nmoix  24776  nmoi2  24777  nmoleub  24778  qdensere  24816  cnblcld  24821  ioo2blex  24841  tgioo  24843  blcvx  24845  zcld  24861  recld2  24862  iccntr  24869  icccmplem1  24870  reconnlem1  24874  reconnlem2  24875  opnreen  24879  metnrmlem3  24909  icoopnst  24988  iocopnst  24989  cnheibor  25004  lebnumii  25015  nmoleub2lem  25163  lmnn  25312  iscau3  25327  minveclem4  25481  ivthlem1  25500  ivthlem2  25501  ivthlem3  25502  ivth2  25504  ivthle  25505  ivthle2  25506  ivthicc  25507  evthicc  25508  cniccbdd  25510  ovolgelb  25529  ovollb2lem  25537  ovolunlem1  25546  ovoliunlem1  25551  ovoliunlem2  25552  ovoliun  25554  ovolscalem1  25562  ovolicc1  25565  ovolicc2lem4  25569  ovolicc2lem5  25570  ovolicc2  25571  ovolicc  25572  nulmbl2  25585  voliunlem2  25600  ioombl1lem4  25610  ioorcl2  25621  uniioombllem1  25630  uniioombllem2a  25631  uniioombllem3  25634  dyaddisjlem  25644  dyadmaxlem  25646  opnmbllem  25650  volivth  25656  vitalilem4  25660  mbfmulc2lem  25696  mbfmax  25698  mbfposr  25701  ismbf3d  25703  mbfaddlem  25709  mbflimsup  25715  mbfi1fseqlem4  25767  itg2lcl  25776  xrge0f  25780  itg2itg1  25785  itg2const2  25790  itg2seq  25791  itg2uba  25792  itg2lea  25793  itg2mulclem  25795  itg2mulc  25796  itg2splitlem  25797  itg2split  25798  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  itg2cn  25812  iblss  25854  itgle  25859  itgeqa  25863  itgioo  25865  ibladdlem  25869  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgsplit  25885  itgspliticc  25886  itgsplitioo  25887  bddmulibl  25888  bddiblnc  25891  ditgcl  25907  ditgswap  25908  ditgsplitlem  25909  dvferm1lem  26033  dvferm2lem  26035  dvferm  26037  rollelem  26038  rolle  26039  cmvth  26040  mvth  26041  dvlip  26042  dvlip2  26044  c1liplem1  26045  c1lip1  26046  dveq0  26049  dvgt0lem1  26051  dvivthlem1  26057  dvivth  26059  lhop1lem  26062  lhop1  26063  lhop2  26064  lhop  26065  dvcnvrelem1  26066  dvcnvre  26068  dvcvx  26069  dvfsumle  26070  dvfsumge  26071  dvfsumabs  26072  dvfsumlem2  26076  dvfsumlem3  26077  dvfsumlem4  26078  dvfsumrlimge0  26079  dvfsumrlim2  26081  ftc1lem1  26084  ftc1lem2  26085  ftc1a  26086  ftc1lem4  26088  ftc2  26093  ftc2ditglem  26094  itgparts  26096  itgsubstlem  26097  itgsubst  26098  itgpowd  26099  degltlem1  26119  deg1ge  26145  coe1mul3  26146  deg1sublt  26157  deg1mul2  26161  deg1tmle  26165  deg1tm  26166  idomrootle  26220  plypf1  26259  taylfvallem1  26407  tayl0  26412  pserulm  26472  psercnlem1  26475  pserdvlem1  26477  pserdvlem2  26478  abelthlem3  26483  abelth  26491  efcvx  26499  logno1  26688  logtayl  26712  xrlimcnp  27020  logfacbnd3  27274  log2sumbnd  27595  pntpbnd2  27638  pntibndlem3  27643  ttgcontlem1  29041  nmooge0  30926  nmoub3i  30932  isblo3i  30960  ubthlem1  31029  minvecolem4  31039  nmopge0  32070  nmfnge0  32086  nmophmi  32190  branmfn  32264  sgnval2  32897  nn0mnfxrd  32913  xaddeq0  32915  xlt2addrd  32921  sgnmulsgp  32994  xmulcand  33058  xreceu  33059  xdivrec  33064  fsumrp0cl  33159  xrge0slmod  33494  ply1degltel  33750  ply1degleel  33751  ply1degltlss  33752  ply1degltdimlem  33879  ply1degltdim  33880  fldextrspundgdvdslem  33937  extdgfialglem1  33949  cos9thpiminplylem2  34040  cnre2csqlem  34167  tpr2rico  34169  xrge0iifcnv  34190  xrge0iifhom  34194  lmxrge0  34209  esumfsup  34327  esumpcvgval  34335  esumcvg  34343  dya2iocress  34531  dya2iocbrsiga  34532  dya2icobrsiga  34533  dya2icoseg  34534  dya2iocucvr  34541  sxbrsigalem2  34543  omssubaddlem  34556  omssubadd  34557  orvcgteel  34725  dstrvprob  34729  orvclteel  34730  signstcl  34819  signstf  34820  signstf0  34822  signstfvn  34823  signsvtn0  34824  signsvfn  34836  signsvfpn  34839  signsvfnn  34840  ftc2re  34852  cvmliftlem6  35600  cvmliftlem7  35601  cvmliftlem8  35602  cvmliftlem9  35603  cvmliftlem10  35604  cvmliftlem13  35606  ivthALT  36655  iooelexlt  37816  relowlssretop  37817  relowlpssretop  37818  sin2h  38069  cos2h  38070  tan2h  38071  poimirlem30  38109  poimir  38112  heicant  38114  opnmbllem0  38115  mblfinlem1  38116  mblfinlem2  38117  mblfinlem3  38118  mblfinlem4  38119  ismblfin  38120  itg2addnclem  38130  itg2addnclem2  38131  itg2gt0cn  38134  ibladdnclem  38135  iblabsnclem  38142  iblabsnc  38143  iblmulc2nc  38144  ftc1cnnclem  38150  ftc1anclem1  38152  ftc1anclem4  38155  ftc1anclem5  38156  ftc1anclem6  38157  ftc1anclem7  38158  ftc1anclem8  38159  ftc1anc  38160  ftc2nc  38161  areacirclem1  38167  areacirclem5  38171  areacirc  38172  isbnd3  38243  blbnd  38246  prdsbnd  38252  prdsbnd2  38254  cntotbnd  38255  dvrelog3  42642  0nonelalab  42644  dvrelogpow2b  42645  dvle2  42649  aks4d1p1p6  42650  aks4d1p1p5  42652  aks6d1c6lem3  42749  aks6d1c7lem2  42758  unitscyglem5  42776  idomodle  43728  imo72b2  44708  cvgdvgrat  44849  radcnvrat  44850  rfcnpre3  45573  rfcnpre4  45574  absfico  45754  nnxrd  45813  lefldiveq  45831  lttri5d  45838  supxrgere  45869  supxrgelem  45873  supxrge  45874  xralrple2  45890  infxr  45902  infleinflem1  45905  infleinflem2  45906  xralrple4  45908  xralrple3  45909  xrralrecnnle  45918  xrralrecnnge  45925  supxrunb3  45934  unb2ltle  45949  zxrd  45987  gtnelioc  46027  ltnelicc  46033  iooabslt  46035  gtnelicc  46036  eliooshift  46042  iocopn  46056  eliccelioc  46057  iooshift  46058  icoopn  46061  ge0lere  46068  iooiinicc  46078  sqrlearg  46089  iooiinioc  46092  uzinico  46095  preimaiocmnf  46096  uzubioo  46101  fsumge0cl  46109  limciccioolb  46157  lptioo1  46168  limcicciooub  46171  ltmod  46172  lptre2pt  46174  limsupre  46175  limcresiooub  46176  limcresioolb  46177  limcleqr  46178  limsupresico  46234  limsuppnfdlem  46235  limsupub  46238  limsupequzlem  46256  limsupre2lem  46258  limsupre3lem  46266  limsupvaluz2  46272  supcnvlimsup  46274  liminfresico  46305  limsup10exlem  46306  liminflelimsuplem  46309  limsupgtlem  46311  liminfval4  46323  liminfvaluz2  46329  limsupvaluz4  46334  liminflimsupclim  46341  xlimxrre  46365  xlimmnfvlem1  46366  xlimmnfv  46368  xlimpnfvlem1  46370  xlimpnfv  46372  sinaover2ne0  46402  ioccncflimc  46419  icccncfext  46421  icocncflimc  46423  cncfiooicclem1  46427  cncfiooicc  46428  cncfiooiccre  46429  cncfioobdlem  46430  dvbdfbdioolem1  46462  dvbdfbdioolem2  46463  dvbdfbdioo  46464  ioodvbdlimc1lem1  46465  ioodvbdlimc1lem2  46466  ioodvbdlimc1  46467  ioodvbdlimc2lem  46468  ioodvbdlimc2  46469  ditgeqiooicc  46494  iblsplit  46500  itgcoscmulx  46503  ibliooicc  46505  iblspltprt  46507  itgsincmulx  46508  itgsubsticc  46510  itgioocnicc  46511  iblcncfioo  46512  itgspltprt  46513  itgiccshift  46514  volioore  46524  voliooico  46526  voliooicof  46530  voliccico  46533  stoweidlem34  46568  stoweidlem52  46586  stirlinglem5  46612  dirkercncflem1  46637  dirkercncflem4  46640  fourierdlem4  46645  fourierdlem10  46651  fourierdlem19  46660  fourierdlem20  46661  fourierdlem24  46665  fourierdlem25  46666  fourierdlem26  46667  fourierdlem27  46668  fourierdlem28  46669  fourierdlem31  46672  fourierdlem32  46673  fourierdlem33  46674  fourierdlem35  46676  fourierdlem37  46678  fourierdlem40  46681  fourierdlem41  46682  fourierdlem43  46684  fourierdlem44  46685  fourierdlem46  46686  fourierdlem47  46687  fourierdlem48  46688  fourierdlem49  46689  fourierdlem50  46690  fourierdlem51  46691  fourierdlem52  46692  fourierdlem54  46694  fourierdlem57  46697  fourierdlem59  46699  fourierdlem60  46700  fourierdlem61  46701  fourierdlem62  46702  fourierdlem63  46703  fourierdlem64  46704  fourierdlem65  46705  fourierdlem68  46708  fourierdlem69  46709  fourierdlem70  46710  fourierdlem72  46712  fourierdlem73  46713  fourierdlem74  46714  fourierdlem75  46715  fourierdlem76  46716  fourierdlem78  46718  fourierdlem79  46719  fourierdlem81  46721  fourierdlem82  46722  fourierdlem84  46724  fourierdlem89  46729  fourierdlem90  46730  fourierdlem91  46731  fourierdlem92  46732  fourierdlem93  46733  fourierdlem94  46734  fourierdlem97  46737  fourierdlem100  46740  fourierdlem101  46741  fourierdlem102  46742  fourierdlem103  46743  fourierdlem104  46744  fourierdlem107  46747  fourierdlem109  46749  fourierdlem111  46751  fourierdlem112  46752  fourierdlem113  46753  fourierdlem114  46754  sqwvfoura  46762  fouriersw  46765  etransclem23  46791  etransclem46  46814  qndenserrnbllem  46828  rrxsnicc  46834  ioorrnopnlem  46838  ioorrnopnxrlem  46840  salgencntex  46877  sge0cl  46915  sge0fsum  46921  sge0iunmptlemre  46949  sge0isum  46961  sge0ad2en  46965  sge0xaddlem1  46967  sge0xaddlem2  46968  sge0reuz  46981  voliunsge0lem  47006  meassre  47011  omessre  47044  omeiunltfirp  47053  hoissre  47078  hoiprodcl  47081  ovnsubaddlem1  47104  hoiprodcl3  47114  hoidmvcl  47116  hsphoidmvle2  47119  hsphoidmvle  47120  sge0hsphoire  47123  hoidmv1lelem1  47125  hoidmv1lelem2  47126  hoidmv1lelem3  47127  hoidmv1le  47128  hoidmvlelem1  47129  hoidmvlelem2  47130  hoidmvlelem3  47131  hoidmvlelem4  47132  ovnhoilem1  47135  ovnhoilem2  47136  ovnhoi  47137  ovnlecvr2  47144  hspdifhsp  47150  hoidifhspdmvle  47154  hoiqssbllem1  47156  hoiqssbllem2  47157  hoiqssbllem3  47158  hspmbllem1  47160  hspmbllem2  47161  volicorege0  47171  ovolval5lem1  47186  ovolval5lem2  47187  iinhoiicclem  47207  iinhoiicc  47208  iunhoiioolem  47209  iunhoiioo  47210  vonioolem2  47215  vonicclem2  47218  vonsn  47225  pimltmnf2f  47231  pimconstlt0  47235  pimgtpnf2f  47239  salpreimagelt  47241  salpreimalegt  47243  preimageiingt  47254  preimaleiinlt  47255  pimrecltneg  47258  issmflem  47261  issmflelem  47278  issmfgtlem  47289  issmfgt  47290  smfaddlem1  47297  issmfgelem  47303  issmfge  47304  smfpimioompt  47320  smfresal  47322  smfrec  47323  smfmullem1  47325  smfmullem2  47326  smfmullem3  47327  smfmullem4  47328  smfpimbor1lem1  47332  smfsuplem1  47345  smflimsuplem4  47357  smfliminflem  47364  smfdmmblpimne  47371  smfpimne  47373  smfpimne2  47374  fsupdm  47376  finfdm  47380  smfinfdmmbllem  47382  bgoldbtbnd  48391  eenglngeehlnmlem2  49320