Theorem rexrd 11260

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-xr 11248

This theorem is referenced by:  xnn0xr  12583  rpxr  13027  rpxrd  13062  max0sub  13223  qextltlem  13229  xralrple  13232  xnegcl  13240  xaddf  13251  xnn0lem1lt  13271  xnn0lenn0nn0  13272  xmulf  13299  xadddi  13322  xrub  13339  supxrre  13354  infxrre  13364  ixxub  13394  ixxlb  13395  ioo0  13398  ico0  13419  ioc0  13420  iooshf  13454  icoshftf1o  13502  supicc  13529  supiccub  13530  supicclub  13531  xnn0xrge0  13534  ssfzunsn  13600  addmodid  13957  hashnnn0genn0  14381  hashunsnggt  14432  sgnsub  15145  sgnmul  15146  sgnmulsgn  15148  elicc4abs  15373  caucvgrlem  15726  fprodge1  16051  pcxcl  16922  pcdvdsb  16930  pcaddlem  16949  ramcl2lem  17070  ramlb  17080  0ram  17081  setsstruct  17237  prdsxmetlem  24506  xblss2ps  24539  xblss2  24540  blss2ps  24541  blss2  24542  blhalf  24543  metustto  24691  metustexhalf  24694  nmoi  24866  nmoix  24867  nmoi2  24868  nmoleub  24869  qdensere  24907  cnblcld  24912  ioo2blex  24932  tgioo  24934  blcvx  24936  zcld  24952  recld2  24953  iccntr  24960  icccmplem1  24961  reconnlem1  24965  reconnlem2  24966  opnreen  24970  metnrmlem3  25000  icoopnst  25079  iocopnst  25080  cnheibor  25095  lebnumii  25106  nmoleub2lem  25254  lmnn  25403  iscau3  25418  minveclem4  25572  ivthlem1  25591  ivthlem2  25592  ivthlem3  25593  ivth2  25595  ivthle  25596  ivthle2  25597  ivthicc  25598  evthicc  25599  cniccbdd  25601  ovolgelb  25620  ovollb2lem  25628  ovolunlem1  25637  ovoliunlem1  25642  ovoliunlem2  25643  ovoliun  25645  ovolscalem1  25653  ovolicc1  25656  ovolicc2lem4  25660  ovolicc2lem5  25661  ovolicc2  25662  ovolicc  25663  nulmbl2  25676  voliunlem2  25691  ioombl1lem4  25701  ioorcl2  25712  uniioombllem1  25721  uniioombllem2a  25722  uniioombllem3  25725  dyaddisjlem  25735  dyadmaxlem  25737  opnmbllem  25741  volivth  25747  vitalilem4  25751  mbfmulc2lem  25787  mbfmax  25789  mbfposr  25792  ismbf3d  25794  mbfaddlem  25800  mbflimsup  25806  mbfi1fseqlem4  25858  itg2lcl  25867  xrge0f  25871  itg2itg1  25876  itg2const2  25881  itg2seq  25882  itg2uba  25883  itg2lea  25884  itg2mulclem  25886  itg2mulc  25887  itg2splitlem  25888  itg2split  25889  itg2monolem2  25891  itg2monolem3  25892  itg2mono  25893  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  itg2cn  25903  iblss  25945  itgle  25950  itgeqa  25954  itgioo  25956  ibladdlem  25960  iblabs  25969  iblabsr  25970  iblmulc2  25971  itgsplit  25976  itgspliticc  25977  itgsplitioo  25978  bddmulibl  25979  bddiblnc  25982  ditgcl  25998  ditgswap  25999  ditgsplitlem  26000  dvferm1lem  26124  dvferm2lem  26126  dvferm  26128  rollelem  26129  rolle  26130  cmvth  26131  mvth  26132  dvlip  26133  dvlip2  26135  c1liplem1  26136  c1lip1  26137  dveq0  26140  dvgt0lem1  26142  dvivthlem1  26148  dvivth  26150  lhop1lem  26153  lhop1  26154  lhop2  26155  lhop  26156  dvcnvrelem1  26157  dvcnvre  26159  dvcvx  26160  dvfsumle  26161  dvfsumge  26162  dvfsumabs  26163  dvfsumlem2  26167  dvfsumlem3  26168  dvfsumlem4  26169  dvfsumrlimge0  26170  dvfsumrlim2  26172  ftc1lem1  26175  ftc1lem2  26176  ftc1a  26177  ftc1lem4  26179  ftc2  26184  ftc2ditglem  26185  itgparts  26187  itgsubstlem  26188  itgsubst  26189  itgpowd  26190  degltlem1  26210  deg1ge  26236  coe1mul3  26237  deg1sublt  26248  deg1mul2  26252  deg1tmle  26256  deg1tm  26257  idomrootle  26311  plypf1  26350  taylfvallem1  26501  tayl0  26506  pserulm  26566  psercnlem1  26569  pserdvlem1  26571  pserdvlem2  26572  abelthlem3  26577  abelth  26585  efcvx  26593  logno1  26782  logtayl  26806  xrlimcnp  27114  logfacbnd3  27368  log2sumbnd  27689  pntpbnd2  27732  pntibndlem3  27737  ttgcontlem1  29215  nmooge0  31100  nmoub3i  31106  isblo3i  31134  ubthlem1  31203  minvecolem4  31213  nmopge0  32244  nmfnge0  32260  nmophmi  32364  branmfn  32438  sgnval2  33061  nn0mnfxrd  33077  xaddeq0  33079  xlt2addrd  33085  sgnmulsgp  33157  xmulcand  33221  xreceu  33222  xdivrec  33227  fsumrp0cl  33322  xrge0slmod  33649  ply1degltel  33865  ply1degleel  33866  ply1degltlss  33867  ply1degltdimlem  33993  ply1degltdim  33994  fldextrspundgdvdslem  34051  extdgfialglem1  34063  cos9thpiminplylem2  34154  cnre2csqlem  34281  tpr2rico  34283  xrge0iifcnv  34304  xrge0iifhom  34308  lmxrge0  34323  esumfsup  34441  esumpcvgval  34449  esumcvg  34457  dya2iocress  34645  dya2iocbrsiga  34646  dya2icobrsiga  34647  dya2icoseg  34648  dya2iocucvr  34655  sxbrsigalem2  34657  omssubaddlem  34670  omssubadd  34671  orvcgteel  34839  dstrvprob  34843  orvclteel  34844  signstcl  34933  signstf  34934  signstf0  34936  signstfvn  34937  signsvtn0  34938  signsvfn  34950  signsvfpn  34953  signsvfnn  34954  ftc2re  34966  cvmliftlem6  35763  cvmliftlem7  35764  cvmliftlem8  35765  cvmliftlem9  35766  cvmliftlem10  35767  cvmliftlem13  35769  ivthALT  36827  iooelexlt  37989  relowlssretop  37990  relowlpssretop  37991  sin2h  38242  cos2h  38243  tan2h  38244  poimirlem30  38282  poimir  38285  heicant  38287  opnmbllem0  38288  mblfinlem1  38289  mblfinlem2  38290  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  itg2addnclem  38303  itg2addnclem2  38304  itg2gt0cn  38307  ibladdnclem  38308  iblabsnclem  38315  iblabsnc  38316  iblmulc2nc  38317  ftc1cnnclem  38323  ftc1anclem1  38325  ftc1anclem4  38328  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  ftc2nc  38334  areacirclem1  38340  areacirclem5  38344  areacirc  38345  isbnd3  38416  blbnd  38419  prdsbnd  38425  prdsbnd2  38427  cntotbnd  38428  dvrelog3  42813  0nonelalab  42815  dvrelogpow2b  42816  dvle2  42820  aks4d1p1p6  42821  aks4d1p1p5  42823  aks6d1c6lem3  42920  aks6d1c7lem2  42929  unitscyglem5  42947  idomodle  43901  imo72b2  44881  cvgdvgrat  45006  radcnvrat  45007  rfcnpre3  45736  rfcnpre4  45737  absfico  45917  nnxrd  45976  lefldiveq  45994  lttri5d  46001  supxrgere  46032  supxrgelem  46036  supxrge  46037  xralrple2  46053  infxr  46065  infleinflem1  46068  infleinflem2  46069  xralrple4  46071  xralrple3  46072  xrralrecnnle  46081  xrralrecnnge  46088  supxrunb3  46097  unb2ltle  46112  zxrd  46150  gtnelioc  46190  ltnelicc  46196  iooabslt  46198  gtnelicc  46199  eliooshift  46205  iocopn  46219  eliccelioc  46220  iooshift  46221  icoopn  46224  ge0lere  46231  iooiinicc  46241  sqrlearg  46252  iooiinioc  46255  uzinico  46258  preimaiocmnf  46259  uzubioo  46264  fsumge0cl  46272  limciccioolb  46320  lptioo1  46331  limcicciooub  46334  ltmod  46335  lptre2pt  46337  limsupre  46338  limcresiooub  46339  limcresioolb  46340  limcleqr  46341  limsupresico  46397  limsuppnfdlem  46398  limsupub  46401  limsupequzlem  46419  limsupre2lem  46421  limsupre3lem  46429  limsupvaluz2  46435  supcnvlimsup  46437  liminfresico  46468  limsup10exlem  46469  liminflelimsuplem  46472  limsupgtlem  46474  liminfval4  46486  liminfvaluz2  46492  limsupvaluz4  46497  liminflimsupclim  46504  xlimxrre  46528  xlimmnfvlem1  46529  xlimmnfv  46531  xlimpnfvlem1  46533  xlimpnfv  46535  sinaover2ne0  46565  ioccncflimc  46582  icccncfext  46584  icocncflimc  46586  cncfiooicclem1  46590  cncfiooicc  46591  cncfiooiccre  46592  cncfioobdlem  46593  dvbdfbdioolem1  46625  dvbdfbdioolem2  46626  dvbdfbdioo  46627  ioodvbdlimc1lem1  46628  ioodvbdlimc1lem2  46629  ioodvbdlimc1  46630  ioodvbdlimc2lem  46631  ioodvbdlimc2  46632  ditgeqiooicc  46657  iblsplit  46663  itgcoscmulx  46666  ibliooicc  46668  iblspltprt  46670  itgsincmulx  46671  itgsubsticc  46673  itgioocnicc  46674  iblcncfioo  46675  itgspltprt  46676  itgiccshift  46677  volioore  46687  voliooico  46689  voliooicof  46693  voliccico  46696  stoweidlem34  46731  stoweidlem52  46749  stirlinglem5  46775  dirkercncflem1  46800  dirkercncflem4  46803  fourierdlem4  46808  fourierdlem10  46814  fourierdlem19  46823  fourierdlem20  46824  fourierdlem24  46828  fourierdlem25  46829  fourierdlem26  46830  fourierdlem27  46831  fourierdlem28  46832  fourierdlem31  46835  fourierdlem32  46836  fourierdlem33  46837  fourierdlem35  46839  fourierdlem37  46841  fourierdlem40  46844  fourierdlem41  46845  fourierdlem43  46847  fourierdlem44  46848  fourierdlem46  46849  fourierdlem47  46850  fourierdlem48  46851  fourierdlem49  46852  fourierdlem50  46853  fourierdlem51  46854  fourierdlem52  46855  fourierdlem54  46857  fourierdlem57  46860  fourierdlem59  46862  fourierdlem60  46863  fourierdlem61  46864  fourierdlem62  46865  fourierdlem63  46866  fourierdlem64  46867  fourierdlem65  46868  fourierdlem68  46871  fourierdlem69  46872  fourierdlem70  46873  fourierdlem72  46875  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem78  46881  fourierdlem79  46882  fourierdlem81  46884  fourierdlem82  46885  fourierdlem84  46887  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem92  46895  fourierdlem93  46896  fourierdlem94  46897  fourierdlem97  46900  fourierdlem100  46903  fourierdlem101  46904  fourierdlem102  46905  fourierdlem103  46906  fourierdlem104  46907  fourierdlem107  46910  fourierdlem109  46912  fourierdlem111  46914  fourierdlem112  46915  fourierdlem113  46916  fourierdlem114  46917  sqwvfoura  46925  fouriersw  46928  etransclem23  46954  etransclem46  46977  qndenserrnbllem  46991  rrxsnicc  46997  ioorrnopnlem  47001  ioorrnopnxrlem  47003  salgencntex  47040  sge0cl  47078  sge0fsum  47084  sge0iunmptlemre  47112  sge0isum  47124  sge0ad2en  47128  sge0xaddlem1  47130  sge0xaddlem2  47131  sge0reuz  47144  voliunsge0lem  47169  meassre  47174  omessre  47207  omeiunltfirp  47216  hoissre  47241  hoiprodcl  47244  ovnsubaddlem1  47267  hoiprodcl3  47277  hoidmvcl  47279  hsphoidmvle2  47282  hsphoidmvle  47283  sge0hsphoire  47286  hoidmv1lelem1  47288  hoidmv1lelem2  47289  hoidmv1lelem3  47290  hoidmv1le  47291  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvlelem4  47295  ovnhoilem1  47298  ovnhoilem2  47299  ovnhoi  47300  ovnlecvr2  47307  hspdifhsp  47313  hoidifhspdmvle  47317  hoiqssbllem1  47319  hoiqssbllem2  47320  hoiqssbllem3  47321  hspmbllem1  47323  hspmbllem2  47324  volicorege0  47334  ovolval5lem1  47349  ovolval5lem2  47350  iinhoiicclem  47370  iinhoiicc  47371  iunhoiioolem  47372  iunhoiioo  47373  vonioolem2  47378  vonicclem2  47381  vonsn  47388  pimltmnf2f  47394  pimconstlt0  47398  pimgtpnf2f  47402  salpreimagelt  47404  salpreimalegt  47406  preimageiingt  47417  preimaleiinlt  47418  pimrecltneg  47421  issmflem  47424  issmflelem  47441  issmfgtlem  47452  issmfgt  47453  smfaddlem1  47460  issmfgelem  47466  issmfge  47467  smfpimioompt  47483  smfresal  47485  smfrec  47486  smfmullem1  47488  smfmullem2  47489  smfmullem3  47490  smfmullem4  47491  smfpimbor1lem1  47495  smfsuplem1  47508  smflimsuplem4  47520  smfliminflem  47527  smfdmmblpimne  47534  smfpimne  47536  smfpimne2  47537  fsupdm  47539  finfdm  47543  smfinfdmmbllem  47545  bgoldbtbnd  48557  eenglngeehlnmlem2  49501