Theorem rexrd 11195

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℝ^*cxr 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-xr 11183

This theorem is referenced by:  xnn0xr  12515  rpxr  12952  rpxrd  12987  max0sub  13148  qextltlem  13154  xralrple  13157  xnegcl  13165  xaddf  13176  xnn0lem1lt  13196  xnn0lenn0nn0  13197  xmulf  13224  xadddi  13247  xrub  13264  supxrre  13279  infxrre  13289  ixxub  13319  ixxlb  13320  ioo0  13323  ico0  13344  ioc0  13345  iooshf  13379  icoshftf1o  13427  supicc  13454  supiccub  13455  supicclub  13456  xnn0xrge0  13459  ssfzunsn  13524  addmodid  13881  hashnnn0genn0  14305  hashunsnggt  14356  elicc4abs  15282  caucvgrlem  15635  fprodge1  15960  pcxcl  16832  pcdvdsb  16840  pcaddlem  16859  ramcl2lem  16980  ramlb  16990  0ram  16991  setsstruct  17146  prdsxmetlem  24333  xblss2ps  24366  xblss2  24367  blss2ps  24368  blss2  24369  blhalf  24370  metustto  24518  metustexhalf  24521  nmoi  24693  nmoix  24694  nmoi2  24695  nmoleub  24696  qdensere  24734  cnblcld  24739  ioo2blex  24759  tgioo  24761  blcvx  24763  zcld  24779  recld2  24780  iccntr  24787  icccmplem1  24788  reconnlem1  24792  reconnlem2  24793  opnreen  24797  metnrmlem3  24827  icoopnst  24906  iocopnst  24907  cnheibor  24922  lebnumii  24933  nmoleub2lem  25081  lmnn  25230  iscau3  25245  minveclem4  25399  ivthlem1  25418  ivthlem2  25419  ivthlem3  25420  ivth2  25422  ivthle  25423  ivthle2  25424  ivthicc  25425  evthicc  25426  cniccbdd  25428  ovolgelb  25447  ovollb2lem  25455  ovolunlem1  25464  ovoliunlem1  25469  ovoliunlem2  25470  ovoliun  25472  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem4  25487  ovolicc2lem5  25488  ovolicc2  25489  ovolicc  25490  nulmbl2  25503  voliunlem2  25518  ioombl1lem4  25528  ioorcl2  25539  uniioombllem1  25548  uniioombllem2a  25549  uniioombllem3  25552  dyaddisjlem  25562  dyadmaxlem  25564  opnmbllem  25568  volivth  25574  vitalilem4  25578  mbfmulc2lem  25614  mbfmax  25616  mbfposr  25619  ismbf3d  25621  mbfaddlem  25627  mbflimsup  25633  mbfi1fseqlem4  25685  itg2lcl  25694  xrge0f  25698  itg2itg1  25703  itg2const2  25708  itg2seq  25709  itg2uba  25710  itg2lea  25711  itg2mulclem  25713  itg2mulc  25714  itg2splitlem  25715  itg2split  25716  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  itg2cn  25730  iblss  25772  itgle  25777  itgeqa  25781  itgioo  25783  ibladdlem  25787  iblabs  25796  iblabsr  25797  iblmulc2  25798  itgsplit  25803  itgspliticc  25804  itgsplitioo  25805  bddmulibl  25806  bddiblnc  25809  ditgcl  25825  ditgswap  25826  ditgsplitlem  25827  dvferm1lem  25951  dvferm2lem  25953  dvferm  25955  rollelem  25956  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  dvlip2  25962  c1liplem1  25963  c1lip1  25964  dveq0  25967  dvgt0lem1  25969  dvivthlem1  25975  dvivth  25977  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  dvcnvrelem1  25984  dvcnvre  25986  dvcvx  25987  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlimge0  25997  dvfsumrlim2  25999  ftc1lem1  26002  ftc1lem2  26003  ftc1a  26004  ftc1lem4  26006  ftc2  26011  ftc2ditglem  26012  itgparts  26014  itgsubstlem  26015  itgsubst  26016  itgpowd  26017  degltlem1  26037  deg1ge  26063  coe1mul3  26064  deg1sublt  26075  deg1mul2  26079  deg1tmle  26083  deg1tm  26084  idomrootle  26138  plypf1  26177  taylfvallem1  26322  tayl0  26327  pserulm  26387  psercnlem1  26390  pserdvlem1  26392  pserdvlem2  26393  abelthlem3  26398  abelth  26406  efcvx  26414  logno1  26600  logtayl  26624  xrlimcnp  26932  logfacbnd3  27186  log2sumbnd  27507  pntpbnd2  27550  pntibndlem3  27555  ttgcontlem1  28953  nmooge0  30838  nmoub3i  30844  isblo3i  30872  ubthlem1  30941  minvecolem4  30951  nmopge0  31982  nmfnge0  31998  nmophmi  32102  branmfn  32176  sgnval2  32808  nn0mnfxrd  32824  xaddeq0  32826  xlt2addrd  32832  sgnmul  32908  sgnsub  32910  sgnmulsgn  32915  sgnmulsgp  32916  xmulcand  32980  xreceu  32981  xdivrec  32986  fsumrp0cl  33081  xrge0slmod  33408  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  ply1degltdimlem  33766  ply1degltdim  33767  fldextrspundgdvdslem  33824  extdgfialglem1  33836  cos9thpiminplylem2  33927  cnre2csqlem  34054  tpr2rico  34056  xrge0iifcnv  34077  xrge0iifhom  34081  lmxrge0  34096  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  dya2iocress  34418  dya2iocbrsiga  34419  dya2icobrsiga  34420  dya2icoseg  34421  dya2iocucvr  34428  sxbrsigalem2  34430  omssubaddlem  34443  omssubadd  34444  orvcgteel  34612  dstrvprob  34616  orvclteel  34617  signstcl  34709  signstf  34710  signstf0  34712  signstfvn  34713  signsvtn0  34714  signsvfn  34726  signsvfpn  34729  signsvfnn  34730  ftc2re  34742  cvmliftlem6  35472  cvmliftlem7  35473  cvmliftlem8  35474  cvmliftlem9  35475  cvmliftlem10  35476  cvmliftlem13  35478  ivthALT  36517  iooelexlt  37678  relowlssretop  37679  relowlpssretop  37680  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem30  37971  poimir  37974  heicant  37976  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem  37992  itg2addnclem2  37993  itg2gt0cn  37996  ibladdnclem  37997  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  ftc1cnnclem  38012  ftc1anclem1  38014  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  ftc2nc  38023  areacirclem1  38029  areacirclem5  38033  areacirc  38034  isbnd3  38105  blbnd  38108  prdsbnd  38114  prdsbnd2  38116  cntotbnd  38117  dvrelog3  42504  0nonelalab  42506  dvrelogpow2b  42507  dvle2  42511  aks4d1p1p6  42512  aks4d1p1p5  42514  aks6d1c6lem3  42611  aks6d1c7lem2  42620  unitscyglem5  42638  idomodle  43619  imo72b2  44599  cvgdvgrat  44740  radcnvrat  44741  rfcnpre3  45464  rfcnpre4  45465  absfico  45647  nnxrd  45707  lefldiveq  45725  lttri5d  45732  supxrgere  45763  supxrgelem  45767  supxrge  45768  xralrple2  45784  infxr  45796  infleinflem1  45799  infleinflem2  45800  xralrple4  45802  xralrple3  45803  xrralrecnnle  45812  xrralrecnnge  45819  supxrunb3  45828  unb2ltle  45843  zxrd  45881  gtnelioc  45921  ltnelicc  45927  iooabslt  45929  gtnelicc  45930  eliooshift  45936  iocopn  45950  eliccelioc  45951  iooshift  45952  icoopn  45955  ge0lere  45962  iooiinicc  45972  sqrlearg  45983  iooiinioc  45986  uzinico  45989  preimaiocmnf  45990  uzubioo  45995  fsumge0cl  46003  limciccioolb  46051  lptioo1  46062  limcicciooub  46065  ltmod  46066  lptre2pt  46068  limsupre  46069  limcresiooub  46070  limcresioolb  46071  limcleqr  46072  limsupresico  46128  limsuppnfdlem  46129  limsupub  46132  limsupequzlem  46150  limsupre2lem  46152  limsupre3lem  46160  limsupvaluz2  46166  supcnvlimsup  46168  liminfresico  46199  limsup10exlem  46200  liminflelimsuplem  46203  limsupgtlem  46205  liminfval4  46217  liminfvaluz2  46223  limsupvaluz4  46228  liminflimsupclim  46235  xlimxrre  46259  xlimmnfvlem1  46260  xlimmnfv  46262  xlimpnfvlem1  46264  xlimpnfv  46266  sinaover2ne0  46296  ioccncflimc  46313  icccncfext  46315  icocncflimc  46317  cncfiooicclem1  46321  cncfiooicc  46322  cncfiooiccre  46323  cncfioobdlem  46324  dvbdfbdioolem1  46356  dvbdfbdioolem2  46357  dvbdfbdioo  46358  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc1  46361  ioodvbdlimc2lem  46362  ioodvbdlimc2  46363  ditgeqiooicc  46388  iblsplit  46394  itgcoscmulx  46397  ibliooicc  46399  iblspltprt  46401  itgsincmulx  46402  itgsubsticc  46404  itgioocnicc  46405  iblcncfioo  46406  itgspltprt  46407  itgiccshift  46408  volioore  46418  voliooico  46420  voliooicof  46424  voliccico  46427  stoweidlem34  46462  stoweidlem52  46480  stirlinglem5  46506  dirkercncflem1  46531  dirkercncflem4  46534  fourierdlem4  46539  fourierdlem10  46545  fourierdlem19  46554  fourierdlem20  46555  fourierdlem24  46559  fourierdlem25  46560  fourierdlem26  46561  fourierdlem27  46562  fourierdlem28  46563  fourierdlem31  46566  fourierdlem32  46567  fourierdlem33  46568  fourierdlem35  46570  fourierdlem37  46572  fourierdlem40  46575  fourierdlem41  46576  fourierdlem43  46578  fourierdlem44  46579  fourierdlem46  46580  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem52  46586  fourierdlem54  46588  fourierdlem57  46591  fourierdlem59  46593  fourierdlem60  46594  fourierdlem61  46595  fourierdlem62  46596  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem68  46602  fourierdlem69  46603  fourierdlem70  46604  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem84  46618  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem94  46628  fourierdlem97  46631  fourierdlem100  46634  fourierdlem101  46635  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem109  46643  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fourierdlem114  46648  sqwvfoura  46656  fouriersw  46659  etransclem23  46685  etransclem46  46708  qndenserrnbllem  46722  rrxsnicc  46728  ioorrnopnlem  46732  ioorrnopnxrlem  46734  salgencntex  46771  sge0cl  46809  sge0fsum  46815  sge0iunmptlemre  46843  sge0isum  46855  sge0ad2en  46859  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0reuz  46875  voliunsge0lem  46900  meassre  46905  omessre  46938  omeiunltfirp  46947  hoissre  46972  hoiprodcl  46975  ovnsubaddlem1  46998  hoiprodcl3  47008  hoidmvcl  47010  hsphoidmvle2  47013  hsphoidmvle  47014  sge0hsphoire  47017  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  ovnhoilem1  47029  ovnhoilem2  47030  ovnhoi  47031  ovnlecvr2  47038  hspdifhsp  47044  hoidifhspdmvle  47048  hoiqssbllem1  47050  hoiqssbllem2  47051  hoiqssbllem3  47052  hspmbllem1  47054  hspmbllem2  47055  volicorege0  47065  ovolval5lem1  47080  ovolval5lem2  47081  iinhoiicclem  47101  iinhoiicc  47102  iunhoiioolem  47103  iunhoiioo  47104  vonioolem2  47109  vonicclem2  47112  vonsn  47119  pimltmnf2f  47125  pimconstlt0  47129  pimgtpnf2f  47133  salpreimagelt  47135  salpreimalegt  47137  preimageiingt  47148  preimaleiinlt  47149  pimrecltneg  47152  issmflem  47155  issmflelem  47172  issmfgtlem  47183  issmfgt  47184  smfaddlem1  47191  issmfgelem  47197  issmfge  47198  smfpimioompt  47214  smfresal  47216  smfrec  47217  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  smfmullem4  47222  smfpimbor1lem1  47226  smfsuplem1  47239  smflimsuplem4  47251  smfliminflem  47258  smfdmmblpimne  47265  smfpimne  47267  smfpimne2  47268  fsupdm  47270  finfdm  47274  smfinfdmmbllem  47276  bgoldbtbnd  48285  eenglngeehlnmlem2  49214