Theorem rexrd 11247

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-xr 11235

This theorem is referenced by:  xnn0xr  12570  rpxr  13014  rpxrd  13049  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  13586  addmodid  13943  hashnnn0genn0  14367  hashunsnggt  14418  sgnsub  15131  sgnmul  15132  sgnmulsgn  15134  elicc4abs  15359  caucvgrlem  15712  fprodge1  16037  pcxcl  16909  pcdvdsb  16917  pcaddlem  16936  ramcl2lem  17057  ramlb  17067  0ram  17068  setsstruct  17224  prdsxmetlem  24482  xblss2ps  24515  xblss2  24516  blss2ps  24517  blss2  24518  blhalf  24519  metustto  24667  metustexhalf  24670  nmoi  24842  nmoix  24843  nmoi2  24844  nmoleub  24845  qdensere  24883  cnblcld  24888  ioo2blex  24908  tgioo  24910  blcvx  24912  zcld  24928  recld2  24929  iccntr  24936  icccmplem1  24937  reconnlem1  24941  reconnlem2  24942  opnreen  24946  metnrmlem3  24976  icoopnst  25055  iocopnst  25056  cnheibor  25071  lebnumii  25082  nmoleub2lem  25230  lmnn  25379  iscau3  25394  minveclem4  25548  ivthlem1  25567  ivthlem2  25568  ivthlem3  25569  ivth2  25571  ivthle  25572  ivthle2  25573  ivthicc  25574  evthicc  25575  cniccbdd  25577  ovolgelb  25596  ovollb2lem  25604  ovolunlem1  25613  ovoliunlem1  25618  ovoliunlem2  25619  ovoliun  25621  ovolscalem1  25629  ovolicc1  25632  ovolicc2lem4  25636  ovolicc2lem5  25637  ovolicc2  25638  ovolicc  25639  nulmbl2  25652  voliunlem2  25667  ioombl1lem4  25677  ioorcl2  25688  uniioombllem1  25697  uniioombllem2a  25698  uniioombllem3  25701  dyaddisjlem  25711  dyadmaxlem  25713  opnmbllem  25717  volivth  25723  vitalilem4  25727  mbfmulc2lem  25763  mbfmax  25765  mbfposr  25768  ismbf3d  25770  mbfaddlem  25776  mbflimsup  25782  mbfi1fseqlem4  25834  itg2lcl  25843  xrge0f  25847  itg2itg1  25852  itg2const2  25857  itg2seq  25858  itg2uba  25859  itg2lea  25860  itg2mulclem  25862  itg2mulc  25863  itg2splitlem  25864  itg2split  25865  itg2monolem2  25867  itg2monolem3  25868  itg2mono  25869  itg2gt0  25876  itg2cnlem1  25877  itg2cnlem2  25878  itg2cn  25879  iblss  25921  itgle  25926  itgeqa  25930  itgioo  25932  ibladdlem  25936  iblabs  25945  iblabsr  25946  iblmulc2  25947  itgsplit  25952  itgspliticc  25953  itgsplitioo  25954  bddmulibl  25955  bddiblnc  25958  ditgcl  25974  ditgswap  25975  ditgsplitlem  25976  dvferm1lem  26100  dvferm2lem  26102  dvferm  26104  rollelem  26105  rolle  26106  cmvth  26107  mvth  26108  dvlip  26109  dvlip2  26111  c1liplem1  26112  c1lip1  26113  dveq0  26116  dvgt0lem1  26118  dvivthlem1  26124  dvivth  26126  lhop1lem  26129  lhop1  26130  lhop2  26131  lhop  26132  dvcnvrelem1  26133  dvcnvre  26135  dvcvx  26136  dvfsumle  26137  dvfsumge  26138  dvfsumabs  26139  dvfsumlem2  26143  dvfsumlem3  26144  dvfsumlem4  26145  dvfsumrlimge0  26146  dvfsumrlim2  26148  ftc1lem1  26151  ftc1lem2  26152  ftc1a  26153  ftc1lem4  26155  ftc2  26160  ftc2ditglem  26161  itgparts  26163  itgsubstlem  26164  itgsubst  26165  itgpowd  26166  degltlem1  26186  deg1ge  26212  coe1mul3  26213  deg1sublt  26224  deg1mul2  26228  deg1tmle  26232  deg1tm  26233  idomrootle  26287  plypf1  26326  taylfvallem1  26474  tayl0  26479  pserulm  26539  psercnlem1  26542  pserdvlem1  26544  pserdvlem2  26545  abelthlem3  26550  abelth  26558  efcvx  26566  logno1  26755  logtayl  26779  xrlimcnp  27087  logfacbnd3  27341  log2sumbnd  27662  pntpbnd2  27705  pntibndlem3  27710  ttgcontlem1  29139  nmooge0  31024  nmoub3i  31030  isblo3i  31058  ubthlem1  31127  minvecolem4  31137  nmopge0  32168  nmfnge0  32184  nmophmi  32288  branmfn  32362  sgnval2  32988  nn0mnfxrd  33004  xaddeq0  33006  xlt2addrd  33012  sgnmulsgp  33084  xmulcand  33148  xreceu  33149  xdivrec  33154  fsumrp0cl  33249  xrge0slmod  33578  ply1degltel  33796  ply1degleel  33797  ply1degltlss  33798  ply1degltdimlem  33924  ply1degltdim  33925  fldextrspundgdvdslem  33982  extdgfialglem1  33994  cos9thpiminplylem2  34085  cnre2csqlem  34212  tpr2rico  34214  xrge0iifcnv  34235  xrge0iifhom  34239  lmxrge0  34254  esumfsup  34372  esumpcvgval  34380  esumcvg  34388  dya2iocress  34576  dya2iocbrsiga  34577  dya2icobrsiga  34578  dya2icoseg  34579  dya2iocucvr  34586  sxbrsigalem2  34588  omssubaddlem  34601  omssubadd  34602  orvcgteel  34770  dstrvprob  34774  orvclteel  34775  signstcl  34864  signstf  34865  signstf0  34867  signstfvn  34868  signsvtn0  34869  signsvfn  34881  signsvfpn  34884  signsvfnn  34885  ftc2re  34897  cvmliftlem6  35648  cvmliftlem7  35649  cvmliftlem8  35650  cvmliftlem9  35651  cvmliftlem10  35652  cvmliftlem13  35654  ivthALT  36703  iooelexlt  37863  relowlssretop  37864  relowlpssretop  37865  sin2h  38116  cos2h  38117  tan2h  38118  poimirlem30  38156  poimir  38159  heicant  38161  opnmbllem0  38162  mblfinlem1  38163  mblfinlem2  38164  mblfinlem3  38165  mblfinlem4  38166  ismblfin  38167  itg2addnclem  38177  itg2addnclem2  38178  itg2gt0cn  38181  ibladdnclem  38182  iblabsnclem  38189  iblabsnc  38190  iblmulc2nc  38191  ftc1cnnclem  38197  ftc1anclem1  38199  ftc1anclem4  38202  ftc1anclem5  38203  ftc1anclem6  38204  ftc1anclem7  38205  ftc1anclem8  38206  ftc1anc  38207  ftc2nc  38208  areacirclem1  38214  areacirclem5  38218  areacirc  38219  isbnd3  38290  blbnd  38293  prdsbnd  38299  prdsbnd2  38301  cntotbnd  38302  dvrelog3  42689  0nonelalab  42691  dvrelogpow2b  42692  dvle2  42696  aks4d1p1p6  42697  aks4d1p1p5  42699  aks6d1c6lem3  42796  aks6d1c7lem2  42805  unitscyglem5  42823  idomodle  43775  imo72b2  44755  cvgdvgrat  44882  radcnvrat  44883  rfcnpre3  45612  rfcnpre4  45613  absfico  45793  nnxrd  45852  lefldiveq  45870  lttri5d  45877  supxrgere  45908  supxrgelem  45912  supxrge  45913  xralrple2  45929  infxr  45941  infleinflem1  45944  infleinflem2  45945  xralrple4  45947  xralrple3  45948  xrralrecnnle  45957  xrralrecnnge  45964  supxrunb3  45973  unb2ltle  45988  zxrd  46026  gtnelioc  46066  ltnelicc  46072  iooabslt  46074  gtnelicc  46075  eliooshift  46081  iocopn  46095  eliccelioc  46096  iooshift  46097  icoopn  46100  ge0lere  46107  iooiinicc  46117  sqrlearg  46128  iooiinioc  46131  uzinico  46134  preimaiocmnf  46135  uzubioo  46140  fsumge0cl  46148  limciccioolb  46196  lptioo1  46207  limcicciooub  46210  ltmod  46211  lptre2pt  46213  limsupre  46214  limcresiooub  46215  limcresioolb  46216  limcleqr  46217  limsupresico  46273  limsuppnfdlem  46274  limsupub  46277  limsupequzlem  46295  limsupre2lem  46297  limsupre3lem  46305  limsupvaluz2  46311  supcnvlimsup  46313  liminfresico  46344  limsup10exlem  46345  liminflelimsuplem  46348  limsupgtlem  46350  liminfval4  46362  liminfvaluz2  46368  limsupvaluz4  46373  liminflimsupclim  46380  xlimxrre  46404  xlimmnfvlem1  46405  xlimmnfv  46407  xlimpnfvlem1  46409  xlimpnfv  46411  sinaover2ne0  46441  ioccncflimc  46458  icccncfext  46460  icocncflimc  46462  cncfiooicclem1  46466  cncfiooicc  46467  cncfiooiccre  46468  cncfioobdlem  46469  dvbdfbdioolem1  46501  dvbdfbdioolem2  46502  dvbdfbdioo  46503  ioodvbdlimc1lem1  46504  ioodvbdlimc1lem2  46505  ioodvbdlimc1  46506  ioodvbdlimc2lem  46507  ioodvbdlimc2  46508  ditgeqiooicc  46533  iblsplit  46539  itgcoscmulx  46542  ibliooicc  46544  iblspltprt  46546  itgsincmulx  46547  itgsubsticc  46549  itgioocnicc  46550  iblcncfioo  46551  itgspltprt  46552  itgiccshift  46553  volioore  46563  voliooico  46565  voliooicof  46569  voliccico  46572  stoweidlem34  46607  stoweidlem52  46625  stirlinglem5  46651  dirkercncflem1  46676  dirkercncflem4  46679  fourierdlem4  46684  fourierdlem10  46690  fourierdlem19  46699  fourierdlem20  46700  fourierdlem24  46704  fourierdlem25  46705  fourierdlem26  46706  fourierdlem27  46707  fourierdlem28  46708  fourierdlem31  46711  fourierdlem32  46712  fourierdlem33  46713  fourierdlem35  46715  fourierdlem37  46717  fourierdlem40  46720  fourierdlem41  46721  fourierdlem43  46723  fourierdlem44  46724  fourierdlem46  46725  fourierdlem47  46726  fourierdlem48  46727  fourierdlem49  46728  fourierdlem50  46729  fourierdlem51  46730  fourierdlem52  46731  fourierdlem54  46733  fourierdlem57  46736  fourierdlem59  46738  fourierdlem60  46739  fourierdlem61  46740  fourierdlem62  46741  fourierdlem63  46742  fourierdlem64  46743  fourierdlem65  46744  fourierdlem68  46747  fourierdlem69  46748  fourierdlem70  46749  fourierdlem72  46751  fourierdlem73  46752  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem78  46757  fourierdlem79  46758  fourierdlem81  46760  fourierdlem82  46761  fourierdlem84  46763  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem92  46771  fourierdlem93  46772  fourierdlem94  46773  fourierdlem97  46776  fourierdlem100  46779  fourierdlem101  46780  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem107  46786  fourierdlem109  46788  fourierdlem111  46790  fourierdlem112  46791  fourierdlem113  46792  fourierdlem114  46793  sqwvfoura  46801  fouriersw  46804  etransclem23  46830  etransclem46  46853  qndenserrnbllem  46867  rrxsnicc  46873  ioorrnopnlem  46877  ioorrnopnxrlem  46879  salgencntex  46916  sge0cl  46954  sge0fsum  46960  sge0iunmptlemre  46988  sge0isum  47000  sge0ad2en  47004  sge0xaddlem1  47006  sge0xaddlem2  47007  sge0reuz  47020  voliunsge0lem  47045  meassre  47050  omessre  47083  omeiunltfirp  47092  hoissre  47117  hoiprodcl  47120  ovnsubaddlem1  47143  hoiprodcl3  47153  hoidmvcl  47155  hsphoidmvle2  47158  hsphoidmvle  47159  sge0hsphoire  47162  hoidmv1lelem1  47164  hoidmv1lelem2  47165  hoidmv1lelem3  47166  hoidmv1le  47167  hoidmvlelem1  47168  hoidmvlelem2  47169  hoidmvlelem3  47170  hoidmvlelem4  47171  ovnhoilem1  47174  ovnhoilem2  47175  ovnhoi  47176  ovnlecvr2  47183  hspdifhsp  47189  hoidifhspdmvle  47193  hoiqssbllem1  47195  hoiqssbllem2  47196  hoiqssbllem3  47197  hspmbllem1  47199  hspmbllem2  47200  volicorege0  47210  ovolval5lem1  47225  ovolval5lem2  47226  iinhoiicclem  47246  iinhoiicc  47247  iunhoiioolem  47248  iunhoiioo  47249  vonioolem2  47254  vonicclem2  47257  vonsn  47264  pimltmnf2f  47270  pimconstlt0  47274  pimgtpnf2f  47278  salpreimagelt  47280  salpreimalegt  47282  preimageiingt  47293  preimaleiinlt  47294  pimrecltneg  47297  issmflem  47300  issmflelem  47317  issmfgtlem  47328  issmfgt  47329  smfaddlem1  47336  issmfgelem  47342  issmfge  47343  smfpimioompt  47359  smfresal  47361  smfrec  47362  smfmullem1  47364  smfmullem2  47365  smfmullem3  47366  smfmullem4  47367  smfpimbor1lem1  47371  smfsuplem1  47384  smflimsuplem4  47396  smfliminflem  47403  smfdmmblpimne  47410  smfpimne  47412  smfpimne2  47413  fsupdm  47415  finfdm  47419  smfinfdmmbllem  47421  bgoldbtbnd  48430  eenglngeehlnmlem2  49370