Theorem rexrd 11283

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11126  ℝ^*cxr 11266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-xr 11271

This theorem is referenced by:  xnn0xr  12577  rpxr  13016  rpxrd  13050  max0sub  13210  qextltlem  13216  xralrple  13219  xnegcl  13227  xaddf  13238  xnn0lem1lt  13258  xnn0lenn0nn0  13259  xmulf  13286  xadddi  13309  xrub  13326  supxrre  13341  infxrre  13351  ixxub  13381  ixxlb  13382  ioo0  13385  ico0  13406  ioc0  13407  iooshf  13441  icoshftf1o  13489  supicc  13516  supiccub  13517  supicclub  13518  xnn0xrge0  13521  ssfzunsn  13585  addmodid  13935  hashnnn0genn0  14359  hashunsnggt  14410  elicc4abs  15336  caucvgrlem  15687  fprodge1  16009  pcxcl  16879  pcdvdsb  16887  pcaddlem  16906  ramcl2lem  17027  ramlb  17037  0ram  17038  setsstruct  17193  prdsxmetlem  24305  xblss2ps  24338  xblss2  24339  blss2ps  24340  blss2  24341  blhalf  24342  metustto  24490  metustexhalf  24493  nmoi  24665  nmoix  24666  nmoi2  24667  nmoleub  24668  qdensere  24706  cnblcld  24711  ioo2blex  24731  tgioo  24733  blcvx  24735  zcld  24751  recld2  24752  iccntr  24759  icccmplem1  24760  reconnlem1  24764  reconnlem2  24765  opnreen  24769  metnrmlem3  24799  icoopnst  24885  iocopnst  24886  cnheibor  24903  lebnumii  24914  nmoleub2lem  25063  lmnn  25213  iscau3  25228  minveclem4  25382  ivthlem1  25402  ivthlem2  25403  ivthlem3  25404  ivth2  25406  ivthle  25407  ivthle2  25408  ivthicc  25409  evthicc  25410  cniccbdd  25412  ovolgelb  25431  ovollb2lem  25439  ovolunlem1  25448  ovoliunlem1  25453  ovoliunlem2  25454  ovoliun  25456  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem4  25471  ovolicc2lem5  25472  ovolicc2  25473  ovolicc  25474  nulmbl2  25487  voliunlem2  25502  ioombl1lem4  25512  ioorcl2  25523  uniioombllem1  25532  uniioombllem2a  25533  uniioombllem3  25536  dyaddisjlem  25546  dyadmaxlem  25548  opnmbllem  25552  volivth  25558  vitalilem4  25562  mbfmulc2lem  25598  mbfmax  25600  mbfposr  25603  ismbf3d  25605  mbfaddlem  25611  mbflimsup  25617  mbfi1fseqlem4  25669  itg2lcl  25678  xrge0f  25682  itg2itg1  25687  itg2const2  25692  itg2seq  25693  itg2uba  25694  itg2lea  25695  itg2mulclem  25697  itg2mulc  25698  itg2splitlem  25699  itg2split  25700  itg2monolem2  25702  itg2monolem3  25703  itg2mono  25704  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  itg2cn  25714  iblss  25756  itgle  25761  itgeqa  25765  itgioo  25767  ibladdlem  25771  iblabs  25780  iblabsr  25781  iblmulc2  25782  itgsplit  25787  itgspliticc  25788  itgsplitioo  25789  bddmulibl  25790  bddiblnc  25793  ditgcl  25809  ditgswap  25810  ditgsplitlem  25811  dvferm1lem  25938  dvferm2lem  25940  dvferm  25942  rollelem  25943  rolle  25944  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  dvlip2  25950  c1liplem1  25951  c1lip1  25952  dveq0  25955  dvgt0lem1  25957  dvivthlem1  25963  dvivth  25965  lhop1lem  25968  lhop1  25969  lhop2  25970  lhop  25971  dvcnvrelem1  25972  dvcnvre  25974  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlimge0  25987  dvfsumrlim2  25989  ftc1lem1  25992  ftc1lem2  25993  ftc1a  25994  ftc1lem4  25996  ftc2  26001  ftc2ditglem  26002  itgparts  26004  itgsubstlem  26005  itgsubst  26006  itgpowd  26007  degltlem1  26027  deg1ge  26053  coe1mul3  26054  deg1sublt  26065  deg1mul2  26069  deg1tmle  26073  deg1tm  26074  idomrootle  26128  plypf1  26167  taylfvallem1  26314  tayl0  26319  pserulm  26381  psercnlem1  26385  pserdvlem1  26387  pserdvlem2  26388  abelthlem3  26393  abelth  26401  efcvx  26409  logno1  26595  logtayl  26619  xrlimcnp  26928  logfacbnd3  27184  log2sumbnd  27505  pntpbnd2  27548  pntibndlem3  27553  ttgcontlem1  28810  nmooge0  30694  nmoub3i  30700  isblo3i  30728  ubthlem1  30797  minvecolem4  30807  nmopge0  31838  nmfnge0  31854  nmophmi  31958  branmfn  32032  sgnval2  32658  xaddeq0  32676  xlt2addrd  32682  sgnmul  32760  sgnsub  32762  sgnmulsgn  32767  sgnmulsgp  32768  xmulcand  32841  xreceu  32842  xdivrec  32847  fsumrp0cl  32962  xrge0slmod  33309  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1degltdimlem  33608  ply1degltdim  33609  fldextrspundgdvdslem  33667  cos9thpiminplylem2  33763  cnre2csqlem  33887  tpr2rico  33889  xrge0iifcnv  33910  xrge0iifhom  33914  lmxrge0  33929  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  dya2iocress  34252  dya2iocbrsiga  34253  dya2icobrsiga  34254  dya2icoseg  34255  dya2iocucvr  34262  sxbrsigalem2  34264  omssubaddlem  34277  omssubadd  34278  orvcgteel  34446  dstrvprob  34450  orvclteel  34451  signstcl  34543  signstf  34544  signstf0  34546  signstfvn  34547  signsvtn0  34548  signsvfn  34560  signsvfpn  34563  signsvfnn  34564  ftc2re  34576  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem10  35262  cvmliftlem13  35264  ivthALT  36299  iooelexlt  37326  relowlssretop  37327  relowlpssretop  37328  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem30  37620  poimir  37623  heicant  37625  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnclem  37641  itg2addnclem2  37642  itg2gt0cn  37645  ibladdnclem  37646  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  ftc1cnnclem  37661  ftc1anclem1  37663  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  areacirclem1  37678  areacirclem5  37682  areacirc  37683  isbnd3  37754  blbnd  37757  prdsbnd  37763  prdsbnd2  37765  cntotbnd  37766  dvrelog3  42024  0nonelalab  42026  dvrelogpow2b  42027  dvle2  42031  aks4d1p1p6  42032  aks4d1p1p5  42034  aks6d1c6lem3  42131  aks6d1c7lem2  42140  unitscyglem5  42158  idomodle  43162  imo72b2  44143  cvgdvgrat  44285  radcnvrat  44286  rfcnpre3  45005  rfcnpre4  45006  absfico  45190  nnxrd  45250  lefldiveq  45269  lttri5d  45276  supxrgere  45308  supxrgelem  45312  supxrge  45313  xralrple2  45329  infxr  45342  infleinflem1  45345  infleinflem2  45346  xralrple4  45348  xralrple3  45349  xrralrecnnle  45358  xrralrecnnge  45365  supxrunb3  45374  unb2ltle  45390  zxrd  45428  gtnelioc  45468  ltnelicc  45474  iooabslt  45476  gtnelicc  45477  eliooshift  45483  iocopn  45497  eliccelioc  45498  iooshift  45499  icoopn  45502  ge0lere  45509  iooiinicc  45519  sqrlearg  45530  iooiinioc  45533  uzinico  45536  preimaiocmnf  45537  uzubioo  45542  fsumge0cl  45550  limciccioolb  45598  lptioo1  45609  limcicciooub  45614  ltmod  45615  lptre2pt  45617  limsupre  45618  limcresiooub  45619  limcresioolb  45620  limcleqr  45621  limsupresico  45677  limsuppnfdlem  45678  limsupub  45681  limsupequzlem  45699  limsupre2lem  45701  limsupre3lem  45709  limsupvaluz2  45715  supcnvlimsup  45717  liminfresico  45748  limsup10exlem  45749  liminflelimsuplem  45752  limsupgtlem  45754  liminfval4  45766  liminfvaluz2  45772  limsupvaluz4  45777  liminflimsupclim  45784  xlimxrre  45808  xlimmnfvlem1  45809  xlimmnfv  45811  xlimpnfvlem1  45813  xlimpnfv  45815  sinaover2ne0  45845  ioccncflimc  45862  icccncfext  45864  icocncflimc  45866  cncfiooicclem1  45870  cncfiooicc  45871  cncfiooiccre  45872  cncfioobdlem  45873  dvbdfbdioolem1  45905  dvbdfbdioolem2  45906  dvbdfbdioo  45907  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc1  45910  ioodvbdlimc2lem  45911  ioodvbdlimc2  45912  ditgeqiooicc  45937  iblsplit  45943  itgcoscmulx  45946  ibliooicc  45948  iblspltprt  45950  itgsincmulx  45951  itgsubsticc  45953  itgioocnicc  45954  iblcncfioo  45955  itgspltprt  45956  itgiccshift  45957  volioore  45967  voliooico  45969  voliooicof  45973  voliccico  45976  stoweidlem34  46011  stoweidlem52  46029  stirlinglem5  46055  dirkercncflem1  46080  dirkercncflem4  46083  fourierdlem4  46088  fourierdlem10  46094  fourierdlem19  46103  fourierdlem20  46104  fourierdlem24  46108  fourierdlem25  46109  fourierdlem26  46110  fourierdlem27  46111  fourierdlem28  46112  fourierdlem31  46115  fourierdlem32  46116  fourierdlem33  46117  fourierdlem35  46119  fourierdlem37  46121  fourierdlem40  46124  fourierdlem41  46125  fourierdlem43  46127  fourierdlem44  46128  fourierdlem46  46129  fourierdlem47  46130  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem52  46135  fourierdlem54  46137  fourierdlem57  46140  fourierdlem59  46142  fourierdlem60  46143  fourierdlem61  46144  fourierdlem62  46145  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem68  46151  fourierdlem69  46152  fourierdlem70  46153  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem84  46167  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem94  46177  fourierdlem97  46180  fourierdlem100  46183  fourierdlem101  46184  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem109  46192  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fourierdlem114  46197  sqwvfoura  46205  fouriersw  46208  etransclem23  46234  etransclem46  46257  qndenserrnbllem  46271  rrxsnicc  46277  ioorrnopnlem  46281  ioorrnopnxrlem  46283  salgencntex  46320  sge0cl  46358  sge0fsum  46364  sge0iunmptlemre  46392  sge0isum  46404  sge0ad2en  46408  sge0xaddlem1  46410  sge0xaddlem2  46411  sge0reuz  46424  voliunsge0lem  46449  meassre  46454  omessre  46487  omeiunltfirp  46496  hoissre  46521  hoiprodcl  46524  ovnsubaddlem1  46547  hoiprodcl3  46557  hoidmvcl  46559  hsphoidmvle2  46562  hsphoidmvle  46563  sge0hsphoire  46566  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  ovnhoilem1  46578  ovnhoilem2  46579  ovnhoi  46580  ovnlecvr2  46587  hspdifhsp  46593  hoidifhspdmvle  46597  hoiqssbllem1  46599  hoiqssbllem2  46600  hoiqssbllem3  46601  hspmbllem1  46603  hspmbllem2  46604  volicorege0  46614  ovolval5lem1  46629  ovolval5lem2  46630  iinhoiicclem  46650  iinhoiicc  46651  iunhoiioolem  46652  iunhoiioo  46653  vonioolem2  46658  vonicclem2  46661  vonsn  46668  pimltmnf2f  46674  pimconstlt0  46678  pimgtpnf2f  46682  salpreimagelt  46684  salpreimalegt  46686  preimageiingt  46697  preimaleiinlt  46698  pimrecltneg  46701  issmflem  46704  issmflelem  46721  issmfgtlem  46732  issmfgt  46733  smfaddlem1  46740  issmfgelem  46746  issmfge  46747  smfpimioompt  46763  smfresal  46765  smfrec  46766  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  smfmullem4  46771  smfpimbor1lem1  46775  smfsuplem1  46788  smflimsuplem4  46800  smfliminflem  46807  smfdmmblpimne  46814  smfpimne  46816  smfpimne2  46817  fsupdm  46819  finfdm  46823  smfinfdmmbllem  46825  bgoldbtbnd  47771  eenglngeehlnmlem2  48666