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  28173  nmooge0  30051  nmoub3i  30057  isblo3i  30085  ubthlem1  30154  minvecolem4  30164  nmopge0  31195  nmfnge0  31211  nmophmi  31315  branmfn  31389  xaddeq0  31997  xlt2addrd  32002  xmulcand  32118  xreceu  32119  xdivrec  32124  fsumrp0cl  32227  xrge0slmod  32494  ply1degltel  32697  ply1degltlss  32698  ply1degltdimlem  32738  ply1degltdim  32739  cnre2csqlem  32921  tpr2rico  32923  xrge0iifcnv  32944  xrge0iifhom  32948  lmxrge0  32963  esumfsup  33099  esumpcvgval  33107  esumcvg  33115  dya2iocress  33304  dya2iocbrsiga  33305  dya2icobrsiga  33306  dya2icoseg  33307  dya2iocucvr  33314  sxbrsigalem2  33316  omssubaddlem  33329  omssubadd  33330  orvcgteel  33497  dstrvprob  33501  orvclteel  33502  sgnmul  33572  sgnsub  33574  sgnmulsgn  33579  sgnmulsgp  33580  signstcl  33607  signstf  33608  signstf0  33610  signstfvn  33611  signsvtn0  33612  signsvfn  33624  signsvfpn  33627  signsvfnn  33628  ftc2re  33641  cvmliftlem6  34312  cvmliftlem7  34313  cvmliftlem8  34314  cvmliftlem9  34315  cvmliftlem10  34316  cvmliftlem13  34318  gg-cmvth  35212  gg-dvfsumle  35213  gg-dvfsumlem2  35214  ivthALT  35268  iooelexlt  36291  relowlssretop  36292  relowlpssretop  36293  sin2h  36526  cos2h  36527  tan2h  36528  poimirlem30  36566  poimir  36569  heicant  36571  opnmbllem0  36572  mblfinlem1  36573  mblfinlem2  36574  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  itg2addnclem  36587  itg2addnclem2  36588  itg2gt0cn  36591  ibladdnclem  36592  iblabsnclem  36599  iblabsnc  36600  iblmulc2nc  36601  ftc1cnnclem  36607  ftc1anclem1  36609  ftc1anclem4  36612  ftc1anclem5  36613  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anclem8  36616  ftc1anc  36617  ftc2nc  36618  areacirclem1  36624  areacirclem5  36628  areacirc  36629  isbnd3  36700  blbnd  36703  prdsbnd  36709  prdsbnd2  36711  cntotbnd  36712  dvrelog3  40978  0nonelalab  40980  dvrelogpow2b  40981  dvle2  40985  aks4d1p1p6  40986  aks4d1p1p5  40988  idomrootle  41985  idomodle  41986  imo72b2  42972  cvgdvgrat  43120  radcnvrat  43121  rfcnpre3  43765  rfcnpre4  43766  absfico  43965  nnxrd  44031  lefldiveq  44050  lttri5d  44057  supxrgere  44091  supxrgelem  44095  supxrge  44096  xralrple2  44112  infxr  44125  infleinflem1  44128  infleinflem2  44129  xralrple4  44131  xralrple3  44132  xrralrecnnle  44141  xrralrecnnge  44148  supxrunb3  44157  unb2ltle  44173  zxrd  44211  gtnelioc  44252  ltnelicc  44258  iooabslt  44260  gtnelicc  44261  eliooshift  44267  iocopn  44281  eliccelioc  44282  iooshift  44283  icoopn  44286  ge0lere  44293  iooiinicc  44303  sqrlearg  44314  iooiinioc  44317  uzinico  44321  preimaiocmnf  44322  uzubioo  44328  fsumge0cl  44337  limciccioolb  44385  lptioo1  44396  limcicciooub  44401  ltmod  44402  lptre2pt  44404  limsupre  44405  limcresiooub  44406  limcresioolb  44407  limcleqr  44408  limsupresico  44464  limsuppnfdlem  44465  limsupub  44468  limsupequzlem  44486  limsupre2lem  44488  limsupre3lem  44496  limsupvaluz2  44502  supcnvlimsup  44504  liminfresico  44535  limsup10exlem  44536  liminflelimsuplem  44539  limsupgtlem  44541  liminfval4  44553  liminfvaluz2  44559  limsupvaluz4  44564  liminflimsupclim  44571  xlimxrre  44595  xlimmnfvlem1  44596  xlimmnfv  44598  xlimpnfvlem1  44600  xlimpnfv  44602  sinaover2ne0  44632  ioccncflimc  44649  icccncfext  44651  icocncflimc  44653  cncfiooicclem1  44657  cncfiooicc  44658  cncfiooiccre  44659  cncfioobdlem  44660  dvbdfbdioolem1  44692  dvbdfbdioolem2  44693  dvbdfbdioo  44694  ioodvbdlimc1lem1  44695  ioodvbdlimc1lem2  44696  ioodvbdlimc1  44697  ioodvbdlimc2lem  44698  ioodvbdlimc2  44699  ditgeqiooicc  44724  iblsplit  44730  itgcoscmulx  44733  ibliooicc  44735  iblspltprt  44737  itgsincmulx  44738  itgsubsticc  44740  itgioocnicc  44741  iblcncfioo  44742  itgspltprt  44743  itgiccshift  44744  volioore  44754  voliooico  44756  voliooicof  44760  voliccico  44763  stoweidlem34  44798  stoweidlem52  44816  stirlinglem5  44842  dirkercncflem1  44867  dirkercncflem4  44870  fourierdlem4  44875  fourierdlem10  44881  fourierdlem19  44890  fourierdlem20  44891  fourierdlem24  44895  fourierdlem25  44896  fourierdlem26  44897  fourierdlem27  44898  fourierdlem28  44899  fourierdlem31  44902  fourierdlem32  44903  fourierdlem33  44904  fourierdlem35  44906  fourierdlem37  44908  fourierdlem40  44911  fourierdlem41  44912  fourierdlem43  44914  fourierdlem44  44915  fourierdlem46  44916  fourierdlem47  44917  fourierdlem48  44918  fourierdlem49  44919  fourierdlem50  44920  fourierdlem51  44921  fourierdlem52  44922  fourierdlem54  44924  fourierdlem57  44927  fourierdlem59  44929  fourierdlem60  44930  fourierdlem61  44931  fourierdlem62  44932  fourierdlem63  44933  fourierdlem64  44934  fourierdlem65  44935  fourierdlem68  44938  fourierdlem69  44939  fourierdlem70  44940  fourierdlem72  44942  fourierdlem73  44943  fourierdlem74  44944  fourierdlem75  44945  fourierdlem76  44946  fourierdlem78  44948  fourierdlem79  44949  fourierdlem81  44951  fourierdlem82  44952  fourierdlem84  44954  fourierdlem89  44959  fourierdlem90  44960  fourierdlem91  44961  fourierdlem92  44962  fourierdlem93  44963  fourierdlem94  44964  fourierdlem97  44967  fourierdlem100  44970  fourierdlem101  44971  fourierdlem102  44972  fourierdlem103  44973  fourierdlem104  44974  fourierdlem107  44977  fourierdlem109  44979  fourierdlem111  44981  fourierdlem112  44982  fourierdlem113  44983  fourierdlem114  44984  sqwvfoura  44992  fouriersw  44995  etransclem23  45021  etransclem46  45044  qndenserrnbllem  45058  rrxsnicc  45064  ioorrnopnlem  45068  ioorrnopnxrlem  45070  salgencntex  45107  sge0cl  45145  sge0fsum  45151  sge0iunmptlemre  45179  sge0isum  45191  sge0ad2en  45195  sge0xaddlem1  45197  sge0xaddlem2  45198  sge0reuz  45211  voliunsge0lem  45236  meassre  45241  omessre  45274  omeiunltfirp  45283  hoissre  45308  hoiprodcl  45311  ovnsubaddlem1  45334  hoiprodcl3  45344  hoidmvcl  45346  hsphoidmvle2  45349  hsphoidmvle  45350  sge0hsphoire  45353  hoidmv1lelem1  45355  hoidmv1lelem2  45356  hoidmv1lelem3  45357  hoidmv1le  45358  hoidmvlelem1  45359  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvlelem4  45362  ovnhoilem1  45365  ovnhoilem2  45366  ovnhoi  45367  ovnlecvr2  45374  hspdifhsp  45380  hoidifhspdmvle  45384  hoiqssbllem1  45386  hoiqssbllem2  45387  hoiqssbllem3  45388  hspmbllem1  45390  hspmbllem2  45391  volicorege0  45401  ovolval5lem1  45416  ovolval5lem2  45417  iinhoiicclem  45437  iinhoiicc  45438  iunhoiioolem  45439  iunhoiioo  45440  vonioolem2  45445  vonicclem2  45448  vonsn  45455  pimltmnf2f  45461  pimconstlt0  45465  pimgtpnf2f  45469  salpreimagelt  45471  salpreimalegt  45473  preimageiingt  45484  preimaleiinlt  45485  pimrecltneg  45488  issmflem  45491  issmflelem  45508  issmfgtlem  45519  issmfgt  45520  smfaddlem1  45527  issmfgelem  45533  issmfge  45534  smfpimioompt  45550  smfresal  45552  smfrec  45553  smfmullem1  45555  smfmullem2  45556  smfmullem3  45557  smfmullem4  45558  smfpimbor1lem1  45562  smfsuplem1  45575  smflimsuplem4  45587  smfliminflem  45594  smfdmmblpimne  45601  smfpimne  45603  smfpimne2  45604  fsupdm  45606  finfdm  45610  smfinfdmmbllem  45612  bgoldbtbnd  46525  eenglngeehlnmlem2  47472