Theorem rexrd 11287

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11127  ℝ^*cxr 11270

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-xr 11275

This theorem is used by:  xnn0xr  12610  rpxr  13056  rpxrd  13091  max0sub  13252  qextltlem  13258  xralrple  13261  xnegcl  13269  xaddf  13280  xnn0lem1lt  13300  xnn0lenn0nn0  13301  xmulf  13328  xadddi  13351  xrub  13368  supxrre  13383  infxrre  13393  ixxub  13423  ixxlb  13424  ioo0  13427  ico0  13448  ioc0  13449  iooshf  13483  icoshftf1o  13531  supicc  13558  supiccub  13559  supicclub  13560  xnn0xrge0  13563  ssfzunsn  13629  addmodid  13987  hashnnn0genn0  14411  hashunsnggt  14462  sgnsub  15183  sgnmul  15184  sgnmulsgn  15186  elicc4abs  15411  caucvgrlem  15764  fprodge1  16088  pcxcl  16959  pcdvdsb  16967  pcaddlem  16986  ramcl2lem  17107  ramlb  17117  0ram  17118  setsstruct  17274  prdsxmetlem  24600  xblss2ps  24633  xblss2  24634  blss2ps  24635  blss2  24636  blhalf  24637  metustto  24785  metustexhalf  24788  nmoi  24960  nmoix  24961  nmoi2  24962  nmoleub  24963  qdensere  25001  cnblcld  25006  ioo2blex  25026  tgioo  25028  blcvx  25030  zcld  25046  recld2  25047  iccntr  25054  icccmplem1  25055  reconnlem1  25059  reconnlem2  25060  opnreen  25064  metnrmlem3  25094  icoopnst  25173  iocopnst  25174  cnheibor  25189  lebnumii  25200  nmoleub2lem  25348  lmnn  25497  iscau3  25512  minveclem4  25666  ivthlem1  25685  ivthlem2  25686  ivthlem3  25687  ivth2  25689  ivthle  25690  ivthle2  25691  ivthicc  25692  evthicc  25693  cniccbdd  25695  ovolgelb  25714  ovollb2lem  25722  ovolunlem1  25731  ovoliunlem1  25736  ovoliunlem2  25737  ovoliun  25739  ovolscalem1  25747  ovolicc1  25750  ovolicc2lem4  25754  ovolicc2lem5  25755  ovolicc2  25756  ovolicc  25757  nulmbl2  25770  voliunlem2  25785  ioombl1lem4  25795  ioorcl2  25806  uniioombllem1  25815  uniioombllem2a  25816  uniioombllem3  25819  dyaddisjlem  25829  dyadmaxlem  25831  opnmbllem  25835  volivth  25841  vitalilem4  25845  mbfmulc2lem  25881  mbfmax  25883  mbfposr  25886  ismbf3d  25888  mbfaddlem  25894  mbflimsup  25900  mbfi1fseqlem4  25952  itg2lcl  25961  xrge0f  25965  itg2itg1  25970  itg2const2  25975  itg2seq  25976  itg2uba  25977  itg2lea  25978  itg2mulclem  25980  itg2mulc  25981  itg2splitlem  25982  itg2split  25983  itg2monolem2  25985  itg2monolem3  25986  itg2mono  25987  itg2gt0  25994  itg2cnlem1  25995  itg2cnlem2  25996  itg2cn  25997  iblss  26039  itgle  26044  itgeqa  26048  itgioo  26050  ibladdlem  26054  iblabs  26063  iblabsr  26064  iblmulc2  26065  itgsplit  26070  itgspliticc  26071  itgsplitioo  26072  bddmulibl  26073  bddiblnc  26076  ditgcl  26092  ditgswap  26093  ditgsplitlem  26094  dvferm1lem  26218  dvferm2lem  26220  dvferm  26222  rollelem  26223  rolle  26224  cmvth  26225  mvth  26226  dvlip  26227  dvlip2  26229  c1liplem1  26230  c1lip1  26231  dveq0  26234  dvgt0lem1  26236  dvivthlem1  26242  dvivth  26244  lhop1lem  26247  lhop1  26248  lhop2  26249  lhop  26250  dvcnvrelem1  26251  dvcnvre  26253  dvcvx  26254  dvfsumle  26255  dvfsumge  26256  dvfsumabs  26257  dvfsumlem2  26261  dvfsumlem3  26262  dvfsumlem4  26263  dvfsumrlimge0  26264  dvfsumrlim2  26266  ftc1lem1  26269  ftc1lem2  26270  ftc1a  26271  ftc1lem4  26273  ftc2  26278  ftc2ditglem  26279  itgparts  26281  itgsubstlem  26282  itgsubst  26283  itgpowd  26284  degltlem1  26304  deg1ge  26330  coe1mul3  26331  deg1sublt  26342  deg1mul2  26346  deg1tmle  26350  deg1tm  26351  idomrootle  26405  plypf1  26445  taylfvallem1  26600  tayl0  26605  pserulm  26665  psercnlem1  26668  pserdvlem1  26670  pserdvlem2  26671  abelthlem3  26676  abelth  26684  efcvx  26692  logno1  26881  logtayl  26905  xrlimcnp  27213  logfacbnd3  27467  log2sumbnd  27788  pntpbnd2  27831  pntibndlem3  27836  ttgcontlem1  29349  nmooge0  31256  nmoub3i  31262  isblo3i  31290  ubthlem1  31359  minvecolem4  31369  nmopge0  32400  nmfnge0  32416  nmophmi  32520  branmfn  32594  sgnval2  33214  nn0mnfxrd  33230  xaddeq0  33232  xlt2addrd  33238  sgnmulsgp  33310  xmulcand  33374  xreceu  33375  xdivrec  33380  fsumrp0cl  33469  xrge0slmod  33796  ply1degltel  34012  ply1degleel  34013  ply1degltlss  34014  ply1degltdimlem  34140  ply1degltdim  34141  fldextrspundgdvdslem  34198  extdgfialglem1  34210  cos9thpiminplylem2  34301  cnre2csqlem  34428  tpr2rico  34430  xrge0iifcnv  34451  xrge0iifhom  34455  lmxrge0  34470  esumfsup  34588  esumpcvgval  34596  esumcvg  34604  dya2iocress  34793  dya2iocbrsiga  34794  dya2icobrsiga  34795  dya2icoseg  34796  dya2iocucvr  34803  sxbrsigalem2  34805  omssubaddlem  34818  omssubadd  34819  orvcgteel  34987  dstrvprob  34991  orvclteel  34992  signstcl  35081  signstf  35082  signstf0  35084  signstfvn  35085  signsvtn0  35086  signsvfn  35098  signsvfpn  35101  signsvfnn  35102  ftc2re  35114  cvmliftlem6  35877  cvmliftlem7  35878  cvmliftlem8  35879  cvmliftlem9  35880  cvmliftlem10  35881  cvmliftlem13  35883  ivthALT  36962  iooelexlt  38124  relowlssretop  38125  relowlpssretop  38126  sin2h  38372  cos2h  38373  tan2h  38374  poimirlem30  38407  poimir  38410  heicant  38412  opnmbllem0  38413  mblfinlem1  38414  mblfinlem2  38415  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  itg2addnclem  38428  itg2addnclem2  38429  itg2gt0cn  38432  ibladdnclem  38433  iblabsnclem  38440  iblabsnc  38441  iblmulc2nc  38442  ftc1cnnclem  38448  ftc1anclem1  38450  ftc1anclem4  38453  ftc1anclem5  38454  ftc1anclem6  38455  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  ftc2nc  38459  areacirclem1  38465  areacirclem5  38469  areacirc  38470  isbnd3  38542  blbnd  38545  prdsbnd  38551  prdsbnd2  38553  cntotbnd  38554  dvrelog3  42939  0nonelalab  42941  dvrelogpow2b  42942  dvle2  42946  aks4d1p1p6  42947  aks4d1p1p5  42949  aks6d1c6lem3  43046  aks6d1c7lem2  43055  unitscyglem5  43073  idomodle  44040  imo72b2  45020  cvgdvgrat  45145  radcnvrat  45146  rfcnpre3  45875  rfcnpre4  45876  absfico  46056  nnxrd  46115  lefldiveq  46133  lttri5d  46140  supxrgere  46171  supxrgelem  46175  supxrge  46176  xralrple2  46192  infxr  46204  infleinflem1  46207  infleinflem2  46208  xralrple4  46210  xralrple3  46211  xrralrecnnle  46220  xrralrecnnge  46227  supxrunb3  46236  unb2ltle  46251  zxrd  46289  gtnelioc  46329  ltnelicc  46335  iooabslt  46337  gtnelicc  46338  eliooshift  46344  iocopn  46358  eliccelioc  46359  iooshift  46360  icoopn  46363  ge0lere  46370  iooiinicc  46380  sqrlearg  46391  iooiinioc  46394  uzinico  46397  preimaiocmnf  46398  uzubioo  46403  fsumge0cl  46411  limciccioolb  46459  lptioo1  46470  limcicciooub  46473  ltmod  46474  lptre2pt  46476  limsupre  46477  limcresiooub  46478  limcresioolb  46479  limcleqr  46480  limsupresico  46536  limsuppnfdlem  46537  limsupub  46540  limsupequzlem  46558  limsupre2lem  46560  limsupre3lem  46568  limsupvaluz2  46574  supcnvlimsup  46576  liminfresico  46607  limsup10exlem  46608  liminflelimsuplem  46611  limsupgtlem  46613  liminfval4  46625  liminfvaluz2  46631  limsupvaluz4  46636  liminflimsupclim  46643  xlimxrre  46667  xlimmnfvlem1  46668  xlimmnfv  46670  xlimpnfvlem1  46672  xlimpnfv  46674  sinaover2ne0  46704  ioccncflimc  46721  icccncfext  46723  icocncflimc  46725  cncfiooicclem1  46729  cncfiooicc  46730  cncfiooiccre  46731  cncfioobdlem  46732  dvbdfbdioolem1  46764  dvbdfbdioolem2  46765  dvbdfbdioo  46766  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc1  46769  ioodvbdlimc2lem  46770  ioodvbdlimc2  46771  ditgeqiooicc  46796  iblsplit  46802  itgcoscmulx  46805  ibliooicc  46807  iblspltprt  46809  itgsincmulx  46810  itgsubsticc  46812  itgioocnicc  46813  iblcncfioo  46814  itgspltprt  46815  itgiccshift  46816  volioore  46826  voliooico  46828  voliooicof  46832  voliccico  46835  stoweidlem34  46870  stoweidlem52  46888  stirlinglem5  46914  dirkercncflem1  46939  dirkercncflem4  46942  fourierdlem4  46947  fourierdlem10  46953  fourierdlem19  46962  fourierdlem20  46963  fourierdlem24  46967  fourierdlem25  46968  fourierdlem26  46969  fourierdlem27  46970  fourierdlem28  46971  fourierdlem31  46974  fourierdlem32  46975  fourierdlem33  46976  fourierdlem35  46978  fourierdlem37  46980  fourierdlem40  46983  fourierdlem41  46984  fourierdlem43  46986  fourierdlem44  46987  fourierdlem46  46988  fourierdlem47  46989  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem51  46993  fourierdlem52  46994  fourierdlem54  46996  fourierdlem57  46999  fourierdlem59  47001  fourierdlem60  47002  fourierdlem61  47003  fourierdlem62  47004  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  fourierdlem68  47010  fourierdlem69  47011  fourierdlem70  47012  fourierdlem72  47014  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem78  47020  fourierdlem79  47021  fourierdlem81  47023  fourierdlem82  47024  fourierdlem84  47026  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem92  47034  fourierdlem93  47035  fourierdlem94  47036  fourierdlem97  47039  fourierdlem100  47042  fourierdlem101  47043  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem107  47049  fourierdlem109  47051  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  fourierdlem114  47056  sqwvfoura  47064  fouriersw  47067  etransclem23  47093  etransclem46  47116  qndenserrnbllem  47130  rrxsnicc  47136  ioorrnopnlem  47140  ioorrnopnxrlem  47142  salgencntex  47179  sge0cl  47217  sge0fsum  47223  sge0iunmptlemre  47251  sge0isum  47263  sge0ad2en  47267  sge0xaddlem1  47269  sge0xaddlem2  47270  sge0reuz  47283  voliunsge0lem  47308  meassre  47313  omessre  47346  omeiunltfirp  47355  hoissre  47380  hoiprodcl  47383  ovnsubaddlem1  47406  hoiprodcl3  47416  hoidmvcl  47418  hsphoidmvle2  47421  hsphoidmvle  47422  sge0hsphoire  47425  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmv1lelem3  47429  hoidmv1le  47430  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  ovnhoilem1  47437  ovnhoilem2  47438  ovnhoi  47439  ovnlecvr2  47446  hspdifhsp  47452  hoidifhspdmvle  47456  hoiqssbllem1  47458  hoiqssbllem2  47459  hoiqssbllem3  47460  hspmbllem1  47462  hspmbllem2  47463  volicorege0  47473  ovolval5lem1  47488  ovolval5lem2  47489  iinhoiicclem  47509  iinhoiicc  47510  iunhoiioolem  47511  iunhoiioo  47512  vonioolem2  47517  vonicclem2  47520  vonsn  47527  pimltmnf2f  47533  pimconstlt0  47537  pimgtpnf2f  47541  salpreimagelt  47543  salpreimalegt  47545  preimageiingt  47556  preimaleiinlt  47557  pimrecltneg  47560  issmflem  47563  issmflelem  47580  issmfgtlem  47591  issmfgt  47592  smfaddlem1  47599  issmfgelem  47605  issmfge  47606  smfpimioompt  47622  smfresal  47624  smfrec  47625  smfmullem1  47627  smfmullem2  47628  smfmullem3  47629  smfmullem4  47630  smfpimbor1lem1  47634  smfsuplem1  47647  smflimsuplem4  47659  smfliminflem  47666  smfdmmblpimne  47673  smfpimne  47675  smfpimne2  47676  fsupdm  47678  finfdm  47682  smfinfdmmbllem  47684  bgoldbtbnd  48733  eenglngeehlnmlem2  49676