Theorem rexrd 11340

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-xr 11328

This theorem is used by:  xnn0xr  12665  rpxr  13111  rpxrd  13146  max0sub  13307  qextltlem  13313  xralrple  13316  xnegcl  13324  xaddf  13335  xnn0lem1lt  13355  xnn0lenn0nn0  13356  xmulf  13383  xadddi  13406  xrub  13423  supxrre  13438  infxrre  13448  ixxub  13478  ixxlb  13479  ioo0  13482  ico0  13503  ioc0  13504  iooshf  13538  icoshftf1o  13586  supicc  13613  supiccub  13614  supicclub  13615  xnn0xrge0  13618  ssfzunsn  13684  addmodid  14042  hashnnn0genn0  14467  hashunsnggt  14518  sgnsub  15239  sgnmul  15240  sgnmulsgn  15242  elicc4abs  15467  caucvgrlem  15820  fprodge1  16142  pcxcl  17019  pcdvdsb  17027  pcaddlem  17046  ramcl2lem  17167  ramlb  17177  0ram  17178  setsstruct  17334  prdsxmetlem  24667  xblss2ps  24700  xblss2  24701  blss2ps  24702  blss2  24703  blhalf  24704  metustto  24852  metustexhalf  24855  nmoi  25027  nmoix  25028  nmoi2  25029  nmoleub  25030  qdensere  25068  cnblcld  25073  ioo2blex  25093  tgioo  25095  blcvx  25097  zcld  25113  recld2  25114  iccntr  25121  icccmplem1  25122  reconnlem1  25126  reconnlem2  25127  opnreen  25131  metnrmlem3  25161  icoopnst  25240  iocopnst  25241  cnheibor  25256  lebnumii  25267  nmoleub2lem  25415  lmnn  25564  iscau3  25579  minveclem4  25733  ivthlem1  25752  ivthlem2  25753  ivthlem3  25754  ivth2  25756  ivthle  25757  ivthle2  25758  ivthicc  25759  evthicc  25760  cniccbdd  25762  ovolgelb  25781  ovollb2lem  25789  ovolunlem1  25798  ovoliunlem1  25803  ovoliunlem2  25804  ovoliun  25806  ovolscalem1  25814  ovolicc1  25817  ovolicc2lem4  25821  ovolicc2lem5  25822  ovolicc2  25823  ovolicc  25824  nulmbl2  25837  voliunlem2  25852  ioombl1lem4  25862  ioorcl2  25873  uniioombllem1  25882  uniioombllem2a  25883  uniioombllem3  25886  dyaddisjlem  25896  dyadmaxlem  25898  opnmbllem  25902  volivth  25908  vitalilem4  25912  mbfmulc2lem  25948  mbfmax  25950  mbfposr  25953  ismbf3d  25955  mbfaddlem  25961  mbflimsup  25967  mbfi1fseqlem4  26019  itg2lcl  26028  xrge0f  26032  itg2itg1  26037  itg2const2  26042  itg2seq  26043  itg2uba  26044  itg2lea  26045  itg2mulclem  26047  itg2mulc  26048  itg2splitlem  26049  itg2split  26050  itg2monolem2  26052  itg2monolem3  26053  itg2mono  26054  itg2gt0  26061  itg2cnlem1  26062  itg2cnlem2  26063  itg2cn  26064  iblss  26105  itgle  26110  itgeqa  26114  itgioo  26116  ibladdlem  26120  iblabs  26129  iblabsr  26130  iblmulc2  26131  itgsplit  26136  itgspliticc  26137  itgsplitioo  26138  bddmulibl  26139  bddiblnc  26142  ditgcl  26158  ditgswap  26159  ditgsplitlem  26160  dvferm1lem  26284  dvferm2lem  26286  dvferm  26288  rollelem  26289  rolle  26290  cmvth  26291  mvth  26292  dvlip  26293  dvlip2  26295  c1liplem1  26296  c1lip1  26297  dveq0  26300  dvgt0lem1  26302  dvivthlem1  26308  dvivth  26310  lhop1lem  26313  lhop1  26314  lhop2  26315  lhop  26316  dvcnvrelem1  26317  dvcnvre  26319  dvcvx  26320  dvfsumle  26321  dvfsumge  26322  dvfsumabs  26323  dvfsumlem2  26327  dvfsumlem3  26328  dvfsumlem4  26329  dvfsumrlimge0  26330  dvfsumrlim2  26332  ftc1lem1  26335  ftc1lem2  26336  ftc1a  26337  ftc1lem4  26339  ftc2  26344  ftc2ditglem  26345  itgparts  26347  itgsubstlem  26348  itgsubst  26349  itgpowd  26350  degltlem1  26370  deg1ge  26396  coe1mul3  26397  deg1sublt  26408  deg1mul2  26412  deg1tmle  26416  deg1tm  26417  idomrootle  26471  plypf1  26511  taylfvallem1  26666  tayl0  26671  pserulm  26731  psercnlem1  26734  pserdvlem1  26736  pserdvlem2  26737  abelthlem3  26742  abelth  26750  efcvx  26758  logno1  26946  logtayl  26970  xrlimcnp  27278  logfacbnd3  27532  log2sumbnd  27853  pntpbnd2  27896  pntibndlem3  27901  ttgcontlem1  29444  nmooge0  31351  nmoub3i  31357  isblo3i  31385  ubthlem1  31454  minvecolem4  31464  nmopge0  32495  nmfnge0  32511  nmophmi  32615  branmfn  32689  sgnval2  33309  nn0mnfxrd  33325  xaddeq0  33327  xlt2addrd  33333  sgnmulsgp  33405  xmulcand  33469  xreceu  33470  xdivrec  33475  fsumrp0cl  33564  xrge0slmod  33891  ply1degltel  34108  ply1degleel  34109  ply1degltlss  34110  ply1degltdimlem  34236  ply1degltdim  34237  fldextrspundgdvdslem  34294  extdgfialglem1  34306  cos9thpiminplylem2  34397  cnre2csqlem  34524  tpr2rico  34526  xrge0iifcnv  34547  xrge0iifhom  34551  lmxrge0  34566  esumfsup  34684  esumpcvgval  34692  esumcvg  34700  dya2iocress  34889  dya2iocbrsiga  34890  dya2icobrsiga  34891  dya2icoseg  34892  dya2iocucvr  34899  sxbrsigalem2  34901  omssubaddlem  34914  omssubadd  34915  orvcgteel  35083  dstrvprob  35087  orvclteel  35088  signstcl  35177  signstf  35178  signstf0  35180  signstfvn  35181  signsvtn0  35182  signsvfn  35194  signsvfpn  35197  signsvfnn  35198  ftc2re  35210  cvmliftlem6  36024  cvmliftlem7  36025  cvmliftlem8  36026  cvmliftlem9  36027  cvmliftlem10  36028  cvmliftlem13  36030  ivthALT  37093  iooelexlt  38253  relowlssretop  38254  relowlpssretop  38255  sin2h  38501  cos2h  38502  tan2h  38503  poimirlem30  38536  poimir  38539  heicant  38541  opnmbllem0  38542  mblfinlem1  38543  mblfinlem2  38544  mblfinlem3  38545  mblfinlem4  38546  ismblfin  38547  itg2addnclem  38557  itg2addnclem2  38558  itg2gt0cn  38561  ibladdnclem  38562  iblabsnclem  38569  iblabsnc  38570  iblmulc2nc  38571  ftc1cnnclem  38577  ftc1anclem1  38579  ftc1anclem4  38582  ftc1anclem5  38583  ftc1anclem6  38584  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  ftc2nc  38588  areacirclem1  38594  areacirclem5  38598  areacirc  38599  isbnd3  38686  blbnd  38689  prdsbnd  38695  prdsbnd2  38697  cntotbnd  38698  dvrelog3  43083  0nonelalab  43085  dvrelogpow2b  43086  dvle2  43090  aks4d1p1p6  43091  aks4d1p1p5  43093  aks6d1c6lem3  43190  aks6d1c7lem2  43199  unitscyglem5  43217  idomodle  44151  imo72b2  45131  cvgdvgrat  45256  radcnvrat  45257  rfcnpre3  45993  rfcnpre4  45994  absfico  46174  nnxrd  46233  lefldiveq  46251  lttri5d  46258  supxrgere  46289  supxrgelem  46293  supxrge  46294  xralrple2  46310  infxr  46322  infleinflem1  46325  infleinflem2  46326  xralrple4  46328  xralrple3  46329  xrralrecnnle  46338  xrralrecnnge  46345  supxrunb3  46354  unb2ltle  46369  zxrd  46407  gtnelioc  46447  ltnelicc  46453  iooabslt  46455  gtnelicc  46456  eliooshift  46462  iocopn  46476  eliccelioc  46477  iooshift  46478  icoopn  46481  ge0lere  46488  iooiinicc  46498  sqrlearg  46509  iooiinioc  46512  uzinico  46515  preimaiocmnf  46516  uzubioo  46521  fsumge0cl  46529  limciccioolb  46577  lptioo1  46588  limcicciooub  46591  ltmod  46592  lptre2pt  46594  limsupre  46595  limcresiooub  46596  limcresioolb  46597  limcleqr  46598  limsupresico  46654  limsuppnfdlem  46655  limsupub  46658  limsupequzlem  46676  limsupre2lem  46678  limsupre3lem  46686  limsupvaluz2  46692  supcnvlimsup  46694  liminfresico  46725  limsup10exlem  46726  liminflelimsuplem  46729  limsupgtlem  46731  liminfval4  46743  liminfvaluz2  46749  limsupvaluz4  46754  liminflimsupclim  46761  xlimxrre  46785  xlimmnfvlem1  46786  xlimmnfv  46788  xlimpnfvlem1  46790  xlimpnfv  46792  sinaover2ne0  46822  ioccncflimc  46839  icccncfext  46841  icocncflimc  46843  cncfiooicclem1  46847  cncfiooicc  46848  cncfiooiccre  46849  cncfioobdlem  46850  dvbdfbdioolem1  46882  dvbdfbdioolem2  46883  dvbdfbdioo  46884  ioodvbdlimc1lem1  46885  ioodvbdlimc1lem2  46886  ioodvbdlimc1  46887  ioodvbdlimc2lem  46888  ioodvbdlimc2  46889  ditgeqiooicc  46914  iblsplit  46920  itgcoscmulx  46923  ibliooicc  46925  iblspltprt  46927  itgsincmulx  46928  itgsubsticc  46930  itgioocnicc  46931  iblcncfioo  46932  itgspltprt  46933  itgiccshift  46934  volioore  46944  voliooico  46946  voliooicof  46950  voliccico  46953  stoweidlem34  46988  stoweidlem52  47006  stirlinglem5  47032  dirkercncflem1  47057  dirkercncflem4  47060  fourierdlem4  47065  fourierdlem10  47071  fourierdlem19  47080  fourierdlem20  47081  fourierdlem24  47085  fourierdlem25  47086  fourierdlem26  47087  fourierdlem27  47088  fourierdlem28  47089  fourierdlem31  47092  fourierdlem32  47093  fourierdlem33  47094  fourierdlem35  47096  fourierdlem37  47098  fourierdlem40  47101  fourierdlem41  47102  fourierdlem43  47104  fourierdlem44  47105  fourierdlem46  47106  fourierdlem47  47107  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem51  47111  fourierdlem52  47112  fourierdlem54  47114  fourierdlem57  47117  fourierdlem59  47119  fourierdlem60  47120  fourierdlem61  47121  fourierdlem62  47122  fourierdlem63  47123  fourierdlem64  47124  fourierdlem65  47125  fourierdlem68  47128  fourierdlem69  47129  fourierdlem70  47130  fourierdlem72  47132  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem78  47138  fourierdlem79  47139  fourierdlem81  47141  fourierdlem82  47142  fourierdlem84  47144  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem92  47152  fourierdlem93  47153  fourierdlem94  47154  fourierdlem97  47157  fourierdlem100  47160  fourierdlem101  47161  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem107  47167  fourierdlem109  47169  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  fourierdlem114  47174  sqwvfoura  47182  fouriersw  47185  etransclem23  47211  etransclem46  47234  qndenserrnbllem  47248  rrxsnicc  47254  ioorrnopnlem  47258  ioorrnopnxrlem  47260  salgencntex  47297  sge0cl  47335  sge0fsum  47341  sge0iunmptlemre  47369  sge0isum  47381  sge0ad2en  47385  sge0xaddlem1  47387  sge0xaddlem2  47388  sge0reuz  47401  voliunsge0lem  47426  meassre  47431  omessre  47464  omeiunltfirp  47473  hoissre  47498  hoiprodcl  47501  ovnsubaddlem1  47524  hoiprodcl3  47534  hoidmvcl  47536  hsphoidmvle2  47539  hsphoidmvle  47540  sge0hsphoire  47543  hoidmv1lelem1  47545  hoidmv1lelem2  47546  hoidmv1lelem3  47547  hoidmv1le  47548  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  ovnhoilem1  47555  ovnhoilem2  47556  ovnhoi  47557  ovnlecvr2  47564  hspdifhsp  47570  hoidifhspdmvle  47574  hoiqssbllem1  47576  hoiqssbllem2  47577  hoiqssbllem3  47578  hspmbllem1  47580  hspmbllem2  47581  volicorege0  47591  ovolval5lem1  47606  ovolval5lem2  47607  iinhoiicclem  47627  iinhoiicc  47628  iunhoiioolem  47629  iunhoiioo  47630  vonioolem2  47635  vonicclem2  47638  vonsn  47645  pimltmnf2f  47651  pimconstlt0  47655  pimgtpnf2f  47659  salpreimagelt  47661  salpreimalegt  47663  preimageiingt  47674  preimaleiinlt  47675  pimrecltneg  47678  issmflem  47681  issmflelem  47698  issmfgtlem  47709  issmfgt  47710  smfaddlem1  47717  issmfgelem  47723  issmfge  47724  smfpimioompt  47740  smfresal  47742  smfrec  47743  smfmullem1  47745  smfmullem2  47746  smfmullem3  47747  smfmullem4  47748  smfpimbor1lem1  47752  smfsuplem1  47765  smflimsuplem4  47777  smfliminflem  47784  smfdmmblpimne  47791  smfpimne  47793  smfpimne2  47794  fsupdm  47796  finfdm  47800  smfinfdmmbllem  47802  bgoldbtbnd  48851  eenglngeehlnmlem2  49794