Theorem rexrd 11264

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  ℝ^*cxr 11247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-xr 11252

This theorem is referenced by:  xnn0xr  12549  rpxr  12983  rpxrd  13017  max0sub  13175  qextltlem  13181  xralrple  13184  xnegcl  13192  xaddf  13203  xnn0lem1lt  13223  xnn0lenn0nn0  13224  xmulf  13251  xadddi  13274  xrub  13291  supxrre  13306  infxrre  13315  ixxub  13345  ixxlb  13346  ioo0  13349  ico0  13370  ioc0  13371  iooshf  13403  icoshftf1o  13451  supicc  13478  supiccub  13479  supicclub  13480  xnn0xrge0  13483  ssfzunsn  13547  addmodid  13884  hashnnn0genn0  14303  hashunsnggt  14354  elicc4abs  15266  caucvgrlem  15619  fprodge1  15939  pcxcl  16794  pcdvdsb  16802  pcaddlem  16821  ramcl2lem  16942  ramlb  16952  0ram  16953  setsstruct  17109  prdsxmetlem  23874  xblss2ps  23907  xblss2  23908  blss2ps  23909  blss2  23910  blhalf  23911  metustto  24062  metustexhalf  24065  nmoi  24245  nmoix  24246  nmoi2  24247  nmoleub  24248  qdensere  24286  cnblcld  24291  ioo2blex  24310  tgioo  24312  blcvx  24314  zcld  24329  recld2  24330  iccntr  24337  icccmplem1  24338  reconnlem1  24342  reconnlem2  24343  opnreen  24347  metnrmlem3  24377  icoopnst  24455  iocopnst  24456  cnheibor  24471  lebnumii  24482  nmoleub2lem  24630  lmnn  24780  iscau3  24795  minveclem4  24949  ivthlem1  24968  ivthlem2  24969  ivthlem3  24970  ivth2  24972  ivthle  24973  ivthle2  24974  ivthicc  24975  evthicc  24976  cniccbdd  24978  ovolgelb  24997  ovollb2lem  25005  ovolunlem1  25014  ovoliunlem1  25019  ovoliunlem2  25020  ovoliun  25022  ovolscalem1  25030  ovolicc1  25033  ovolicc2lem4  25037  ovolicc2lem5  25038  ovolicc2  25039  ovolicc  25040  nulmbl2  25053  voliunlem2  25068  ioombl1lem4  25078  ioorcl2  25089  uniioombllem1  25098  uniioombllem2a  25099  uniioombllem3  25102  dyaddisjlem  25112  dyadmaxlem  25114  opnmbllem  25118  volivth  25124  vitalilem4  25128  mbfmulc2lem  25164  mbfmax  25166  mbfposr  25169  ismbf3d  25171  mbfaddlem  25177  mbflimsup  25183  mbfi1fseqlem4  25236  itg2lcl  25245  xrge0f  25249  itg2itg1  25254  itg2const2  25259  itg2seq  25260  itg2uba  25261  itg2lea  25262  itg2mulclem  25264  itg2mulc  25265  itg2splitlem  25266  itg2split  25267  itg2monolem2  25269  itg2monolem3  25270  itg2mono  25271  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  itg2cn  25281  iblss  25322  itgle  25327  itgeqa  25331  itgioo  25333  ibladdlem  25337  iblabs  25346  iblabsr  25347  iblmulc2  25348  itgsplit  25353  itgspliticc  25354  itgsplitioo  25355  bddmulibl  25356  bddiblnc  25359  ditgcl  25375  ditgswap  25376  ditgsplitlem  25377  dvferm1lem  25501  dvferm2lem  25503  dvferm  25505  rollelem  25506  rolle  25507  cmvth  25508  mvth  25509  dvlip  25510  dvlip2  25512  c1liplem1  25513  c1lip1  25514  dveq0  25517  dvgt0lem1  25519  dvivthlem1  25525  dvivth  25527  lhop1lem  25530  lhop1  25531  lhop2  25532  lhop  25533  dvcnvrelem1  25534  dvcnvre  25536  dvcvx  25537  dvfsumle  25538  dvfsumge  25539  dvfsumabs  25540  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlimge0  25547  dvfsumrlim2  25549  ftc1lem1  25552  ftc1lem2  25553  ftc1a  25554  ftc1lem4  25556  ftc2  25561  ftc2ditglem  25562  itgparts  25564  itgsubstlem  25565  itgsubst  25566  itgpowd  25567  degltlem1  25590  deg1ge  25616  coe1mul3  25617  deg1sublt  25628  deg1mul2  25632  deg1tmle  25635  deg1tm  25636  plypf1  25726  taylfvallem1  25869  tayl0  25874  pserulm  25934  psercnlem1  25937  pserdvlem1  25939  pserdvlem2  25940  abelthlem3  25945  abelth  25953  efcvx  25961  logno1  26144  logtayl  26168  xrlimcnp  26473  logfacbnd3  26726  log2sumbnd  27047  pntpbnd2  27090  pntibndlem3  27095  ttgcontlem1  28142  nmooge0  30020  nmoub3i  30026  isblo3i  30054  ubthlem1  30123  minvecolem4  30133  nmopge0  31164  nmfnge0  31180  nmophmi  31284  branmfn  31358  xaddeq0  31966  xlt2addrd  31971  xmulcand  32087  xreceu  32088  xdivrec  32093  fsumrp0cl  32196  xrge0slmod  32463  ply1degltel  32666  ply1degltlss  32667  ply1degltdimlem  32707  ply1degltdim  32708  cnre2csqlem  32890  tpr2rico  32892  xrge0iifcnv  32913  xrge0iifhom  32917  lmxrge0  32932  esumfsup  33068  esumpcvgval  33076  esumcvg  33084  dya2iocress  33273  dya2iocbrsiga  33274  dya2icobrsiga  33275  dya2icoseg  33276  dya2iocucvr  33283  sxbrsigalem2  33285  omssubaddlem  33298  omssubadd  33299  orvcgteel  33466  dstrvprob  33470  orvclteel  33471  sgnmul  33541  sgnsub  33543  sgnmulsgn  33548  sgnmulsgp  33549  signstcl  33576  signstf  33577  signstf0  33579  signstfvn  33580  signsvtn0  33581  signsvfn  33593  signsvfpn  33596  signsvfnn  33597  ftc2re  33610  cvmliftlem6  34281  cvmliftlem7  34282  cvmliftlem8  34283  cvmliftlem9  34284  cvmliftlem10  34285  cvmliftlem13  34287  gg-cmvth  35181  gg-dvfsumle  35182  gg-dvfsumlem2  35183  ivthALT  35220  iooelexlt  36243  relowlssretop  36244  relowlpssretop  36245  sin2h  36478  cos2h  36479  tan2h  36480  poimirlem30  36518  poimir  36521  heicant  36523  opnmbllem0  36524  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnclem  36539  itg2addnclem2  36540  itg2gt0cn  36543  ibladdnclem  36544  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  ftc1cnnclem  36559  ftc1anclem1  36561  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  ftc2nc  36570  areacirclem1  36576  areacirclem5  36580  areacirc  36581  isbnd3  36652  blbnd  36655  prdsbnd  36661  prdsbnd2  36663  cntotbnd  36664  dvrelog3  40930  0nonelalab  40932  dvrelogpow2b  40933  dvle2  40937  aks4d1p1p6  40938  aks4d1p1p5  40940  idomrootle  41937  idomodle  41938  imo72b2  42924  cvgdvgrat  43072  radcnvrat  43073  rfcnpre3  43717  rfcnpre4  43718  absfico  43917  nnxrd  43983  lefldiveq  44002  lttri5d  44009  supxrgere  44043  supxrgelem  44047  supxrge  44048  xralrple2  44064  infxr  44077  infleinflem1  44080  infleinflem2  44081  xralrple4  44083  xralrple3  44084  xrralrecnnle  44093  xrralrecnnge  44100  supxrunb3  44109  unb2ltle  44125  zxrd  44163  gtnelioc  44204  ltnelicc  44210  iooabslt  44212  gtnelicc  44213  eliooshift  44219  iocopn  44233  eliccelioc  44234  iooshift  44235  icoopn  44238  ge0lere  44245  iooiinicc  44255  sqrlearg  44266  iooiinioc  44269  uzinico  44273  preimaiocmnf  44274  uzubioo  44280  fsumge0cl  44289  limciccioolb  44337  lptioo1  44348  limcicciooub  44353  ltmod  44354  lptre2pt  44356  limsupre  44357  limcresiooub  44358  limcresioolb  44359  limcleqr  44360  limsupresico  44416  limsuppnfdlem  44417  limsupub  44420  limsupequzlem  44438  limsupre2lem  44440  limsupre3lem  44448  limsupvaluz2  44454  supcnvlimsup  44456  liminfresico  44487  limsup10exlem  44488  liminflelimsuplem  44491  limsupgtlem  44493  liminfval4  44505  liminfvaluz2  44511  limsupvaluz4  44516  liminflimsupclim  44523  xlimxrre  44547  xlimmnfvlem1  44548  xlimmnfv  44550  xlimpnfvlem1  44552  xlimpnfv  44554  sinaover2ne0  44584  ioccncflimc  44601  icccncfext  44603  icocncflimc  44605  cncfiooicclem1  44609  cncfiooicc  44610  cncfiooiccre  44611  cncfioobdlem  44612  dvbdfbdioolem1  44644  dvbdfbdioolem2  44645  dvbdfbdioo  44646  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc1  44649  ioodvbdlimc2lem  44650  ioodvbdlimc2  44651  ditgeqiooicc  44676  iblsplit  44682  itgcoscmulx  44685  ibliooicc  44687  iblspltprt  44689  itgsincmulx  44690  itgsubsticc  44692  itgioocnicc  44693  iblcncfioo  44694  itgspltprt  44695  itgiccshift  44696  volioore  44706  voliooico  44708  voliooicof  44712  voliccico  44715  stoweidlem34  44750  stoweidlem52  44768  stirlinglem5  44794  dirkercncflem1  44819  dirkercncflem4  44822  fourierdlem4  44827  fourierdlem10  44833  fourierdlem19  44842  fourierdlem20  44843  fourierdlem24  44847  fourierdlem25  44848  fourierdlem26  44849  fourierdlem27  44850  fourierdlem28  44851  fourierdlem31  44854  fourierdlem32  44855  fourierdlem33  44856  fourierdlem35  44858  fourierdlem37  44860  fourierdlem40  44863  fourierdlem41  44864  fourierdlem43  44866  fourierdlem44  44867  fourierdlem46  44868  fourierdlem47  44869  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem52  44874  fourierdlem54  44876  fourierdlem57  44879  fourierdlem59  44881  fourierdlem60  44882  fourierdlem61  44883  fourierdlem62  44884  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem68  44890  fourierdlem69  44891  fourierdlem70  44892  fourierdlem72  44894  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem84  44906  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem92  44914  fourierdlem93  44915  fourierdlem94  44916  fourierdlem97  44919  fourierdlem100  44922  fourierdlem101  44923  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem107  44929  fourierdlem109  44931  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  fourierdlem114  44936  sqwvfoura  44944  fouriersw  44947  etransclem23  44973  etransclem46  44996  qndenserrnbllem  45010  rrxsnicc  45016  ioorrnopnlem  45020  ioorrnopnxrlem  45022  salgencntex  45059  sge0cl  45097  sge0fsum  45103  sge0iunmptlemre  45131  sge0isum  45143  sge0ad2en  45147  sge0xaddlem1  45149  sge0xaddlem2  45150  sge0reuz  45163  voliunsge0lem  45188  meassre  45193  omessre  45226  omeiunltfirp  45235  hoissre  45260  hoiprodcl  45263  ovnsubaddlem1  45286  hoiprodcl3  45296  hoidmvcl  45298  hsphoidmvle2  45301  hsphoidmvle  45302  sge0hsphoire  45305  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  ovnhoilem1  45317  ovnhoilem2  45318  ovnhoi  45319  ovnlecvr2  45326  hspdifhsp  45332  hoidifhspdmvle  45336  hoiqssbllem1  45338  hoiqssbllem2  45339  hoiqssbllem3  45340  hspmbllem1  45342  hspmbllem2  45343  volicorege0  45353  ovolval5lem1  45368  ovolval5lem2  45369  iinhoiicclem  45389  iinhoiicc  45390  iunhoiioolem  45391  iunhoiioo  45392  vonioolem2  45397  vonicclem2  45400  vonsn  45407  pimltmnf2f  45413  pimconstlt0  45417  pimgtpnf2f  45421  salpreimagelt  45423  salpreimalegt  45425  preimageiingt  45436  preimaleiinlt  45437  pimrecltneg  45440  issmflem  45443  issmflelem  45460  issmfgtlem  45471  issmfgt  45472  smfaddlem1  45479  issmfgelem  45485  issmfge  45486  smfpimioompt  45502  smfresal  45504  smfrec  45505  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509  smfmullem4  45510  smfpimbor1lem1  45514  smfsuplem1  45527  smflimsuplem4  45539  smfliminflem  45546  smfdmmblpimne  45553  smfpimne  45555  smfpimne2  45556  fsupdm  45558  finfdm  45562  smfinfdmmbllem  45564  bgoldbtbnd  46477  eenglngeehlnmlem2  47424