Theorem rexrd 11162

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11005  ℝ^*cxr 11145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-xr 11150

This theorem is referenced by:  xnn0xr  12459  rpxr  12900  rpxrd  12935  max0sub  13095  qextltlem  13101  xralrple  13104  xnegcl  13112  xaddf  13123  xnn0lem1lt  13143  xnn0lenn0nn0  13144  xmulf  13171  xadddi  13194  xrub  13211  supxrre  13226  infxrre  13236  ixxub  13266  ixxlb  13267  ioo0  13270  ico0  13291  ioc0  13292  iooshf  13326  icoshftf1o  13374  supicc  13401  supiccub  13402  supicclub  13403  xnn0xrge0  13406  ssfzunsn  13470  addmodid  13826  hashnnn0genn0  14250  hashunsnggt  14301  elicc4abs  15227  caucvgrlem  15580  fprodge1  15902  pcxcl  16773  pcdvdsb  16781  pcaddlem  16800  ramcl2lem  16921  ramlb  16931  0ram  16932  setsstruct  17087  prdsxmetlem  24284  xblss2ps  24317  xblss2  24318  blss2ps  24319  blss2  24320  blhalf  24321  metustto  24469  metustexhalf  24472  nmoi  24644  nmoix  24645  nmoi2  24646  nmoleub  24647  qdensere  24685  cnblcld  24690  ioo2blex  24710  tgioo  24712  blcvx  24714  zcld  24730  recld2  24731  iccntr  24738  icccmplem1  24739  reconnlem1  24743  reconnlem2  24744  opnreen  24748  metnrmlem3  24778  icoopnst  24864  iocopnst  24865  cnheibor  24882  lebnumii  24893  nmoleub2lem  25042  lmnn  25191  iscau3  25206  minveclem4  25360  ivthlem1  25380  ivthlem2  25381  ivthlem3  25382  ivth2  25384  ivthle  25385  ivthle2  25386  ivthicc  25387  evthicc  25388  cniccbdd  25390  ovolgelb  25409  ovollb2lem  25417  ovolunlem1  25426  ovoliunlem1  25431  ovoliunlem2  25432  ovoliun  25434  ovolscalem1  25442  ovolicc1  25445  ovolicc2lem4  25449  ovolicc2lem5  25450  ovolicc2  25451  ovolicc  25452  nulmbl2  25465  voliunlem2  25480  ioombl1lem4  25490  ioorcl2  25501  uniioombllem1  25510  uniioombllem2a  25511  uniioombllem3  25514  dyaddisjlem  25524  dyadmaxlem  25526  opnmbllem  25530  volivth  25536  vitalilem4  25540  mbfmulc2lem  25576  mbfmax  25578  mbfposr  25581  ismbf3d  25583  mbfaddlem  25589  mbflimsup  25595  mbfi1fseqlem4  25647  itg2lcl  25656  xrge0f  25660  itg2itg1  25665  itg2const2  25670  itg2seq  25671  itg2uba  25672  itg2lea  25673  itg2mulclem  25675  itg2mulc  25676  itg2splitlem  25677  itg2split  25678  itg2monolem2  25680  itg2monolem3  25681  itg2mono  25682  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  itg2cn  25692  iblss  25734  itgle  25739  itgeqa  25743  itgioo  25745  ibladdlem  25749  iblabs  25758  iblabsr  25759  iblmulc2  25760  itgsplit  25765  itgspliticc  25766  itgsplitioo  25767  bddmulibl  25768  bddiblnc  25771  ditgcl  25787  ditgswap  25788  ditgsplitlem  25789  dvferm1lem  25916  dvferm2lem  25918  dvferm  25920  rollelem  25921  rolle  25922  cmvth  25923  cmvthOLD  25924  mvth  25925  dvlip  25926  dvlip2  25928  c1liplem1  25929  c1lip1  25930  dveq0  25933  dvgt0lem1  25935  dvivthlem1  25941  dvivth  25943  lhop1lem  25946  lhop1  25947  lhop2  25948  lhop  25949  dvcnvrelem1  25950  dvcnvre  25952  dvcvx  25953  dvfsumle  25954  dvfsumleOLD  25955  dvfsumge  25956  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumlem3  25963  dvfsumlem4  25964  dvfsumrlimge0  25965  dvfsumrlim2  25967  ftc1lem1  25970  ftc1lem2  25971  ftc1a  25972  ftc1lem4  25974  ftc2  25979  ftc2ditglem  25980  itgparts  25982  itgsubstlem  25983  itgsubst  25984  itgpowd  25985  degltlem1  26005  deg1ge  26031  coe1mul3  26032  deg1sublt  26043  deg1mul2  26047  deg1tmle  26051  deg1tm  26052  idomrootle  26106  plypf1  26145  taylfvallem1  26292  tayl0  26297  pserulm  26359  psercnlem1  26363  pserdvlem1  26365  pserdvlem2  26366  abelthlem3  26371  abelth  26379  efcvx  26387  logno1  26573  logtayl  26597  xrlimcnp  26906  logfacbnd3  27162  log2sumbnd  27483  pntpbnd2  27526  pntibndlem3  27531  ttgcontlem1  28864  nmooge0  30745  nmoub3i  30751  isblo3i  30779  ubthlem1  30848  minvecolem4  30858  nmopge0  31889  nmfnge0  31905  nmophmi  32009  branmfn  32083  sgnval2  32716  xaddeq0  32734  xlt2addrd  32740  sgnmul  32816  sgnsub  32818  sgnmulsgn  32823  sgnmulsgp  32824  xmulcand  32899  xreceu  32900  xdivrec  32905  fsumrp0cl  33000  xrge0slmod  33311  ply1degltel  33553  ply1degleel  33554  ply1degltlss  33555  ply1degltdimlem  33633  ply1degltdim  33634  fldextrspundgdvdslem  33691  extdgfialglem1  33703  cos9thpiminplylem2  33794  cnre2csqlem  33921  tpr2rico  33923  xrge0iifcnv  33944  xrge0iifhom  33948  lmxrge0  33963  esumfsup  34081  esumpcvgval  34089  esumcvg  34097  dya2iocress  34285  dya2iocbrsiga  34286  dya2icobrsiga  34287  dya2icoseg  34288  dya2iocucvr  34295  sxbrsigalem2  34297  omssubaddlem  34310  omssubadd  34311  orvcgteel  34479  dstrvprob  34483  orvclteel  34484  signstcl  34576  signstf  34577  signstf0  34579  signstfvn  34580  signsvtn0  34581  signsvfn  34593  signsvfpn  34596  signsvfnn  34597  ftc2re  34609  cvmliftlem6  35332  cvmliftlem7  35333  cvmliftlem8  35334  cvmliftlem9  35335  cvmliftlem10  35336  cvmliftlem13  35338  ivthALT  36375  iooelexlt  37402  relowlssretop  37403  relowlpssretop  37404  sin2h  37656  cos2h  37657  tan2h  37658  poimirlem30  37696  poimir  37699  heicant  37701  opnmbllem0  37702  mblfinlem1  37703  mblfinlem2  37704  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  itg2addnclem  37717  itg2addnclem2  37718  itg2gt0cn  37721  ibladdnclem  37722  iblabsnclem  37729  iblabsnc  37730  iblmulc2nc  37731  ftc1cnnclem  37737  ftc1anclem1  37739  ftc1anclem4  37742  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  ftc2nc  37748  areacirclem1  37754  areacirclem5  37758  areacirc  37759  isbnd3  37830  blbnd  37833  prdsbnd  37839  prdsbnd2  37841  cntotbnd  37842  dvrelog3  42104  0nonelalab  42106  dvrelogpow2b  42107  dvle2  42111  aks4d1p1p6  42112  aks4d1p1p5  42114  aks6d1c6lem3  42211  aks6d1c7lem2  42220  unitscyglem5  42238  idomodle  43230  imo72b2  44211  cvgdvgrat  44352  radcnvrat  44353  rfcnpre3  45076  rfcnpre4  45077  absfico  45261  nnxrd  45321  lefldiveq  45339  lttri5d  45346  supxrgere  45378  supxrgelem  45382  supxrge  45383  xralrple2  45399  infxr  45411  infleinflem1  45414  infleinflem2  45415  xralrple4  45417  xralrple3  45418  xrralrecnnle  45427  xrralrecnnge  45434  supxrunb3  45443  unb2ltle  45459  zxrd  45497  gtnelioc  45537  ltnelicc  45543  iooabslt  45545  gtnelicc  45546  eliooshift  45552  iocopn  45566  eliccelioc  45567  iooshift  45568  icoopn  45571  ge0lere  45578  iooiinicc  45588  sqrlearg  45599  iooiinioc  45602  uzinico  45605  preimaiocmnf  45606  uzubioo  45611  fsumge0cl  45619  limciccioolb  45667  lptioo1  45678  limcicciooub  45681  ltmod  45682  lptre2pt  45684  limsupre  45685  limcresiooub  45686  limcresioolb  45687  limcleqr  45688  limsupresico  45744  limsuppnfdlem  45745  limsupub  45748  limsupequzlem  45766  limsupre2lem  45768  limsupre3lem  45776  limsupvaluz2  45782  supcnvlimsup  45784  liminfresico  45815  limsup10exlem  45816  liminflelimsuplem  45819  limsupgtlem  45821  liminfval4  45833  liminfvaluz2  45839  limsupvaluz4  45844  liminflimsupclim  45851  xlimxrre  45875  xlimmnfvlem1  45876  xlimmnfv  45878  xlimpnfvlem1  45880  xlimpnfv  45882  sinaover2ne0  45912  ioccncflimc  45929  icccncfext  45931  icocncflimc  45933  cncfiooicclem1  45937  cncfiooicc  45938  cncfiooiccre  45939  cncfioobdlem  45940  dvbdfbdioolem1  45972  dvbdfbdioolem2  45973  dvbdfbdioo  45974  ioodvbdlimc1lem1  45975  ioodvbdlimc1lem2  45976  ioodvbdlimc1  45977  ioodvbdlimc2lem  45978  ioodvbdlimc2  45979  ditgeqiooicc  46004  iblsplit  46010  itgcoscmulx  46013  ibliooicc  46015  iblspltprt  46017  itgsincmulx  46018  itgsubsticc  46020  itgioocnicc  46021  iblcncfioo  46022  itgspltprt  46023  itgiccshift  46024  volioore  46034  voliooico  46036  voliooicof  46040  voliccico  46043  stoweidlem34  46078  stoweidlem52  46096  stirlinglem5  46122  dirkercncflem1  46147  dirkercncflem4  46150  fourierdlem4  46155  fourierdlem10  46161  fourierdlem19  46170  fourierdlem20  46171  fourierdlem24  46175  fourierdlem25  46176  fourierdlem26  46177  fourierdlem27  46178  fourierdlem28  46179  fourierdlem31  46182  fourierdlem32  46183  fourierdlem33  46184  fourierdlem35  46186  fourierdlem37  46188  fourierdlem40  46191  fourierdlem41  46192  fourierdlem43  46194  fourierdlem44  46195  fourierdlem46  46196  fourierdlem47  46197  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  fourierdlem51  46201  fourierdlem52  46202  fourierdlem54  46204  fourierdlem57  46207  fourierdlem59  46209  fourierdlem60  46210  fourierdlem61  46211  fourierdlem62  46212  fourierdlem63  46213  fourierdlem64  46214  fourierdlem65  46215  fourierdlem68  46218  fourierdlem69  46219  fourierdlem70  46220  fourierdlem72  46222  fourierdlem73  46223  fourierdlem74  46224  fourierdlem75  46225  fourierdlem76  46226  fourierdlem78  46228  fourierdlem79  46229  fourierdlem81  46231  fourierdlem82  46232  fourierdlem84  46234  fourierdlem89  46239  fourierdlem90  46240  fourierdlem91  46241  fourierdlem92  46242  fourierdlem93  46243  fourierdlem94  46244  fourierdlem97  46247  fourierdlem100  46250  fourierdlem101  46251  fourierdlem102  46252  fourierdlem103  46253  fourierdlem104  46254  fourierdlem107  46257  fourierdlem109  46259  fourierdlem111  46261  fourierdlem112  46262  fourierdlem113  46263  fourierdlem114  46264  sqwvfoura  46272  fouriersw  46275  etransclem23  46301  etransclem46  46324  qndenserrnbllem  46338  rrxsnicc  46344  ioorrnopnlem  46348  ioorrnopnxrlem  46350  salgencntex  46387  sge0cl  46425  sge0fsum  46431  sge0iunmptlemre  46459  sge0isum  46471  sge0ad2en  46475  sge0xaddlem1  46477  sge0xaddlem2  46478  sge0reuz  46491  voliunsge0lem  46516  meassre  46521  omessre  46554  omeiunltfirp  46563  hoissre  46588  hoiprodcl  46591  ovnsubaddlem1  46614  hoiprodcl3  46624  hoidmvcl  46626  hsphoidmvle2  46629  hsphoidmvle  46630  sge0hsphoire  46633  hoidmv1lelem1  46635  hoidmv1lelem2  46636  hoidmv1lelem3  46637  hoidmv1le  46638  hoidmvlelem1  46639  hoidmvlelem2  46640  hoidmvlelem3  46641  hoidmvlelem4  46642  ovnhoilem1  46645  ovnhoilem2  46646  ovnhoi  46647  ovnlecvr2  46654  hspdifhsp  46660  hoidifhspdmvle  46664  hoiqssbllem1  46666  hoiqssbllem2  46667  hoiqssbllem3  46668  hspmbllem1  46670  hspmbllem2  46671  volicorege0  46681  ovolval5lem1  46696  ovolval5lem2  46697  iinhoiicclem  46717  iinhoiicc  46718  iunhoiioolem  46719  iunhoiioo  46720  vonioolem2  46725  vonicclem2  46728  vonsn  46735  pimltmnf2f  46741  pimconstlt0  46745  pimgtpnf2f  46749  salpreimagelt  46751  salpreimalegt  46753  preimageiingt  46764  preimaleiinlt  46765  pimrecltneg  46768  issmflem  46771  issmflelem  46788  issmfgtlem  46799  issmfgt  46800  smfaddlem1  46807  issmfgelem  46813  issmfge  46814  smfpimioompt  46830  smfresal  46832  smfrec  46833  smfmullem1  46835  smfmullem2  46836  smfmullem3  46837  smfmullem4  46838  smfpimbor1lem1  46842  smfsuplem1  46855  smflimsuplem4  46867  smfliminflem  46874  smfdmmblpimne  46881  smfpimne  46883  smfpimne2  46884  fsupdm  46886  finfdm  46890  smfinfdmmbllem  46892  bgoldbtbnd  47846  eenglngeehlnmlem2  48776