Theorem rexrd 11277

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  ℝ^*cxr 11260

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-xr 11265

This theorem is used by:  xnn0xr  12600  rpxr  13044  rpxrd  13079  max0sub  13240  qextltlem  13246  xralrple  13249  xnegcl  13257  xaddf  13268  xnn0lem1lt  13288  xnn0lenn0nn0  13289  xmulf  13316  xadddi  13339  xrub  13356  supxrre  13371  infxrre  13381  ixxub  13411  ixxlb  13412  ioo0  13415  ico0  13436  ioc0  13437  iooshf  13471  icoshftf1o  13519  supicc  13546  supiccub  13547  supicclub  13548  xnn0xrge0  13551  ssfzunsn  13617  addmodid  13975  hashnnn0genn0  14399  hashunsnggt  14450  sgnsub  15169  sgnmul  15170  sgnmulsgn  15172  elicc4abs  15397  caucvgrlem  15750  fprodge1  16075  pcxcl  16946  pcdvdsb  16954  pcaddlem  16973  ramcl2lem  17094  ramlb  17104  0ram  17105  setsstruct  17261  prdsxmetlem  24562  xblss2ps  24595  xblss2  24596  blss2ps  24597  blss2  24598  blhalf  24599  metustto  24747  metustexhalf  24750  nmoi  24922  nmoix  24923  nmoi2  24924  nmoleub  24925  qdensere  24963  cnblcld  24968  ioo2blex  24988  tgioo  24990  blcvx  24992  zcld  25008  recld2  25009  iccntr  25016  icccmplem1  25017  reconnlem1  25021  reconnlem2  25022  opnreen  25026  metnrmlem3  25056  icoopnst  25135  iocopnst  25136  cnheibor  25151  lebnumii  25162  nmoleub2lem  25310  lmnn  25459  iscau3  25474  minveclem4  25628  ivthlem1  25647  ivthlem2  25648  ivthlem3  25649  ivth2  25651  ivthle  25652  ivthle2  25653  ivthicc  25654  evthicc  25655  cniccbdd  25657  ovolgelb  25676  ovollb2lem  25684  ovolunlem1  25693  ovoliunlem1  25698  ovoliunlem2  25699  ovoliun  25701  ovolscalem1  25709  ovolicc1  25712  ovolicc2lem4  25716  ovolicc2lem5  25717  ovolicc2  25718  ovolicc  25719  nulmbl2  25732  voliunlem2  25747  ioombl1lem4  25757  ioorcl2  25768  uniioombllem1  25777  uniioombllem2a  25778  uniioombllem3  25781  dyaddisjlem  25791  dyadmaxlem  25793  opnmbllem  25797  volivth  25803  vitalilem4  25807  mbfmulc2lem  25843  mbfmax  25845  mbfposr  25848  ismbf3d  25850  mbfaddlem  25856  mbflimsup  25862  mbfi1fseqlem4  25914  itg2lcl  25923  xrge0f  25927  itg2itg1  25932  itg2const2  25937  itg2seq  25938  itg2uba  25939  itg2lea  25940  itg2mulclem  25942  itg2mulc  25943  itg2splitlem  25944  itg2split  25945  itg2monolem2  25947  itg2monolem3  25948  itg2mono  25949  itg2gt0  25956  itg2cnlem1  25957  itg2cnlem2  25958  itg2cn  25959  iblss  26001  itgle  26006  itgeqa  26010  itgioo  26012  ibladdlem  26016  iblabs  26025  iblabsr  26026  iblmulc2  26027  itgsplit  26032  itgspliticc  26033  itgsplitioo  26034  bddmulibl  26035  bddiblnc  26038  ditgcl  26054  ditgswap  26055  ditgsplitlem  26056  dvferm1lem  26180  dvferm2lem  26182  dvferm  26184  rollelem  26185  rolle  26186  cmvth  26187  mvth  26188  dvlip  26189  dvlip2  26191  c1liplem1  26192  c1lip1  26193  dveq0  26196  dvgt0lem1  26198  dvivthlem1  26204  dvivth  26206  lhop1lem  26209  lhop1  26210  lhop2  26211  lhop  26212  dvcnvrelem1  26213  dvcnvre  26215  dvcvx  26216  dvfsumle  26217  dvfsumge  26218  dvfsumabs  26219  dvfsumlem2  26223  dvfsumlem3  26224  dvfsumlem4  26225  dvfsumrlimge0  26226  dvfsumrlim2  26228  ftc1lem1  26231  ftc1lem2  26232  ftc1a  26233  ftc1lem4  26235  ftc2  26240  ftc2ditglem  26241  itgparts  26243  itgsubstlem  26244  itgsubst  26245  itgpowd  26246  degltlem1  26266  deg1ge  26292  coe1mul3  26293  deg1sublt  26304  deg1mul2  26308  deg1tmle  26312  deg1tm  26313  idomrootle  26367  plypf1  26406  taylfvallem1  26557  tayl0  26562  pserulm  26622  psercnlem1  26625  pserdvlem1  26627  pserdvlem2  26628  abelthlem3  26633  abelth  26641  efcvx  26649  logno1  26838  logtayl  26862  xrlimcnp  27170  logfacbnd3  27424  log2sumbnd  27745  pntpbnd2  27788  pntibndlem3  27793  ttgcontlem1  29271  nmooge0  31156  nmoub3i  31162  isblo3i  31190  ubthlem1  31259  minvecolem4  31269  nmopge0  32300  nmfnge0  32316  nmophmi  32420  branmfn  32494  sgnval2  33117  nn0mnfxrd  33133  xaddeq0  33135  xlt2addrd  33141  sgnmulsgp  33213  xmulcand  33277  xreceu  33278  xdivrec  33283  fsumrp0cl  33372  xrge0slmod  33699  ply1degltel  33915  ply1degleel  33916  ply1degltlss  33917  ply1degltdimlem  34043  ply1degltdim  34044  fldextrspundgdvdslem  34101  extdgfialglem1  34113  cos9thpiminplylem2  34204  cnre2csqlem  34331  tpr2rico  34333  xrge0iifcnv  34354  xrge0iifhom  34358  lmxrge0  34373  esumfsup  34491  esumpcvgval  34499  esumcvg  34507  dya2iocress  34696  dya2iocbrsiga  34697  dya2icobrsiga  34698  dya2icoseg  34699  dya2iocucvr  34706  sxbrsigalem2  34708  omssubaddlem  34721  omssubadd  34722  orvcgteel  34890  dstrvprob  34894  orvclteel  34895  signstcl  34984  signstf  34985  signstf0  34987  signstfvn  34988  signsvtn0  34989  signsvfn  35001  signsvfpn  35004  signsvfnn  35005  ftc2re  35017  cvmliftlem6  35803  cvmliftlem7  35804  cvmliftlem8  35805  cvmliftlem9  35806  cvmliftlem10  35807  cvmliftlem13  35809  ivthALT  36887  iooelexlt  38049  relowlssretop  38050  relowlpssretop  38051  sin2h  38302  cos2h  38303  tan2h  38304  poimirlem30  38342  poimir  38345  heicant  38347  opnmbllem0  38348  mblfinlem1  38349  mblfinlem2  38350  mblfinlem3  38351  mblfinlem4  38352  ismblfin  38353  itg2addnclem  38363  itg2addnclem2  38364  itg2gt0cn  38367  ibladdnclem  38368  iblabsnclem  38375  iblabsnc  38376  iblmulc2nc  38377  ftc1cnnclem  38383  ftc1anclem1  38385  ftc1anclem4  38388  ftc1anclem5  38389  ftc1anclem6  38390  ftc1anclem7  38391  ftc1anclem8  38392  ftc1anc  38393  ftc2nc  38394  areacirclem1  38400  areacirclem5  38404  areacirc  38405  isbnd3  38476  blbnd  38479  prdsbnd  38485  prdsbnd2  38487  cntotbnd  38488  dvrelog3  42873  0nonelalab  42875  dvrelogpow2b  42876  dvle2  42880  aks4d1p1p6  42881  aks4d1p1p5  42883  aks6d1c6lem3  42980  aks6d1c7lem2  42989  unitscyglem5  43007  idomodle  43959  imo72b2  44939  cvgdvgrat  45064  radcnvrat  45065  rfcnpre3  45794  rfcnpre4  45795  absfico  45975  nnxrd  46034  lefldiveq  46052  lttri5d  46059  supxrgere  46090  supxrgelem  46094  supxrge  46095  xralrple2  46111  infxr  46123  infleinflem1  46126  infleinflem2  46127  xralrple4  46129  xralrple3  46130  xrralrecnnle  46139  xrralrecnnge  46146  supxrunb3  46155  unb2ltle  46170  zxrd  46208  gtnelioc  46248  ltnelicc  46254  iooabslt  46256  gtnelicc  46257  eliooshift  46263  iocopn  46277  eliccelioc  46278  iooshift  46279  icoopn  46282  ge0lere  46289  iooiinicc  46299  sqrlearg  46310  iooiinioc  46313  uzinico  46316  preimaiocmnf  46317  uzubioo  46322  fsumge0cl  46330  limciccioolb  46378  lptioo1  46389  limcicciooub  46392  ltmod  46393  lptre2pt  46395  limsupre  46396  limcresiooub  46397  limcresioolb  46398  limcleqr  46399  limsupresico  46455  limsuppnfdlem  46456  limsupub  46459  limsupequzlem  46477  limsupre2lem  46479  limsupre3lem  46487  limsupvaluz2  46493  supcnvlimsup  46495  liminfresico  46526  limsup10exlem  46527  liminflelimsuplem  46530  limsupgtlem  46532  liminfval4  46544  liminfvaluz2  46550  limsupvaluz4  46555  liminflimsupclim  46562  xlimxrre  46586  xlimmnfvlem1  46587  xlimmnfv  46589  xlimpnfvlem1  46591  xlimpnfv  46593  sinaover2ne0  46623  ioccncflimc  46640  icccncfext  46642  icocncflimc  46644  cncfiooicclem1  46648  cncfiooicc  46649  cncfiooiccre  46650  cncfioobdlem  46651  dvbdfbdioolem1  46683  dvbdfbdioolem2  46684  dvbdfbdioo  46685  ioodvbdlimc1lem1  46686  ioodvbdlimc1lem2  46687  ioodvbdlimc1  46688  ioodvbdlimc2lem  46689  ioodvbdlimc2  46690  ditgeqiooicc  46715  iblsplit  46721  itgcoscmulx  46724  ibliooicc  46726  iblspltprt  46728  itgsincmulx  46729  itgsubsticc  46731  itgioocnicc  46732  iblcncfioo  46733  itgspltprt  46734  itgiccshift  46735  volioore  46745  voliooico  46747  voliooicof  46751  voliccico  46754  stoweidlem34  46789  stoweidlem52  46807  stirlinglem5  46833  dirkercncflem1  46858  dirkercncflem4  46861  fourierdlem4  46866  fourierdlem10  46872  fourierdlem19  46881  fourierdlem20  46882  fourierdlem24  46886  fourierdlem25  46887  fourierdlem26  46888  fourierdlem27  46889  fourierdlem28  46890  fourierdlem31  46893  fourierdlem32  46894  fourierdlem33  46895  fourierdlem35  46897  fourierdlem37  46899  fourierdlem40  46902  fourierdlem41  46903  fourierdlem43  46905  fourierdlem44  46906  fourierdlem46  46907  fourierdlem47  46908  fourierdlem48  46909  fourierdlem49  46910  fourierdlem50  46911  fourierdlem51  46912  fourierdlem52  46913  fourierdlem54  46915  fourierdlem57  46918  fourierdlem59  46920  fourierdlem60  46921  fourierdlem61  46922  fourierdlem62  46923  fourierdlem63  46924  fourierdlem64  46925  fourierdlem65  46926  fourierdlem68  46929  fourierdlem69  46930  fourierdlem70  46931  fourierdlem72  46933  fourierdlem73  46934  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem78  46939  fourierdlem79  46940  fourierdlem81  46942  fourierdlem82  46943  fourierdlem84  46945  fourierdlem89  46950  fourierdlem90  46951  fourierdlem91  46952  fourierdlem92  46953  fourierdlem93  46954  fourierdlem94  46955  fourierdlem97  46958  fourierdlem100  46961  fourierdlem101  46962  fourierdlem102  46963  fourierdlem103  46964  fourierdlem104  46965  fourierdlem107  46968  fourierdlem109  46970  fourierdlem111  46972  fourierdlem112  46973  fourierdlem113  46974  fourierdlem114  46975  sqwvfoura  46983  fouriersw  46986  etransclem23  47012  etransclem46  47035  qndenserrnbllem  47049  rrxsnicc  47055  ioorrnopnlem  47059  ioorrnopnxrlem  47061  salgencntex  47098  sge0cl  47136  sge0fsum  47142  sge0iunmptlemre  47170  sge0isum  47182  sge0ad2en  47186  sge0xaddlem1  47188  sge0xaddlem2  47189  sge0reuz  47202  voliunsge0lem  47227  meassre  47232  omessre  47265  omeiunltfirp  47274  hoissre  47299  hoiprodcl  47302  ovnsubaddlem1  47325  hoiprodcl3  47335  hoidmvcl  47337  hsphoidmvle2  47340  hsphoidmvle  47341  sge0hsphoire  47344  hoidmv1lelem1  47346  hoidmv1lelem2  47347  hoidmv1lelem3  47348  hoidmv1le  47349  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem4  47353  ovnhoilem1  47356  ovnhoilem2  47357  ovnhoi  47358  ovnlecvr2  47365  hspdifhsp  47371  hoidifhspdmvle  47375  hoiqssbllem1  47377  hoiqssbllem2  47378  hoiqssbllem3  47379  hspmbllem1  47381  hspmbllem2  47382  volicorege0  47392  ovolval5lem1  47407  ovolval5lem2  47408  iinhoiicclem  47428  iinhoiicc  47429  iunhoiioolem  47430  iunhoiioo  47431  vonioolem2  47436  vonicclem2  47439  vonsn  47446  pimltmnf2f  47452  pimconstlt0  47456  pimgtpnf2f  47460  salpreimagelt  47462  salpreimalegt  47464  preimageiingt  47475  preimaleiinlt  47476  pimrecltneg  47479  issmflem  47482  issmflelem  47499  issmfgtlem  47510  issmfgt  47511  smfaddlem1  47518  issmfgelem  47524  issmfge  47525  smfpimioompt  47541  smfresal  47543  smfrec  47544  smfmullem1  47546  smfmullem2  47547  smfmullem3  47548  smfmullem4  47549  smfpimbor1lem1  47553  smfsuplem1  47566  smflimsuplem4  47578  smfliminflem  47585  smfdmmblpimne  47592  smfpimne  47594  smfpimne2  47595  fsupdm  47597  finfdm  47601  smfinfdmmbllem  47603  bgoldbtbnd  48615  eenglngeehlnmlem2  49559