Theorem rexrd 11034

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  ℝ^*cxr 11017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905  df-xr 11022

This theorem is referenced by:  xnn0xr  12319  rpxr  12748  rpxrd  12782  max0sub  12939  qextltlem  12945  xralrple  12948  xnegcl  12956  xaddf  12967  xnn0lem1lt  12987  xnn0lenn0nn0  12988  xmulf  13015  xadddi  13038  xrub  13055  supxrre  13070  infxrre  13079  ixxub  13109  ixxlb  13110  ioo0  13113  ico0  13134  ioc0  13135  iooshf  13167  icoshftf1o  13215  supicc  13242  supiccub  13243  supicclub  13244  xnn0xrge0  13247  ssfzunsn  13311  addmodid  13648  hashnnn0genn0  14066  hashunsnggt  14118  elicc4abs  15040  caucvgrlem  15393  fprodge1  15714  pcxcl  16571  pcdvdsb  16579  pcaddlem  16598  ramcl2lem  16719  ramlb  16729  0ram  16730  setsstruct  16886  prdsxmetlem  23530  xblss2ps  23563  xblss2  23564  blss2ps  23565  blss2  23566  blhalf  23567  metustto  23718  metustexhalf  23721  nmoi  23901  nmoix  23902  nmoi2  23903  nmoleub  23904  qdensere  23942  cnblcld  23947  ioo2blex  23966  tgioo  23968  blcvx  23970  zcld  23985  recld2  23986  iccntr  23993  icccmplem1  23994  reconnlem1  23998  reconnlem2  23999  opnreen  24003  metnrmlem3  24033  icoopnst  24111  iocopnst  24112  cnheibor  24127  lebnumii  24138  nmoleub2lem  24286  lmnn  24436  iscau3  24451  minveclem4  24605  ivthlem1  24624  ivthlem2  24625  ivthlem3  24626  ivth2  24628  ivthle  24629  ivthle2  24630  ivthicc  24631  evthicc  24632  cniccbdd  24634  ovolgelb  24653  ovollb2lem  24661  ovolunlem1  24670  ovoliunlem1  24675  ovoliunlem2  24676  ovoliun  24678  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem4  24693  ovolicc2lem5  24694  ovolicc2  24695  ovolicc  24696  nulmbl2  24709  voliunlem2  24724  ioombl1lem4  24734  ioorcl2  24745  uniioombllem1  24754  uniioombllem2a  24755  uniioombllem3  24758  dyaddisjlem  24768  dyadmaxlem  24770  opnmbllem  24774  volivth  24780  vitalilem4  24784  mbfmulc2lem  24820  mbfmax  24822  mbfposr  24825  ismbf3d  24827  mbfaddlem  24833  mbflimsup  24839  mbfi1fseqlem4  24892  itg2lcl  24901  xrge0f  24905  itg2itg1  24910  itg2const2  24915  itg2seq  24916  itg2uba  24917  itg2lea  24918  itg2mulclem  24920  itg2mulc  24921  itg2splitlem  24922  itg2split  24923  itg2monolem2  24925  itg2monolem3  24926  itg2mono  24927  itg2gt0  24934  itg2cnlem1  24935  itg2cnlem2  24936  itg2cn  24937  iblss  24978  itgle  24983  itgeqa  24987  itgioo  24989  ibladdlem  24993  iblabs  25002  iblabsr  25003  iblmulc2  25004  itgsplit  25009  itgspliticc  25010  itgsplitioo  25011  bddmulibl  25012  bddiblnc  25015  ditgcl  25031  ditgswap  25032  ditgsplitlem  25033  dvferm1lem  25157  dvferm2lem  25159  dvferm  25161  rollelem  25162  rolle  25163  cmvth  25164  mvth  25165  dvlip  25166  dvlip2  25168  c1liplem1  25169  c1lip1  25170  dveq0  25173  dvgt0lem1  25175  dvivthlem1  25181  dvivth  25183  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  dvcnvrelem1  25190  dvcnvre  25192  dvcvx  25193  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsumrlimge0  25203  dvfsumrlim2  25205  ftc1lem1  25208  ftc1lem2  25209  ftc1a  25210  ftc1lem4  25212  ftc2  25217  ftc2ditglem  25218  itgparts  25220  itgsubstlem  25221  itgsubst  25222  itgpowd  25223  degltlem1  25246  deg1ge  25272  coe1mul3  25273  deg1sublt  25284  deg1mul2  25288  deg1tmle  25291  deg1tm  25292  plypf1  25382  taylfvallem1  25525  tayl0  25530  pserulm  25590  psercnlem1  25593  pserdvlem1  25595  pserdvlem2  25596  abelthlem3  25601  abelth  25609  efcvx  25617  logno1  25800  logtayl  25824  xrlimcnp  26127  logfacbnd3  26380  log2sumbnd  26701  pntpbnd2  26744  pntibndlem3  26749  ttgcontlem1  27261  nmooge0  29138  nmoub3i  29144  isblo3i  29172  ubthlem1  29241  minvecolem4  29251  nmopge0  30282  nmfnge0  30298  nmophmi  30402  branmfn  30476  xaddeq0  31085  xlt2addrd  31090  xmulcand  31204  xreceu  31205  xdivrec  31210  fsumrp0cl  31313  xrge0slmod  31557  cnre2csqlem  31869  tpr2rico  31871  xrge0iifcnv  31892  xrge0iifhom  31896  lmxrge0  31911  esumfsup  32047  esumpcvgval  32055  esumcvg  32063  dya2iocress  32250  dya2iocbrsiga  32251  dya2icobrsiga  32252  dya2icoseg  32253  dya2iocucvr  32260  sxbrsigalem2  32262  omssubaddlem  32275  omssubadd  32276  orvcgteel  32443  dstrvprob  32447  orvclteel  32448  sgnmul  32518  sgnsub  32520  sgnmulsgn  32525  sgnmulsgp  32526  signstcl  32553  signstf  32554  signstf0  32556  signstfvn  32557  signsvtn0  32558  signsvfn  32570  signsvfpn  32573  signsvfnn  32574  ftc2re  32587  cvmliftlem6  33261  cvmliftlem7  33262  cvmliftlem8  33263  cvmliftlem9  33264  cvmliftlem10  33265  cvmliftlem13  33267  ivthALT  34533  iooelexlt  35542  relowlssretop  35543  relowlpssretop  35544  sin2h  35776  cos2h  35777  tan2h  35778  poimirlem30  35816  poimir  35819  heicant  35821  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  itg2addnclem  35837  itg2addnclem2  35838  itg2gt0cn  35841  ibladdnclem  35842  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  ftc1cnnclem  35857  ftc1anclem1  35859  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  ftc2nc  35868  areacirclem1  35874  areacirclem5  35878  areacirc  35879  isbnd3  35951  blbnd  35954  prdsbnd  35960  prdsbnd2  35962  cntotbnd  35963  dvrelog3  40080  0nonelalab  40082  dvrelogpow2b  40083  dvle2  40087  aks4d1p1p6  40088  aks4d1p1p5  40090  idomrootle  41027  idomodle  41028  imo72b2  41790  cvgdvgrat  41938  radcnvrat  41939  rfcnpre3  42583  rfcnpre4  42584  nnxrd  42592  absfico  42765  lefldiveq  42838  lttri5d  42845  supxrgere  42879  supxrgelem  42883  supxrge  42884  xralrple2  42900  infxr  42913  infleinflem1  42916  infleinflem2  42917  xralrple4  42919  xralrple3  42920  xrralrecnnle  42929  xrralrecnnge  42937  supxrunb3  42946  unb2ltle  42962  zxrd  43000  gtnelioc  43036  ltnelicc  43042  iooabslt  43044  gtnelicc  43045  eliooshift  43051  iocopn  43065  eliccelioc  43066  iooshift  43067  icoopn  43070  ge0lere  43077  iooiinicc  43087  sqrlearg  43098  iooiinioc  43101  uzinico  43105  preimaiocmnf  43106  uzubioo  43112  fsumge0cl  43121  limciccioolb  43169  lptioo1  43180  limcicciooub  43185  ltmod  43186  lptre2pt  43188  limsupre  43189  limcresiooub  43190  limcresioolb  43191  limcleqr  43192  limsupresico  43248  limsuppnfdlem  43249  limsupub  43252  limsupequzlem  43270  limsupre2lem  43272  limsupre3lem  43280  limsupvaluz2  43286  supcnvlimsup  43288  liminfresico  43319  limsup10exlem  43320  liminflelimsuplem  43323  limsupgtlem  43325  liminfval4  43337  liminfvaluz2  43343  limsupvaluz4  43348  liminflimsupclim  43355  xlimxrre  43379  xlimmnfvlem1  43380  xlimmnfv  43382  xlimpnfvlem1  43384  xlimpnfv  43386  sinaover2ne0  43416  ioccncflimc  43433  icccncfext  43435  icocncflimc  43437  cncfiooicclem1  43441  cncfiooicc  43442  cncfiooiccre  43443  cncfioobdlem  43444  dvbdfbdioolem1  43476  dvbdfbdioolem2  43477  dvbdfbdioo  43478  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc1  43481  ioodvbdlimc2lem  43482  ioodvbdlimc2  43483  ditgeqiooicc  43508  iblsplit  43514  itgcoscmulx  43517  ibliooicc  43519  iblspltprt  43521  itgsincmulx  43522  itgsubsticc  43524  itgioocnicc  43525  iblcncfioo  43526  itgspltprt  43527  itgiccshift  43528  volioore  43538  voliooico  43540  voliooicof  43544  voliccico  43547  stoweidlem34  43582  stoweidlem52  43600  stirlinglem5  43626  dirkercncflem1  43651  dirkercncflem4  43654  fourierdlem4  43659  fourierdlem10  43665  fourierdlem19  43674  fourierdlem20  43675  fourierdlem24  43679  fourierdlem25  43680  fourierdlem26  43681  fourierdlem27  43682  fourierdlem28  43683  fourierdlem31  43686  fourierdlem32  43687  fourierdlem33  43688  fourierdlem35  43690  fourierdlem37  43692  fourierdlem40  43695  fourierdlem41  43696  fourierdlem43  43698  fourierdlem44  43699  fourierdlem46  43700  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem51  43705  fourierdlem52  43706  fourierdlem54  43708  fourierdlem57  43711  fourierdlem59  43713  fourierdlem60  43714  fourierdlem61  43715  fourierdlem62  43716  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem68  43722  fourierdlem69  43723  fourierdlem70  43724  fourierdlem72  43726  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem78  43732  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem84  43738  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem93  43747  fourierdlem94  43748  fourierdlem97  43751  fourierdlem100  43754  fourierdlem101  43755  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem109  43763  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fourierdlem114  43768  sqwvfoura  43776  fouriersw  43779  etransclem23  43805  etransclem46  43828  qndenserrnbllem  43842  rrxsnicc  43848  ioorrnopnlem  43852  ioorrnopnxrlem  43854  salgencntex  43889  sge0cl  43926  sge0fsum  43932  sge0iunmptlemre  43960  sge0isum  43972  sge0ad2en  43976  sge0xaddlem1  43978  sge0xaddlem2  43979  sge0reuz  43992  voliunsge0lem  44017  meassre  44022  omessre  44055  omeiunltfirp  44064  hoissre  44089  hoiprodcl  44092  ovnsubaddlem1  44115  hoiprodcl3  44125  hoidmvcl  44127  hsphoidmvle2  44130  hsphoidmvle  44131  sge0hsphoire  44134  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  ovnhoilem1  44146  ovnhoilem2  44147  ovnhoi  44148  ovnlecvr2  44155  hspdifhsp  44161  hoidifhspdmvle  44165  hoiqssbllem1  44167  hoiqssbllem2  44168  hoiqssbllem3  44169  hspmbllem1  44171  hspmbllem2  44172  volicorege0  44182  ovolval5lem1  44197  ovolval5lem2  44198  iinhoiicclem  44218  iinhoiicc  44219  iunhoiioolem  44220  iunhoiioo  44221  vonioolem2  44226  vonicclem2  44229  vonsn  44236  pimltmnf2f  44242  pimconstlt0  44246  pimgtpnf2f  44250  salpreimagelt  44252  salpreimalegt  44254  preimageiingt  44265  preimaleiinlt  44266  pimrecltneg  44269  issmflem  44272  issmflelem  44289  issmfgtlem  44300  issmfgt  44301  smfaddlem1  44308  issmfgelem  44314  issmfge  44315  smfpimioompt  44331  smfresal  44333  smfrec  44334  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  smfmullem4  44339  smfpimbor1lem1  44343  smfsuplem1  44355  smflimsuplem4  44367  smfliminflem  44374  bgoldbtbnd  45272  eenglngeehlnmlem2  46095