Theorem rexrd 11308

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-xr 11296

This theorem is referenced by:  xnn0xr  12601  rpxr  13041  rpxrd  13075  max0sub  13234  qextltlem  13240  xralrple  13243  xnegcl  13251  xaddf  13262  xnn0lem1lt  13282  xnn0lenn0nn0  13283  xmulf  13310  xadddi  13333  xrub  13350  supxrre  13365  infxrre  13374  ixxub  13404  ixxlb  13405  ioo0  13408  ico0  13429  ioc0  13430  iooshf  13462  icoshftf1o  13510  supicc  13537  supiccub  13538  supicclub  13539  xnn0xrge0  13542  ssfzunsn  13606  addmodid  13956  hashnnn0genn0  14378  hashunsnggt  14429  elicc4abs  15354  caucvgrlem  15705  fprodge1  16027  pcxcl  16894  pcdvdsb  16902  pcaddlem  16921  ramcl2lem  17042  ramlb  17052  0ram  17053  setsstruct  17209  prdsxmetlem  24393  xblss2ps  24426  xblss2  24427  blss2ps  24428  blss2  24429  blhalf  24430  metustto  24581  metustexhalf  24584  nmoi  24764  nmoix  24765  nmoi2  24766  nmoleub  24767  qdensere  24805  cnblcld  24810  ioo2blex  24829  tgioo  24831  blcvx  24833  zcld  24848  recld2  24849  iccntr  24856  icccmplem1  24857  reconnlem1  24861  reconnlem2  24862  opnreen  24866  metnrmlem3  24896  icoopnst  24982  iocopnst  24983  cnheibor  25000  lebnumii  25011  nmoleub2lem  25160  lmnn  25310  iscau3  25325  minveclem4  25479  ivthlem1  25499  ivthlem2  25500  ivthlem3  25501  ivth2  25503  ivthle  25504  ivthle2  25505  ivthicc  25506  evthicc  25507  cniccbdd  25509  ovolgelb  25528  ovollb2lem  25536  ovolunlem1  25545  ovoliunlem1  25550  ovoliunlem2  25551  ovoliun  25553  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem4  25568  ovolicc2lem5  25569  ovolicc2  25570  ovolicc  25571  nulmbl2  25584  voliunlem2  25599  ioombl1lem4  25609  ioorcl2  25620  uniioombllem1  25629  uniioombllem2a  25630  uniioombllem3  25633  dyaddisjlem  25643  dyadmaxlem  25645  opnmbllem  25649  volivth  25655  vitalilem4  25659  mbfmulc2lem  25695  mbfmax  25697  mbfposr  25700  ismbf3d  25702  mbfaddlem  25708  mbflimsup  25714  mbfi1fseqlem4  25767  itg2lcl  25776  xrge0f  25780  itg2itg1  25785  itg2const2  25790  itg2seq  25791  itg2uba  25792  itg2lea  25793  itg2mulclem  25795  itg2mulc  25796  itg2splitlem  25797  itg2split  25798  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  itg2cn  25812  iblss  25854  itgle  25859  itgeqa  25863  itgioo  25865  ibladdlem  25869  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgsplit  25885  itgspliticc  25886  itgsplitioo  25887  bddmulibl  25888  bddiblnc  25891  ditgcl  25907  ditgswap  25908  ditgsplitlem  25909  dvferm1lem  26036  dvferm2lem  26038  dvferm  26040  rollelem  26041  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvlip2  26048  c1liplem1  26049  c1lip1  26050  dveq0  26053  dvgt0lem1  26055  dvivthlem1  26061  dvivth  26063  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  dvcnvrelem1  26070  dvcnvre  26072  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlimge0  26085  dvfsumrlim2  26087  ftc1lem1  26090  ftc1lem2  26091  ftc1a  26092  ftc1lem4  26094  ftc2  26099  ftc2ditglem  26100  itgparts  26102  itgsubstlem  26103  itgsubst  26104  itgpowd  26105  degltlem1  26125  deg1ge  26151  coe1mul3  26152  deg1sublt  26163  deg1mul2  26167  deg1tmle  26171  deg1tm  26172  idomrootle  26226  plypf1  26265  taylfvallem1  26412  tayl0  26417  pserulm  26479  psercnlem1  26483  pserdvlem1  26485  pserdvlem2  26486  abelthlem3  26491  abelth  26499  efcvx  26507  logno1  26692  logtayl  26716  xrlimcnp  27025  logfacbnd3  27281  log2sumbnd  27602  pntpbnd2  27645  pntibndlem3  27650  ttgcontlem1  28913  nmooge0  30795  nmoub3i  30801  isblo3i  30829  ubthlem1  30898  minvecolem4  30908  nmopge0  31939  nmfnge0  31955  nmophmi  32059  branmfn  32133  xaddeq0  32763  xlt2addrd  32768  xmulcand  32887  xreceu  32888  xdivrec  32893  fsumrp0cl  33008  xrge0slmod  33355  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  ply1degltdimlem  33649  ply1degltdim  33650  cnre2csqlem  33870  tpr2rico  33872  xrge0iifcnv  33893  xrge0iifhom  33897  lmxrge0  33912  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  dya2iocress  34255  dya2iocbrsiga  34256  dya2icobrsiga  34257  dya2icoseg  34258  dya2iocucvr  34265  sxbrsigalem2  34267  omssubaddlem  34280  omssubadd  34281  orvcgteel  34448  dstrvprob  34452  orvclteel  34453  sgnmul  34523  sgnsub  34525  sgnmulsgn  34530  sgnmulsgp  34531  signstcl  34558  signstf  34559  signstf0  34561  signstfvn  34562  signsvtn0  34563  signsvfn  34575  signsvfpn  34578  signsvfnn  34579  ftc2re  34591  cvmliftlem6  35274  cvmliftlem7  35275  cvmliftlem8  35276  cvmliftlem9  35277  cvmliftlem10  35278  cvmliftlem13  35280  ivthALT  36317  iooelexlt  37344  relowlssretop  37345  relowlpssretop  37346  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem30  37636  poimir  37639  heicant  37641  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem  37657  itg2addnclem2  37658  itg2gt0cn  37661  ibladdnclem  37662  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  ftc1cnnclem  37677  ftc1anclem1  37679  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  areacirclem1  37694  areacirclem5  37698  areacirc  37699  isbnd3  37770  blbnd  37773  prdsbnd  37779  prdsbnd2  37781  cntotbnd  37782  dvrelog3  42046  0nonelalab  42048  dvrelogpow2b  42049  dvle2  42053  aks4d1p1p6  42054  aks4d1p1p5  42056  aks6d1c6lem3  42153  aks6d1c7lem2  42162  unitscyglem5  42180  idomodle  43179  imo72b2  44161  cvgdvgrat  44308  radcnvrat  44309  rfcnpre3  44970  rfcnpre4  44971  absfico  45160  nnxrd  45223  lefldiveq  45242  lttri5d  45249  supxrgere  45282  supxrgelem  45286  supxrge  45287  xralrple2  45303  infxr  45316  infleinflem1  45319  infleinflem2  45320  xralrple4  45322  xralrple3  45323  xrralrecnnle  45332  xrralrecnnge  45339  supxrunb3  45348  unb2ltle  45364  zxrd  45402  gtnelioc  45443  ltnelicc  45449  iooabslt  45451  gtnelicc  45452  eliooshift  45458  iocopn  45472  eliccelioc  45473  iooshift  45474  icoopn  45477  ge0lere  45484  iooiinicc  45494  sqrlearg  45505  iooiinioc  45508  uzinico  45512  preimaiocmnf  45513  uzubioo  45519  fsumge0cl  45528  limciccioolb  45576  lptioo1  45587  limcicciooub  45592  ltmod  45593  lptre2pt  45595  limsupre  45596  limcresiooub  45597  limcresioolb  45598  limcleqr  45599  limsupresico  45655  limsuppnfdlem  45656  limsupub  45659  limsupequzlem  45677  limsupre2lem  45679  limsupre3lem  45687  limsupvaluz2  45693  supcnvlimsup  45695  liminfresico  45726  limsup10exlem  45727  liminflelimsuplem  45730  limsupgtlem  45732  liminfval4  45744  liminfvaluz2  45750  limsupvaluz4  45755  liminflimsupclim  45762  xlimxrre  45786  xlimmnfvlem1  45787  xlimmnfv  45789  xlimpnfvlem1  45791  xlimpnfv  45793  sinaover2ne0  45823  ioccncflimc  45840  icccncfext  45842  icocncflimc  45844  cncfiooicclem1  45848  cncfiooicc  45849  cncfiooiccre  45850  cncfioobdlem  45851  dvbdfbdioolem1  45883  dvbdfbdioolem2  45884  dvbdfbdioo  45885  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc1  45888  ioodvbdlimc2lem  45889  ioodvbdlimc2  45890  ditgeqiooicc  45915  iblsplit  45921  itgcoscmulx  45924  ibliooicc  45926  iblspltprt  45928  itgsincmulx  45929  itgsubsticc  45931  itgioocnicc  45932  iblcncfioo  45933  itgspltprt  45934  itgiccshift  45935  volioore  45945  voliooico  45947  voliooicof  45951  voliccico  45954  stoweidlem34  45989  stoweidlem52  46007  stirlinglem5  46033  dirkercncflem1  46058  dirkercncflem4  46061  fourierdlem4  46066  fourierdlem10  46072  fourierdlem19  46081  fourierdlem20  46082  fourierdlem24  46086  fourierdlem25  46087  fourierdlem26  46088  fourierdlem27  46089  fourierdlem28  46090  fourierdlem31  46093  fourierdlem32  46094  fourierdlem33  46095  fourierdlem35  46097  fourierdlem37  46099  fourierdlem40  46102  fourierdlem41  46103  fourierdlem43  46105  fourierdlem44  46106  fourierdlem46  46107  fourierdlem47  46108  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem52  46113  fourierdlem54  46115  fourierdlem57  46118  fourierdlem59  46120  fourierdlem60  46121  fourierdlem61  46122  fourierdlem62  46123  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem68  46129  fourierdlem69  46130  fourierdlem70  46131  fourierdlem72  46133  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem84  46145  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem94  46155  fourierdlem97  46158  fourierdlem100  46161  fourierdlem101  46162  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  fourierdlem109  46170  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fourierdlem114  46175  sqwvfoura  46183  fouriersw  46186  etransclem23  46212  etransclem46  46235  qndenserrnbllem  46249  rrxsnicc  46255  ioorrnopnlem  46259  ioorrnopnxrlem  46261  salgencntex  46298  sge0cl  46336  sge0fsum  46342  sge0iunmptlemre  46370  sge0isum  46382  sge0ad2en  46386  sge0xaddlem1  46388  sge0xaddlem2  46389  sge0reuz  46402  voliunsge0lem  46427  meassre  46432  omessre  46465  omeiunltfirp  46474  hoissre  46499  hoiprodcl  46502  ovnsubaddlem1  46525  hoiprodcl3  46535  hoidmvcl  46537  hsphoidmvle2  46540  hsphoidmvle  46541  sge0hsphoire  46544  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  ovnhoilem1  46556  ovnhoilem2  46557  ovnhoi  46558  ovnlecvr2  46565  hspdifhsp  46571  hoidifhspdmvle  46575  hoiqssbllem1  46577  hoiqssbllem2  46578  hoiqssbllem3  46579  hspmbllem1  46581  hspmbllem2  46582  volicorege0  46592  ovolval5lem1  46607  ovolval5lem2  46608  iinhoiicclem  46628  iinhoiicc  46629  iunhoiioolem  46630  iunhoiioo  46631  vonioolem2  46636  vonicclem2  46639  vonsn  46646  pimltmnf2f  46652  pimconstlt0  46656  pimgtpnf2f  46660  salpreimagelt  46662  salpreimalegt  46664  preimageiingt  46675  preimaleiinlt  46676  pimrecltneg  46679  issmflem  46682  issmflelem  46699  issmfgtlem  46710  issmfgt  46711  smfaddlem1  46718  issmfgelem  46724  issmfge  46725  smfpimioompt  46741  smfresal  46743  smfrec  46744  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  smfmullem4  46749  smfpimbor1lem1  46753  smfsuplem1  46766  smflimsuplem4  46778  smfliminflem  46785  smfdmmblpimne  46792  smfpimne  46794  smfpimne2  46795  fsupdm  46797  finfdm  46801  smfinfdmmbllem  46803  bgoldbtbnd  47733  eenglngeehlnmlem2  48587