Theorem rexrd 11171

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11014  ℝ^*cxr 11154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-xr 11159

This theorem is referenced by:  xnn0xr  12468  rpxr  12904  rpxrd  12939  max0sub  13099  qextltlem  13105  xralrple  13108  xnegcl  13116  xaddf  13127  xnn0lem1lt  13147  xnn0lenn0nn0  13148  xmulf  13175  xadddi  13198  xrub  13215  supxrre  13230  infxrre  13240  ixxub  13270  ixxlb  13271  ioo0  13274  ico0  13295  ioc0  13296  iooshf  13330  icoshftf1o  13378  supicc  13405  supiccub  13406  supicclub  13407  xnn0xrge0  13410  ssfzunsn  13474  addmodid  13830  hashnnn0genn0  14254  hashunsnggt  14305  elicc4abs  15231  caucvgrlem  15584  fprodge1  15906  pcxcl  16777  pcdvdsb  16785  pcaddlem  16804  ramcl2lem  16925  ramlb  16935  0ram  16936  setsstruct  17091  prdsxmetlem  24286  xblss2ps  24319  xblss2  24320  blss2ps  24321  blss2  24322  blhalf  24323  metustto  24471  metustexhalf  24474  nmoi  24646  nmoix  24647  nmoi2  24648  nmoleub  24649  qdensere  24687  cnblcld  24692  ioo2blex  24712  tgioo  24714  blcvx  24716  zcld  24732  recld2  24733  iccntr  24740  icccmplem1  24741  reconnlem1  24745  reconnlem2  24746  opnreen  24750  metnrmlem3  24780  icoopnst  24866  iocopnst  24867  cnheibor  24884  lebnumii  24895  nmoleub2lem  25044  lmnn  25193  iscau3  25208  minveclem4  25362  ivthlem1  25382  ivthlem2  25383  ivthlem3  25384  ivth2  25386  ivthle  25387  ivthle2  25388  ivthicc  25389  evthicc  25390  cniccbdd  25392  ovolgelb  25411  ovollb2lem  25419  ovolunlem1  25428  ovoliunlem1  25433  ovoliunlem2  25434  ovoliun  25436  ovolscalem1  25444  ovolicc1  25447  ovolicc2lem4  25451  ovolicc2lem5  25452  ovolicc2  25453  ovolicc  25454  nulmbl2  25467  voliunlem2  25482  ioombl1lem4  25492  ioorcl2  25503  uniioombllem1  25512  uniioombllem2a  25513  uniioombllem3  25516  dyaddisjlem  25526  dyadmaxlem  25528  opnmbllem  25532  volivth  25538  vitalilem4  25542  mbfmulc2lem  25578  mbfmax  25580  mbfposr  25583  ismbf3d  25585  mbfaddlem  25591  mbflimsup  25597  mbfi1fseqlem4  25649  itg2lcl  25658  xrge0f  25662  itg2itg1  25667  itg2const2  25672  itg2seq  25673  itg2uba  25674  itg2lea  25675  itg2mulclem  25677  itg2mulc  25678  itg2splitlem  25679  itg2split  25680  itg2monolem2  25682  itg2monolem3  25683  itg2mono  25684  itg2gt0  25691  itg2cnlem1  25692  itg2cnlem2  25693  itg2cn  25694  iblss  25736  itgle  25741  itgeqa  25745  itgioo  25747  ibladdlem  25751  iblabs  25760  iblabsr  25761  iblmulc2  25762  itgsplit  25767  itgspliticc  25768  itgsplitioo  25769  bddmulibl  25770  bddiblnc  25773  ditgcl  25789  ditgswap  25790  ditgsplitlem  25791  dvferm1lem  25918  dvferm2lem  25920  dvferm  25922  rollelem  25923  rolle  25924  cmvth  25925  cmvthOLD  25926  mvth  25927  dvlip  25928  dvlip2  25930  c1liplem1  25931  c1lip1  25932  dveq0  25935  dvgt0lem1  25937  dvivthlem1  25943  dvivth  25945  lhop1lem  25948  lhop1  25949  lhop2  25950  lhop  25951  dvcnvrelem1  25952  dvcnvre  25954  dvcvx  25955  dvfsumle  25956  dvfsumleOLD  25957  dvfsumge  25958  dvfsumabs  25959  dvfsumlem2  25963  dvfsumlem2OLD  25964  dvfsumlem3  25965  dvfsumlem4  25966  dvfsumrlimge0  25967  dvfsumrlim2  25969  ftc1lem1  25972  ftc1lem2  25973  ftc1a  25974  ftc1lem4  25976  ftc2  25981  ftc2ditglem  25982  itgparts  25984  itgsubstlem  25985  itgsubst  25986  itgpowd  25987  degltlem1  26007  deg1ge  26033  coe1mul3  26034  deg1sublt  26045  deg1mul2  26049  deg1tmle  26053  deg1tm  26054  idomrootle  26108  plypf1  26147  taylfvallem1  26294  tayl0  26299  pserulm  26361  psercnlem1  26365  pserdvlem1  26367  pserdvlem2  26368  abelthlem3  26373  abelth  26381  efcvx  26389  logno1  26575  logtayl  26599  xrlimcnp  26908  logfacbnd3  27164  log2sumbnd  27485  pntpbnd2  27528  pntibndlem3  27533  ttgcontlem1  28866  nmooge0  30751  nmoub3i  30757  isblo3i  30785  ubthlem1  30854  minvecolem4  30864  nmopge0  31895  nmfnge0  31911  nmophmi  32015  branmfn  32089  sgnval2  32724  xaddeq0  32742  xlt2addrd  32748  sgnmul  32825  sgnsub  32827  sgnmulsgn  32832  sgnmulsgp  32833  xmulcand  32910  xreceu  32911  xdivrec  32916  fsumrp0cl  33011  xrge0slmod  33322  ply1degltel  33564  ply1degleel  33565  ply1degltlss  33566  ply1degltdimlem  33658  ply1degltdim  33659  fldextrspundgdvdslem  33716  extdgfialglem1  33728  cos9thpiminplylem2  33819  cnre2csqlem  33946  tpr2rico  33948  xrge0iifcnv  33969  xrge0iifhom  33973  lmxrge0  33988  esumfsup  34106  esumpcvgval  34114  esumcvg  34122  dya2iocress  34310  dya2iocbrsiga  34311  dya2icobrsiga  34312  dya2icoseg  34313  dya2iocucvr  34320  sxbrsigalem2  34322  omssubaddlem  34335  omssubadd  34336  orvcgteel  34504  dstrvprob  34508  orvclteel  34509  signstcl  34601  signstf  34602  signstf0  34604  signstfvn  34605  signsvtn0  34606  signsvfn  34618  signsvfpn  34621  signsvfnn  34622  ftc2re  34634  cvmliftlem6  35357  cvmliftlem7  35358  cvmliftlem8  35359  cvmliftlem9  35360  cvmliftlem10  35361  cvmliftlem13  35363  ivthALT  36402  iooelexlt  37429  relowlssretop  37430  relowlpssretop  37431  sin2h  37673  cos2h  37674  tan2h  37675  poimirlem30  37713  poimir  37716  heicant  37718  opnmbllem0  37719  mblfinlem1  37720  mblfinlem2  37721  mblfinlem3  37722  mblfinlem4  37723  ismblfin  37724  itg2addnclem  37734  itg2addnclem2  37735  itg2gt0cn  37738  ibladdnclem  37739  iblabsnclem  37746  iblabsnc  37747  iblmulc2nc  37748  ftc1cnnclem  37754  ftc1anclem1  37756  ftc1anclem4  37759  ftc1anclem5  37760  ftc1anclem6  37761  ftc1anclem7  37762  ftc1anclem8  37763  ftc1anc  37764  ftc2nc  37765  areacirclem1  37771  areacirclem5  37775  areacirc  37776  isbnd3  37847  blbnd  37850  prdsbnd  37856  prdsbnd2  37858  cntotbnd  37859  dvrelog3  42181  0nonelalab  42183  dvrelogpow2b  42184  dvle2  42188  aks4d1p1p6  42189  aks4d1p1p5  42191  aks6d1c6lem3  42288  aks6d1c7lem2  42297  unitscyglem5  42315  idomodle  43311  imo72b2  44292  cvgdvgrat  44433  radcnvrat  44434  rfcnpre3  45157  rfcnpre4  45158  absfico  45342  nnxrd  45402  lefldiveq  45420  lttri5d  45427  supxrgere  45459  supxrgelem  45463  supxrge  45464  xralrple2  45480  infxr  45492  infleinflem1  45495  infleinflem2  45496  xralrple4  45498  xralrple3  45499  xrralrecnnle  45508  xrralrecnnge  45515  supxrunb3  45524  unb2ltle  45540  zxrd  45578  gtnelioc  45618  ltnelicc  45624  iooabslt  45626  gtnelicc  45627  eliooshift  45633  iocopn  45647  eliccelioc  45648  iooshift  45649  icoopn  45652  ge0lere  45659  iooiinicc  45669  sqrlearg  45680  iooiinioc  45683  uzinico  45686  preimaiocmnf  45687  uzubioo  45692  fsumge0cl  45700  limciccioolb  45748  lptioo1  45759  limcicciooub  45762  ltmod  45763  lptre2pt  45765  limsupre  45766  limcresiooub  45767  limcresioolb  45768  limcleqr  45769  limsupresico  45825  limsuppnfdlem  45826  limsupub  45829  limsupequzlem  45847  limsupre2lem  45849  limsupre3lem  45857  limsupvaluz2  45863  supcnvlimsup  45865  liminfresico  45896  limsup10exlem  45897  liminflelimsuplem  45900  limsupgtlem  45902  liminfval4  45914  liminfvaluz2  45920  limsupvaluz4  45925  liminflimsupclim  45932  xlimxrre  45956  xlimmnfvlem1  45957  xlimmnfv  45959  xlimpnfvlem1  45961  xlimpnfv  45963  sinaover2ne0  45993  ioccncflimc  46010  icccncfext  46012  icocncflimc  46014  cncfiooicclem1  46018  cncfiooicc  46019  cncfiooiccre  46020  cncfioobdlem  46021  dvbdfbdioolem1  46053  dvbdfbdioolem2  46054  dvbdfbdioo  46055  ioodvbdlimc1lem1  46056  ioodvbdlimc1lem2  46057  ioodvbdlimc1  46058  ioodvbdlimc2lem  46059  ioodvbdlimc2  46060  ditgeqiooicc  46085  iblsplit  46091  itgcoscmulx  46094  ibliooicc  46096  iblspltprt  46098  itgsincmulx  46099  itgsubsticc  46101  itgioocnicc  46102  iblcncfioo  46103  itgspltprt  46104  itgiccshift  46105  volioore  46115  voliooico  46117  voliooicof  46121  voliccico  46124  stoweidlem34  46159  stoweidlem52  46177  stirlinglem5  46203  dirkercncflem1  46228  dirkercncflem4  46231  fourierdlem4  46236  fourierdlem10  46242  fourierdlem19  46251  fourierdlem20  46252  fourierdlem24  46256  fourierdlem25  46257  fourierdlem26  46258  fourierdlem27  46259  fourierdlem28  46260  fourierdlem31  46263  fourierdlem32  46264  fourierdlem33  46265  fourierdlem35  46267  fourierdlem37  46269  fourierdlem40  46272  fourierdlem41  46273  fourierdlem43  46275  fourierdlem44  46276  fourierdlem46  46277  fourierdlem47  46278  fourierdlem48  46279  fourierdlem49  46280  fourierdlem50  46281  fourierdlem51  46282  fourierdlem52  46283  fourierdlem54  46285  fourierdlem57  46288  fourierdlem59  46290  fourierdlem60  46291  fourierdlem61  46292  fourierdlem62  46293  fourierdlem63  46294  fourierdlem64  46295  fourierdlem65  46296  fourierdlem68  46299  fourierdlem69  46300  fourierdlem70  46301  fourierdlem72  46303  fourierdlem73  46304  fourierdlem74  46305  fourierdlem75  46306  fourierdlem76  46307  fourierdlem78  46309  fourierdlem79  46310  fourierdlem81  46312  fourierdlem82  46313  fourierdlem84  46315  fourierdlem89  46320  fourierdlem90  46321  fourierdlem91  46322  fourierdlem92  46323  fourierdlem93  46324  fourierdlem94  46325  fourierdlem97  46328  fourierdlem100  46331  fourierdlem101  46332  fourierdlem102  46333  fourierdlem103  46334  fourierdlem104  46335  fourierdlem107  46338  fourierdlem109  46340  fourierdlem111  46342  fourierdlem112  46343  fourierdlem113  46344  fourierdlem114  46345  sqwvfoura  46353  fouriersw  46356  etransclem23  46382  etransclem46  46405  qndenserrnbllem  46419  rrxsnicc  46425  ioorrnopnlem  46429  ioorrnopnxrlem  46431  salgencntex  46468  sge0cl  46506  sge0fsum  46512  sge0iunmptlemre  46540  sge0isum  46552  sge0ad2en  46556  sge0xaddlem1  46558  sge0xaddlem2  46559  sge0reuz  46572  voliunsge0lem  46597  meassre  46602  omessre  46635  omeiunltfirp  46644  hoissre  46669  hoiprodcl  46672  ovnsubaddlem1  46695  hoiprodcl3  46705  hoidmvcl  46707  hsphoidmvle2  46710  hsphoidmvle  46711  sge0hsphoire  46714  hoidmv1lelem1  46716  hoidmv1lelem2  46717  hoidmv1lelem3  46718  hoidmv1le  46719  hoidmvlelem1  46720  hoidmvlelem2  46721  hoidmvlelem3  46722  hoidmvlelem4  46723  ovnhoilem1  46726  ovnhoilem2  46727  ovnhoi  46728  ovnlecvr2  46735  hspdifhsp  46741  hoidifhspdmvle  46745  hoiqssbllem1  46747  hoiqssbllem2  46748  hoiqssbllem3  46749  hspmbllem1  46751  hspmbllem2  46752  volicorege0  46762  ovolval5lem1  46777  ovolval5lem2  46778  iinhoiicclem  46798  iinhoiicc  46799  iunhoiioolem  46800  iunhoiioo  46801  vonioolem2  46806  vonicclem2  46809  vonsn  46816  pimltmnf2f  46822  pimconstlt0  46826  pimgtpnf2f  46830  salpreimagelt  46832  salpreimalegt  46834  preimageiingt  46845  preimaleiinlt  46846  pimrecltneg  46849  issmflem  46852  issmflelem  46869  issmfgtlem  46880  issmfgt  46881  smfaddlem1  46888  issmfgelem  46894  issmfge  46895  smfpimioompt  46911  smfresal  46913  smfrec  46914  smfmullem1  46916  smfmullem2  46917  smfmullem3  46918  smfmullem4  46919  smfpimbor1lem1  46923  smfsuplem1  46936  smflimsuplem4  46948  smfliminflem  46955  smfdmmblpimne  46962  smfpimne  46964  smfpimne2  46965  fsupdm  46967  finfdm  46971  smfinfdmmbllem  46973  bgoldbtbnd  47936  eenglngeehlnmlem2  48866