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 4006	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-xr 11328

This theorem is referenced by:  xnn0xr  12630  rpxr  13066  rpxrd  13100  max0sub  13258  qextltlem  13264  xralrple  13267  xnegcl  13275  xaddf  13286  xnn0lem1lt  13306  xnn0lenn0nn0  13307  xmulf  13334  xadddi  13357  xrub  13374  supxrre  13389  infxrre  13398  ixxub  13428  ixxlb  13429  ioo0  13432  ico0  13453  ioc0  13454  iooshf  13486  icoshftf1o  13534  supicc  13561  supiccub  13562  supicclub  13563  xnn0xrge0  13566  ssfzunsn  13630  addmodid  13970  hashnnn0genn0  14392  hashunsnggt  14443  elicc4abs  15368  caucvgrlem  15721  fprodge1  16043  pcxcl  16908  pcdvdsb  16916  pcaddlem  16935  ramcl2lem  17056  ramlb  17066  0ram  17067  setsstruct  17223  prdsxmetlem  24399  xblss2ps  24432  xblss2  24433  blss2ps  24434  blss2  24435  blhalf  24436  metustto  24587  metustexhalf  24590  nmoi  24770  nmoix  24771  nmoi2  24772  nmoleub  24773  qdensere  24811  cnblcld  24816  ioo2blex  24835  tgioo  24837  blcvx  24839  zcld  24854  recld2  24855  iccntr  24862  icccmplem1  24863  reconnlem1  24867  reconnlem2  24868  opnreen  24872  metnrmlem3  24902  icoopnst  24988  iocopnst  24989  cnheibor  25006  lebnumii  25017  nmoleub2lem  25166  lmnn  25316  iscau3  25331  minveclem4  25485  ivthlem1  25505  ivthlem2  25506  ivthlem3  25507  ivth2  25509  ivthle  25510  ivthle2  25511  ivthicc  25512  evthicc  25513  cniccbdd  25515  ovolgelb  25534  ovollb2lem  25542  ovolunlem1  25551  ovoliunlem1  25556  ovoliunlem2  25557  ovoliun  25559  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem4  25574  ovolicc2lem5  25575  ovolicc2  25576  ovolicc  25577  nulmbl2  25590  voliunlem2  25605  ioombl1lem4  25615  ioorcl2  25626  uniioombllem1  25635  uniioombllem2a  25636  uniioombllem3  25639  dyaddisjlem  25649  dyadmaxlem  25651  opnmbllem  25655  volivth  25661  vitalilem4  25665  mbfmulc2lem  25701  mbfmax  25703  mbfposr  25706  ismbf3d  25708  mbfaddlem  25714  mbflimsup  25720  mbfi1fseqlem4  25773  itg2lcl  25782  xrge0f  25786  itg2itg1  25791  itg2const2  25796  itg2seq  25797  itg2uba  25798  itg2lea  25799  itg2mulclem  25801  itg2mulc  25802  itg2splitlem  25803  itg2split  25804  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  itg2cn  25818  iblss  25860  itgle  25865  itgeqa  25869  itgioo  25871  ibladdlem  25875  iblabs  25884  iblabsr  25885  iblmulc2  25886  itgsplit  25891  itgspliticc  25892  itgsplitioo  25893  bddmulibl  25894  bddiblnc  25897  ditgcl  25913  ditgswap  25914  ditgsplitlem  25915  dvferm1lem  26042  dvferm2lem  26044  dvferm  26046  rollelem  26047  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlip2  26054  c1liplem1  26055  c1lip1  26056  dveq0  26059  dvgt0lem1  26061  dvivthlem1  26067  dvivth  26069  lhop1lem  26072  lhop1  26073  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcnvre  26078  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlimge0  26091  dvfsumrlim2  26093  ftc1lem1  26096  ftc1lem2  26097  ftc1a  26098  ftc1lem4  26100  ftc2  26105  ftc2ditglem  26106  itgparts  26108  itgsubstlem  26109  itgsubst  26110  itgpowd  26111  degltlem1  26131  deg1ge  26157  coe1mul3  26158  deg1sublt  26169  deg1mul2  26173  deg1tmle  26177  deg1tm  26178  idomrootle  26232  plypf1  26271  taylfvallem1  26416  tayl0  26421  pserulm  26483  psercnlem1  26487  pserdvlem1  26489  pserdvlem2  26490  abelthlem3  26495  abelth  26503  efcvx  26511  logno1  26696  logtayl  26720  xrlimcnp  27029  logfacbnd3  27285  log2sumbnd  27606  pntpbnd2  27649  pntibndlem3  27654  ttgcontlem1  28917  nmooge0  30799  nmoub3i  30805  isblo3i  30833  ubthlem1  30902  minvecolem4  30912  nmopge0  31943  nmfnge0  31959  nmophmi  32063  branmfn  32137  xaddeq0  32760  xlt2addrd  32765  xmulcand  32885  xreceu  32886  xdivrec  32891  fsumrp0cl  33007  xrge0slmod  33341  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ply1degltdimlem  33635  ply1degltdim  33636  cnre2csqlem  33856  tpr2rico  33858  xrge0iifcnv  33879  xrge0iifhom  33883  lmxrge0  33898  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  dya2iocress  34239  dya2iocbrsiga  34240  dya2icobrsiga  34241  dya2icoseg  34242  dya2iocucvr  34249  sxbrsigalem2  34251  omssubaddlem  34264  omssubadd  34265  orvcgteel  34432  dstrvprob  34436  orvclteel  34437  sgnmul  34507  sgnsub  34509  sgnmulsgn  34514  sgnmulsgp  34515  signstcl  34542  signstf  34543  signstf0  34545  signstfvn  34546  signsvtn0  34547  signsvfn  34559  signsvfpn  34562  signsvfnn  34563  ftc2re  34575  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem10  35262  cvmliftlem13  35264  ivthALT  36301  iooelexlt  37328  relowlssretop  37329  relowlpssretop  37330  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem30  37610  poimir  37613  heicant  37615  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnclem2  37632  itg2gt0cn  37635  ibladdnclem  37636  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  ftc1cnnclem  37651  ftc1anclem1  37653  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  ftc2nc  37662  areacirclem1  37668  areacirclem5  37672  areacirc  37673  isbnd3  37744  blbnd  37747  prdsbnd  37753  prdsbnd2  37755  cntotbnd  37756  dvrelog3  42022  0nonelalab  42024  dvrelogpow2b  42025  dvle2  42029  aks4d1p1p6  42030  aks4d1p1p5  42032  aks6d1c6lem3  42129  aks6d1c7lem2  42138  unitscyglem5  42156  idomodle  43152  imo72b2  44134  cvgdvgrat  44282  radcnvrat  44283  rfcnpre3  44933  rfcnpre4  44934  absfico  45125  nnxrd  45188  lefldiveq  45207  lttri5d  45214  supxrgere  45248  supxrgelem  45252  supxrge  45253  xralrple2  45269  infxr  45282  infleinflem1  45285  infleinflem2  45286  xralrple4  45288  xralrple3  45289  xrralrecnnle  45298  xrralrecnnge  45305  supxrunb3  45314  unb2ltle  45330  zxrd  45368  gtnelioc  45409  ltnelicc  45415  iooabslt  45417  gtnelicc  45418  eliooshift  45424  iocopn  45438  eliccelioc  45439  iooshift  45440  icoopn  45443  ge0lere  45450  iooiinicc  45460  sqrlearg  45471  iooiinioc  45474  uzinico  45478  preimaiocmnf  45479  uzubioo  45485  fsumge0cl  45494  limciccioolb  45542  lptioo1  45553  limcicciooub  45558  ltmod  45559  lptre2pt  45561  limsupre  45562  limcresiooub  45563  limcresioolb  45564  limcleqr  45565  limsupresico  45621  limsuppnfdlem  45622  limsupub  45625  limsupequzlem  45643  limsupre2lem  45645  limsupre3lem  45653  limsupvaluz2  45659  supcnvlimsup  45661  liminfresico  45692  limsup10exlem  45693  liminflelimsuplem  45696  limsupgtlem  45698  liminfval4  45710  liminfvaluz2  45716  limsupvaluz4  45721  liminflimsupclim  45728  xlimxrre  45752  xlimmnfvlem1  45753  xlimmnfv  45755  xlimpnfvlem1  45757  xlimpnfv  45759  sinaover2ne0  45789  ioccncflimc  45806  icccncfext  45808  icocncflimc  45810  cncfiooicclem1  45814  cncfiooicc  45815  cncfiooiccre  45816  cncfioobdlem  45817  dvbdfbdioolem1  45849  dvbdfbdioolem2  45850  dvbdfbdioo  45851  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc1  45854  ioodvbdlimc2lem  45855  ioodvbdlimc2  45856  ditgeqiooicc  45881  iblsplit  45887  itgcoscmulx  45890  ibliooicc  45892  iblspltprt  45894  itgsincmulx  45895  itgsubsticc  45897  itgioocnicc  45898  iblcncfioo  45899  itgspltprt  45900  itgiccshift  45901  volioore  45911  voliooico  45913  voliooicof  45917  voliccico  45920  stoweidlem34  45955  stoweidlem52  45973  stirlinglem5  45999  dirkercncflem1  46024  dirkercncflem4  46027  fourierdlem4  46032  fourierdlem10  46038  fourierdlem19  46047  fourierdlem20  46048  fourierdlem24  46052  fourierdlem25  46053  fourierdlem26  46054  fourierdlem27  46055  fourierdlem28  46056  fourierdlem31  46059  fourierdlem32  46060  fourierdlem33  46061  fourierdlem35  46063  fourierdlem37  46065  fourierdlem40  46068  fourierdlem41  46069  fourierdlem43  46071  fourierdlem44  46072  fourierdlem46  46073  fourierdlem47  46074  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem52  46079  fourierdlem54  46081  fourierdlem57  46084  fourierdlem59  46086  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem68  46095  fourierdlem69  46096  fourierdlem70  46097  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem84  46111  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem94  46121  fourierdlem97  46124  fourierdlem100  46127  fourierdlem101  46128  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem109  46136  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fourierdlem114  46141  sqwvfoura  46149  fouriersw  46152  etransclem23  46178  etransclem46  46201  qndenserrnbllem  46215  rrxsnicc  46221  ioorrnopnlem  46225  ioorrnopnxrlem  46227  salgencntex  46264  sge0cl  46302  sge0fsum  46308  sge0iunmptlemre  46336  sge0isum  46348  sge0ad2en  46352  sge0xaddlem1  46354  sge0xaddlem2  46355  sge0reuz  46368  voliunsge0lem  46393  meassre  46398  omessre  46431  omeiunltfirp  46440  hoissre  46465  hoiprodcl  46468  ovnsubaddlem1  46491  hoiprodcl3  46501  hoidmvcl  46503  hsphoidmvle2  46506  hsphoidmvle  46507  sge0hsphoire  46510  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  ovnhoilem1  46522  ovnhoilem2  46523  ovnhoi  46524  ovnlecvr2  46531  hspdifhsp  46537  hoidifhspdmvle  46541  hoiqssbllem1  46543  hoiqssbllem2  46544  hoiqssbllem3  46545  hspmbllem1  46547  hspmbllem2  46548  volicorege0  46558  ovolval5lem1  46573  ovolval5lem2  46574  iinhoiicclem  46594  iinhoiicc  46595  iunhoiioolem  46596  iunhoiioo  46597  vonioolem2  46602  vonicclem2  46605  vonsn  46612  pimltmnf2f  46618  pimconstlt0  46622  pimgtpnf2f  46626  salpreimagelt  46628  salpreimalegt  46630  preimageiingt  46641  preimaleiinlt  46642  pimrecltneg  46645  issmflem  46648  issmflelem  46665  issmfgtlem  46676  issmfgt  46677  smfaddlem1  46684  issmfgelem  46690  issmfge  46691  smfpimioompt  46707  smfresal  46709  smfrec  46710  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  smfmullem4  46715  smfpimbor1lem1  46719  smfsuplem1  46732  smflimsuplem4  46744  smfliminflem  46751  smfdmmblpimne  46758  smfpimne  46760  smfpimne2  46761  fsupdm  46763  finfdm  46767  smfinfdmmbllem  46769  bgoldbtbnd  47683  eenglngeehlnmlem2  48472