Theorem rexrd 11293

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11136  ℝ^*cxr 11276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-un 3936  df-ss 3948  df-xr 11281

This theorem is referenced by:  xnn0xr  12587  rpxr  13026  rpxrd  13060  max0sub  13220  qextltlem  13226  xralrple  13229  xnegcl  13237  xaddf  13248  xnn0lem1lt  13268  xnn0lenn0nn0  13269  xmulf  13296  xadddi  13319  xrub  13336  supxrre  13351  infxrre  13360  ixxub  13390  ixxlb  13391  ioo0  13394  ico0  13415  ioc0  13416  iooshf  13448  icoshftf1o  13496  supicc  13523  supiccub  13524  supicclub  13525  xnn0xrge0  13528  ssfzunsn  13592  addmodid  13942  hashnnn0genn0  14365  hashunsnggt  14416  elicc4abs  15341  caucvgrlem  15692  fprodge1  16014  pcxcl  16882  pcdvdsb  16890  pcaddlem  16909  ramcl2lem  17030  ramlb  17040  0ram  17041  setsstruct  17196  prdsxmetlem  24324  xblss2ps  24357  xblss2  24358  blss2ps  24359  blss2  24360  blhalf  24361  metustto  24511  metustexhalf  24514  nmoi  24686  nmoix  24687  nmoi2  24688  nmoleub  24689  qdensere  24727  cnblcld  24732  ioo2blex  24752  tgioo  24754  blcvx  24756  zcld  24772  recld2  24773  iccntr  24780  icccmplem1  24781  reconnlem1  24785  reconnlem2  24786  opnreen  24790  metnrmlem3  24820  icoopnst  24906  iocopnst  24907  cnheibor  24924  lebnumii  24935  nmoleub2lem  25084  lmnn  25234  iscau3  25249  minveclem4  25403  ivthlem1  25423  ivthlem2  25424  ivthlem3  25425  ivth2  25427  ivthle  25428  ivthle2  25429  ivthicc  25430  evthicc  25431  cniccbdd  25433  ovolgelb  25452  ovollb2lem  25460  ovolunlem1  25469  ovoliunlem1  25474  ovoliunlem2  25475  ovoliun  25477  ovolscalem1  25485  ovolicc1  25488  ovolicc2lem4  25492  ovolicc2lem5  25493  ovolicc2  25494  ovolicc  25495  nulmbl2  25508  voliunlem2  25523  ioombl1lem4  25533  ioorcl2  25544  uniioombllem1  25553  uniioombllem2a  25554  uniioombllem3  25557  dyaddisjlem  25567  dyadmaxlem  25569  opnmbllem  25573  volivth  25579  vitalilem4  25583  mbfmulc2lem  25619  mbfmax  25621  mbfposr  25624  ismbf3d  25626  mbfaddlem  25632  mbflimsup  25638  mbfi1fseqlem4  25690  itg2lcl  25699  xrge0f  25703  itg2itg1  25708  itg2const2  25713  itg2seq  25714  itg2uba  25715  itg2lea  25716  itg2mulclem  25718  itg2mulc  25719  itg2splitlem  25720  itg2split  25721  itg2monolem2  25723  itg2monolem3  25724  itg2mono  25725  itg2gt0  25732  itg2cnlem1  25733  itg2cnlem2  25734  itg2cn  25735  iblss  25777  itgle  25782  itgeqa  25786  itgioo  25788  ibladdlem  25792  iblabs  25801  iblabsr  25802  iblmulc2  25803  itgsplit  25808  itgspliticc  25809  itgsplitioo  25810  bddmulibl  25811  bddiblnc  25814  ditgcl  25830  ditgswap  25831  ditgsplitlem  25832  dvferm1lem  25959  dvferm2lem  25961  dvferm  25963  rollelem  25964  rolle  25965  cmvth  25966  cmvthOLD  25967  mvth  25968  dvlip  25969  dvlip2  25971  c1liplem1  25972  c1lip1  25973  dveq0  25976  dvgt0lem1  25978  dvivthlem1  25984  dvivth  25986  lhop1lem  25989  lhop1  25990  lhop2  25991  lhop  25992  dvcnvrelem1  25993  dvcnvre  25995  dvcvx  25996  dvfsumle  25997  dvfsumleOLD  25998  dvfsumge  25999  dvfsumabs  26000  dvfsumlem2  26004  dvfsumlem2OLD  26005  dvfsumlem3  26006  dvfsumlem4  26007  dvfsumrlimge0  26008  dvfsumrlim2  26010  ftc1lem1  26013  ftc1lem2  26014  ftc1a  26015  ftc1lem4  26017  ftc2  26022  ftc2ditglem  26023  itgparts  26025  itgsubstlem  26026  itgsubst  26027  itgpowd  26028  degltlem1  26048  deg1ge  26074  coe1mul3  26075  deg1sublt  26086  deg1mul2  26090  deg1tmle  26094  deg1tm  26095  idomrootle  26149  plypf1  26188  taylfvallem1  26335  tayl0  26340  pserulm  26402  psercnlem1  26406  pserdvlem1  26408  pserdvlem2  26409  abelthlem3  26414  abelth  26422  efcvx  26430  logno1  26615  logtayl  26639  xrlimcnp  26948  logfacbnd3  27204  log2sumbnd  27525  pntpbnd2  27568  pntibndlem3  27573  ttgcontlem1  28831  nmooge0  30715  nmoub3i  30721  isblo3i  30749  ubthlem1  30818  minvecolem4  30828  nmopge0  31859  nmfnge0  31875  nmophmi  31979  branmfn  32053  xaddeq0  32698  xlt2addrd  32704  xmulcand  32848  xreceu  32849  xdivrec  32854  fsumrp0cl  32970  xrge0slmod  33316  ply1degltel  33555  ply1degleel  33556  ply1degltlss  33557  ply1degltdimlem  33613  ply1degltdim  33614  fldextrspundgdvdslem  33672  cnre2csqlem  33884  tpr2rico  33886  xrge0iifcnv  33907  xrge0iifhom  33911  lmxrge0  33926  esumfsup  34046  esumpcvgval  34054  esumcvg  34062  dya2iocress  34251  dya2iocbrsiga  34252  dya2icobrsiga  34253  dya2icoseg  34254  dya2iocucvr  34261  sxbrsigalem2  34263  omssubaddlem  34276  omssubadd  34277  orvcgteel  34445  dstrvprob  34449  orvclteel  34450  sgnmul  34520  sgnsub  34522  sgnmulsgn  34527  sgnmulsgp  34528  signstcl  34555  signstf  34556  signstf0  34558  signstfvn  34559  signsvtn0  34560  signsvfn  34572  signsvfpn  34575  signsvfnn  34576  ftc2re  34588  cvmliftlem6  35270  cvmliftlem7  35271  cvmliftlem8  35272  cvmliftlem9  35273  cvmliftlem10  35274  cvmliftlem13  35276  ivthALT  36311  iooelexlt  37338  relowlssretop  37339  relowlpssretop  37340  sin2h  37592  cos2h  37593  tan2h  37594  poimirlem30  37632  poimir  37635  heicant  37637  opnmbllem0  37638  mblfinlem1  37639  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  itg2addnclem  37653  itg2addnclem2  37654  itg2gt0cn  37657  ibladdnclem  37658  iblabsnclem  37665  iblabsnc  37666  iblmulc2nc  37667  ftc1cnnclem  37673  ftc1anclem1  37675  ftc1anclem4  37678  ftc1anclem5  37679  ftc1anclem6  37680  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  ftc2nc  37684  areacirclem1  37690  areacirclem5  37694  areacirc  37695  isbnd3  37766  blbnd  37769  prdsbnd  37775  prdsbnd2  37777  cntotbnd  37778  dvrelog3  42041  0nonelalab  42043  dvrelogpow2b  42044  dvle2  42048  aks4d1p1p6  42049  aks4d1p1p5  42051  aks6d1c6lem3  42148  aks6d1c7lem2  42157  unitscyglem5  42175  idomodle  43181  imo72b2  44162  cvgdvgrat  44304  radcnvrat  44305  rfcnpre3  45010  rfcnpre4  45011  absfico  45195  nnxrd  45257  lefldiveq  45276  lttri5d  45283  supxrgere  45316  supxrgelem  45320  supxrge  45321  xralrple2  45337  infxr  45350  infleinflem1  45353  infleinflem2  45354  xralrple4  45356  xralrple3  45357  xrralrecnnle  45366  xrralrecnnge  45373  supxrunb3  45382  unb2ltle  45398  zxrd  45436  gtnelioc  45476  ltnelicc  45482  iooabslt  45484  gtnelicc  45485  eliooshift  45491  iocopn  45505  eliccelioc  45506  iooshift  45507  icoopn  45510  ge0lere  45517  iooiinicc  45527  sqrlearg  45538  iooiinioc  45541  uzinico  45545  preimaiocmnf  45546  uzubioo  45552  fsumge0cl  45560  limciccioolb  45608  lptioo1  45619  limcicciooub  45624  ltmod  45625  lptre2pt  45627  limsupre  45628  limcresiooub  45629  limcresioolb  45630  limcleqr  45631  limsupresico  45687  limsuppnfdlem  45688  limsupub  45691  limsupequzlem  45709  limsupre2lem  45711  limsupre3lem  45719  limsupvaluz2  45725  supcnvlimsup  45727  liminfresico  45758  limsup10exlem  45759  liminflelimsuplem  45762  limsupgtlem  45764  liminfval4  45776  liminfvaluz2  45782  limsupvaluz4  45787  liminflimsupclim  45794  xlimxrre  45818  xlimmnfvlem1  45819  xlimmnfv  45821  xlimpnfvlem1  45823  xlimpnfv  45825  sinaover2ne0  45855  ioccncflimc  45872  icccncfext  45874  icocncflimc  45876  cncfiooicclem1  45880  cncfiooicc  45881  cncfiooiccre  45882  cncfioobdlem  45883  dvbdfbdioolem1  45915  dvbdfbdioolem2  45916  dvbdfbdioo  45917  ioodvbdlimc1lem1  45918  ioodvbdlimc1lem2  45919  ioodvbdlimc1  45920  ioodvbdlimc2lem  45921  ioodvbdlimc2  45922  ditgeqiooicc  45947  iblsplit  45953  itgcoscmulx  45956  ibliooicc  45958  iblspltprt  45960  itgsincmulx  45961  itgsubsticc  45963  itgioocnicc  45964  iblcncfioo  45965  itgspltprt  45966  itgiccshift  45967  volioore  45977  voliooico  45979  voliooicof  45983  voliccico  45986  stoweidlem34  46021  stoweidlem52  46039  stirlinglem5  46065  dirkercncflem1  46090  dirkercncflem4  46093  fourierdlem4  46098  fourierdlem10  46104  fourierdlem19  46113  fourierdlem20  46114  fourierdlem24  46118  fourierdlem25  46119  fourierdlem26  46120  fourierdlem27  46121  fourierdlem28  46122  fourierdlem31  46125  fourierdlem32  46126  fourierdlem33  46127  fourierdlem35  46129  fourierdlem37  46131  fourierdlem40  46134  fourierdlem41  46135  fourierdlem43  46137  fourierdlem44  46138  fourierdlem46  46139  fourierdlem47  46140  fourierdlem48  46141  fourierdlem49  46142  fourierdlem50  46143  fourierdlem51  46144  fourierdlem52  46145  fourierdlem54  46147  fourierdlem57  46150  fourierdlem59  46152  fourierdlem60  46153  fourierdlem61  46154  fourierdlem62  46155  fourierdlem63  46156  fourierdlem64  46157  fourierdlem65  46158  fourierdlem68  46161  fourierdlem69  46162  fourierdlem70  46163  fourierdlem72  46165  fourierdlem73  46166  fourierdlem74  46167  fourierdlem75  46168  fourierdlem76  46169  fourierdlem78  46171  fourierdlem79  46172  fourierdlem81  46174  fourierdlem82  46175  fourierdlem84  46177  fourierdlem89  46182  fourierdlem90  46183  fourierdlem91  46184  fourierdlem92  46185  fourierdlem93  46186  fourierdlem94  46187  fourierdlem97  46190  fourierdlem100  46193  fourierdlem101  46194  fourierdlem102  46195  fourierdlem103  46196  fourierdlem104  46197  fourierdlem107  46200  fourierdlem109  46202  fourierdlem111  46204  fourierdlem112  46205  fourierdlem113  46206  fourierdlem114  46207  sqwvfoura  46215  fouriersw  46218  etransclem23  46244  etransclem46  46267  qndenserrnbllem  46281  rrxsnicc  46287  ioorrnopnlem  46291  ioorrnopnxrlem  46293  salgencntex  46330  sge0cl  46368  sge0fsum  46374  sge0iunmptlemre  46402  sge0isum  46414  sge0ad2en  46418  sge0xaddlem1  46420  sge0xaddlem2  46421  sge0reuz  46434  voliunsge0lem  46459  meassre  46464  omessre  46497  omeiunltfirp  46506  hoissre  46531  hoiprodcl  46534  ovnsubaddlem1  46557  hoiprodcl3  46567  hoidmvcl  46569  hsphoidmvle2  46572  hsphoidmvle  46573  sge0hsphoire  46576  hoidmv1lelem1  46578  hoidmv1lelem2  46579  hoidmv1lelem3  46580  hoidmv1le  46581  hoidmvlelem1  46582  hoidmvlelem2  46583  hoidmvlelem3  46584  hoidmvlelem4  46585  ovnhoilem1  46588  ovnhoilem2  46589  ovnhoi  46590  ovnlecvr2  46597  hspdifhsp  46603  hoidifhspdmvle  46607  hoiqssbllem1  46609  hoiqssbllem2  46610  hoiqssbllem3  46611  hspmbllem1  46613  hspmbllem2  46614  volicorege0  46624  ovolval5lem1  46639  ovolval5lem2  46640  iinhoiicclem  46660  iinhoiicc  46661  iunhoiioolem  46662  iunhoiioo  46663  vonioolem2  46668  vonicclem2  46671  vonsn  46678  pimltmnf2f  46684  pimconstlt0  46688  pimgtpnf2f  46692  salpreimagelt  46694  salpreimalegt  46696  preimageiingt  46707  preimaleiinlt  46708  pimrecltneg  46711  issmflem  46714  issmflelem  46731  issmfgtlem  46742  issmfgt  46743  smfaddlem1  46750  issmfgelem  46756  issmfge  46757  smfpimioompt  46773  smfresal  46775  smfrec  46776  smfmullem1  46778  smfmullem2  46779  smfmullem3  46780  smfmullem4  46781  smfpimbor1lem1  46785  smfsuplem1  46798  smflimsuplem4  46810  smfliminflem  46817  smfdmmblpimne  46824  smfpimne  46826  smfpimne2  46827  fsupdm  46829  finfdm  46833  smfinfdmmbllem  46835  bgoldbtbnd  47769  eenglngeehlnmlem2  48632