Theorem rexrd 11231

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 11225	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sselid 3947	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℝ^*cxr 11214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-xr 11219

This theorem is referenced by:  xnn0xr  12527  rpxr  12968  rpxrd  13003  max0sub  13163  qextltlem  13169  xralrple  13172  xnegcl  13180  xaddf  13191  xnn0lem1lt  13211  xnn0lenn0nn0  13212  xmulf  13239  xadddi  13262  xrub  13279  supxrre  13294  infxrre  13304  ixxub  13334  ixxlb  13335  ioo0  13338  ico0  13359  ioc0  13360  iooshf  13394  icoshftf1o  13442  supicc  13469  supiccub  13470  supicclub  13471  xnn0xrge0  13474  ssfzunsn  13538  addmodid  13891  hashnnn0genn0  14315  hashunsnggt  14366  elicc4abs  15293  caucvgrlem  15646  fprodge1  15968  pcxcl  16839  pcdvdsb  16847  pcaddlem  16866  ramcl2lem  16987  ramlb  16997  0ram  16998  setsstruct  17153  prdsxmetlem  24263  xblss2ps  24296  xblss2  24297  blss2ps  24298  blss2  24299  blhalf  24300  metustto  24448  metustexhalf  24451  nmoi  24623  nmoix  24624  nmoi2  24625  nmoleub  24626  qdensere  24664  cnblcld  24669  ioo2blex  24689  tgioo  24691  blcvx  24693  zcld  24709  recld2  24710  iccntr  24717  icccmplem1  24718  reconnlem1  24722  reconnlem2  24723  opnreen  24727  metnrmlem3  24757  icoopnst  24843  iocopnst  24844  cnheibor  24861  lebnumii  24872  nmoleub2lem  25021  lmnn  25170  iscau3  25185  minveclem4  25339  ivthlem1  25359  ivthlem2  25360  ivthlem3  25361  ivth2  25363  ivthle  25364  ivthle2  25365  ivthicc  25366  evthicc  25367  cniccbdd  25369  ovolgelb  25388  ovollb2lem  25396  ovolunlem1  25405  ovoliunlem1  25410  ovoliunlem2  25411  ovoliun  25413  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem4  25428  ovolicc2lem5  25429  ovolicc2  25430  ovolicc  25431  nulmbl2  25444  voliunlem2  25459  ioombl1lem4  25469  ioorcl2  25480  uniioombllem1  25489  uniioombllem2a  25490  uniioombllem3  25493  dyaddisjlem  25503  dyadmaxlem  25505  opnmbllem  25509  volivth  25515  vitalilem4  25519  mbfmulc2lem  25555  mbfmax  25557  mbfposr  25560  ismbf3d  25562  mbfaddlem  25568  mbflimsup  25574  mbfi1fseqlem4  25626  itg2lcl  25635  xrge0f  25639  itg2itg1  25644  itg2const2  25649  itg2seq  25650  itg2uba  25651  itg2lea  25652  itg2mulclem  25654  itg2mulc  25655  itg2splitlem  25656  itg2split  25657  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  itg2cn  25671  iblss  25713  itgle  25718  itgeqa  25722  itgioo  25724  ibladdlem  25728  iblabs  25737  iblabsr  25738  iblmulc2  25739  itgsplit  25744  itgspliticc  25745  itgsplitioo  25746  bddmulibl  25747  bddiblnc  25750  ditgcl  25766  ditgswap  25767  ditgsplitlem  25768  dvferm1lem  25895  dvferm2lem  25897  dvferm  25899  rollelem  25900  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlip2  25907  c1liplem1  25908  c1lip1  25909  dveq0  25912  dvgt0lem1  25914  dvivthlem1  25920  dvivth  25922  lhop1lem  25925  lhop1  25926  lhop2  25927  lhop  25928  dvcnvrelem1  25929  dvcnvre  25931  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsumrlimge0  25944  dvfsumrlim2  25946  ftc1lem1  25949  ftc1lem2  25950  ftc1a  25951  ftc1lem4  25953  ftc2  25958  ftc2ditglem  25959  itgparts  25961  itgsubstlem  25962  itgsubst  25963  itgpowd  25964  degltlem1  25984  deg1ge  26010  coe1mul3  26011  deg1sublt  26022  deg1mul2  26026  deg1tmle  26030  deg1tm  26031  idomrootle  26085  plypf1  26124  taylfvallem1  26271  tayl0  26276  pserulm  26338  psercnlem1  26342  pserdvlem1  26344  pserdvlem2  26345  abelthlem3  26350  abelth  26358  efcvx  26366  logno1  26552  logtayl  26576  xrlimcnp  26885  logfacbnd3  27141  log2sumbnd  27462  pntpbnd2  27505  pntibndlem3  27510  ttgcontlem1  28819  nmooge0  30703  nmoub3i  30709  isblo3i  30737  ubthlem1  30806  minvecolem4  30816  nmopge0  31847  nmfnge0  31863  nmophmi  31967  branmfn  32041  sgnval2  32665  xaddeq0  32683  xlt2addrd  32689  sgnmul  32767  sgnsub  32769  sgnmulsgn  32774  sgnmulsgp  32775  xmulcand  32848  xreceu  32849  xdivrec  32854  fsumrp0cl  32969  xrge0slmod  33326  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  ply1degltdimlem  33625  ply1degltdim  33626  fldextrspundgdvdslem  33682  cos9thpiminplylem2  33780  cnre2csqlem  33907  tpr2rico  33909  xrge0iifcnv  33930  xrge0iifhom  33934  lmxrge0  33949  esumfsup  34067  esumpcvgval  34075  esumcvg  34083  dya2iocress  34272  dya2iocbrsiga  34273  dya2icobrsiga  34274  dya2icoseg  34275  dya2iocucvr  34282  sxbrsigalem2  34284  omssubaddlem  34297  omssubadd  34298  orvcgteel  34466  dstrvprob  34470  orvclteel  34471  signstcl  34563  signstf  34564  signstf0  34566  signstfvn  34567  signsvtn0  34568  signsvfn  34580  signsvfpn  34583  signsvfnn  34584  ftc2re  34596  cvmliftlem6  35284  cvmliftlem7  35285  cvmliftlem8  35286  cvmliftlem9  35287  cvmliftlem10  35288  cvmliftlem13  35290  ivthALT  36330  iooelexlt  37357  relowlssretop  37358  relowlpssretop  37359  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem30  37651  poimir  37654  heicant  37656  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem  37672  itg2addnclem2  37673  itg2gt0cn  37676  ibladdnclem  37677  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  ftc1cnnclem  37692  ftc1anclem1  37694  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  ftc2nc  37703  areacirclem1  37709  areacirclem5  37713  areacirc  37714  isbnd3  37785  blbnd  37788  prdsbnd  37794  prdsbnd2  37796  cntotbnd  37797  dvrelog3  42060  0nonelalab  42062  dvrelogpow2b  42063  dvle2  42067  aks4d1p1p6  42068  aks4d1p1p5  42070  aks6d1c6lem3  42167  aks6d1c7lem2  42176  unitscyglem5  42194  idomodle  43187  imo72b2  44168  cvgdvgrat  44309  radcnvrat  44310  rfcnpre3  45034  rfcnpre4  45035  absfico  45219  nnxrd  45279  lefldiveq  45297  lttri5d  45304  supxrgere  45336  supxrgelem  45340  supxrge  45341  xralrple2  45357  infxr  45370  infleinflem1  45373  infleinflem2  45374  xralrple4  45376  xralrple3  45377  xrralrecnnle  45386  xrralrecnnge  45393  supxrunb3  45402  unb2ltle  45418  zxrd  45456  gtnelioc  45496  ltnelicc  45502  iooabslt  45504  gtnelicc  45505  eliooshift  45511  iocopn  45525  eliccelioc  45526  iooshift  45527  icoopn  45530  ge0lere  45537  iooiinicc  45547  sqrlearg  45558  iooiinioc  45561  uzinico  45564  preimaiocmnf  45565  uzubioo  45570  fsumge0cl  45578  limciccioolb  45626  lptioo1  45637  limcicciooub  45642  ltmod  45643  lptre2pt  45645  limsupre  45646  limcresiooub  45647  limcresioolb  45648  limcleqr  45649  limsupresico  45705  limsuppnfdlem  45706  limsupub  45709  limsupequzlem  45727  limsupre2lem  45729  limsupre3lem  45737  limsupvaluz2  45743  supcnvlimsup  45745  liminfresico  45776  limsup10exlem  45777  liminflelimsuplem  45780  limsupgtlem  45782  liminfval4  45794  liminfvaluz2  45800  limsupvaluz4  45805  liminflimsupclim  45812  xlimxrre  45836  xlimmnfvlem1  45837  xlimmnfv  45839  xlimpnfvlem1  45841  xlimpnfv  45843  sinaover2ne0  45873  ioccncflimc  45890  icccncfext  45892  icocncflimc  45894  cncfiooicclem1  45898  cncfiooicc  45899  cncfiooiccre  45900  cncfioobdlem  45901  dvbdfbdioolem1  45933  dvbdfbdioolem2  45934  dvbdfbdioo  45935  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc1  45938  ioodvbdlimc2lem  45939  ioodvbdlimc2  45940  ditgeqiooicc  45965  iblsplit  45971  itgcoscmulx  45974  ibliooicc  45976  iblspltprt  45978  itgsincmulx  45979  itgsubsticc  45981  itgioocnicc  45982  iblcncfioo  45983  itgspltprt  45984  itgiccshift  45985  volioore  45995  voliooico  45997  voliooicof  46001  voliccico  46004  stoweidlem34  46039  stoweidlem52  46057  stirlinglem5  46083  dirkercncflem1  46108  dirkercncflem4  46111  fourierdlem4  46116  fourierdlem10  46122  fourierdlem19  46131  fourierdlem20  46132  fourierdlem24  46136  fourierdlem25  46137  fourierdlem26  46138  fourierdlem27  46139  fourierdlem28  46140  fourierdlem31  46143  fourierdlem32  46144  fourierdlem33  46145  fourierdlem35  46147  fourierdlem37  46149  fourierdlem40  46152  fourierdlem41  46153  fourierdlem43  46155  fourierdlem44  46156  fourierdlem46  46157  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem52  46163  fourierdlem54  46165  fourierdlem57  46168  fourierdlem59  46170  fourierdlem60  46171  fourierdlem61  46172  fourierdlem62  46173  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem68  46179  fourierdlem69  46180  fourierdlem70  46181  fourierdlem72  46183  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem84  46195  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem92  46203  fourierdlem93  46204  fourierdlem94  46205  fourierdlem97  46208  fourierdlem100  46211  fourierdlem101  46212  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem109  46220  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fourierdlem114  46225  sqwvfoura  46233  fouriersw  46236  etransclem23  46262  etransclem46  46285  qndenserrnbllem  46299  rrxsnicc  46305  ioorrnopnlem  46309  ioorrnopnxrlem  46311  salgencntex  46348  sge0cl  46386  sge0fsum  46392  sge0iunmptlemre  46420  sge0isum  46432  sge0ad2en  46436  sge0xaddlem1  46438  sge0xaddlem2  46439  sge0reuz  46452  voliunsge0lem  46477  meassre  46482  omessre  46515  omeiunltfirp  46524  hoissre  46549  hoiprodcl  46552  ovnsubaddlem1  46575  hoiprodcl3  46585  hoidmvcl  46587  hsphoidmvle2  46590  hsphoidmvle  46591  sge0hsphoire  46594  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  ovnhoilem1  46606  ovnhoilem2  46607  ovnhoi  46608  ovnlecvr2  46615  hspdifhsp  46621  hoidifhspdmvle  46625  hoiqssbllem1  46627  hoiqssbllem2  46628  hoiqssbllem3  46629  hspmbllem1  46631  hspmbllem2  46632  volicorege0  46642  ovolval5lem1  46657  ovolval5lem2  46658  iinhoiicclem  46678  iinhoiicc  46679  iunhoiioolem  46680  iunhoiioo  46681  vonioolem2  46686  vonicclem2  46689  vonsn  46696  pimltmnf2f  46702  pimconstlt0  46706  pimgtpnf2f  46710  salpreimagelt  46712  salpreimalegt  46714  preimageiingt  46725  preimaleiinlt  46726  pimrecltneg  46729  issmflem  46732  issmflelem  46749  issmfgtlem  46760  issmfgt  46761  smfaddlem1  46768  issmfgelem  46774  issmfge  46775  smfpimioompt  46791  smfresal  46793  smfrec  46794  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  smfmullem4  46799  smfpimbor1lem1  46803  smfsuplem1  46816  smflimsuplem4  46828  smfliminflem  46835  smfdmmblpimne  46842  smfpimne  46844  smfpimne2  46845  fsupdm  46847  finfdm  46851  smfinfdmmbllem  46853  bgoldbtbnd  47814  eenglngeehlnmlem2  48731