Theorem rexrd 11193

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-xr 11181

This theorem is referenced by:  xnn0xr  12513  rpxr  12950  rpxrd  12985  max0sub  13146  qextltlem  13152  xralrple  13155  xnegcl  13163  xaddf  13174  xnn0lem1lt  13194  xnn0lenn0nn0  13195  xmulf  13222  xadddi  13245  xrub  13262  supxrre  13277  infxrre  13287  ixxub  13317  ixxlb  13318  ioo0  13321  ico0  13342  ioc0  13343  iooshf  13377  icoshftf1o  13425  supicc  13452  supiccub  13453  supicclub  13454  xnn0xrge0  13457  ssfzunsn  13522  addmodid  13879  hashnnn0genn0  14303  hashunsnggt  14354  elicc4abs  15280  caucvgrlem  15633  fprodge1  15958  pcxcl  16830  pcdvdsb  16838  pcaddlem  16857  ramcl2lem  16978  ramlb  16988  0ram  16989  setsstruct  17144  prdsxmetlem  24358  xblss2ps  24391  xblss2  24392  blss2ps  24393  blss2  24394  blhalf  24395  metustto  24543  metustexhalf  24546  nmoi  24718  nmoix  24719  nmoi2  24720  nmoleub  24721  qdensere  24759  cnblcld  24764  ioo2blex  24784  tgioo  24786  blcvx  24788  zcld  24804  recld2  24805  iccntr  24812  icccmplem1  24813  reconnlem1  24817  reconnlem2  24818  opnreen  24822  metnrmlem3  24852  icoopnst  24931  iocopnst  24932  cnheibor  24947  lebnumii  24958  nmoleub2lem  25106  lmnn  25255  iscau3  25270  minveclem4  25424  ivthlem1  25443  ivthlem2  25444  ivthlem3  25445  ivth2  25447  ivthle  25448  ivthle2  25449  ivthicc  25450  evthicc  25451  cniccbdd  25453  ovolgelb  25472  ovollb2lem  25480  ovolunlem1  25489  ovoliunlem1  25494  ovoliunlem2  25495  ovoliun  25497  ovolscalem1  25505  ovolicc1  25508  ovolicc2lem4  25512  ovolicc2lem5  25513  ovolicc2  25514  ovolicc  25515  nulmbl2  25528  voliunlem2  25543  ioombl1lem4  25553  ioorcl2  25564  uniioombllem1  25573  uniioombllem2a  25574  uniioombllem3  25577  dyaddisjlem  25587  dyadmaxlem  25589  opnmbllem  25593  volivth  25599  vitalilem4  25603  mbfmulc2lem  25639  mbfmax  25641  mbfposr  25644  ismbf3d  25646  mbfaddlem  25652  mbflimsup  25658  mbfi1fseqlem4  25710  itg2lcl  25719  xrge0f  25723  itg2itg1  25728  itg2const2  25733  itg2seq  25734  itg2uba  25735  itg2lea  25736  itg2mulclem  25738  itg2mulc  25739  itg2splitlem  25740  itg2split  25741  itg2monolem2  25743  itg2monolem3  25744  itg2mono  25745  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  itg2cn  25755  iblss  25797  itgle  25802  itgeqa  25806  itgioo  25808  ibladdlem  25812  iblabs  25821  iblabsr  25822  iblmulc2  25823  itgsplit  25828  itgspliticc  25829  itgsplitioo  25830  bddmulibl  25831  bddiblnc  25834  ditgcl  25850  ditgswap  25851  ditgsplitlem  25852  dvferm1lem  25976  dvferm2lem  25978  dvferm  25980  rollelem  25981  rolle  25982  cmvth  25983  mvth  25984  dvlip  25985  dvlip2  25987  c1liplem1  25988  c1lip1  25989  dveq0  25992  dvgt0lem1  25994  dvivthlem1  26000  dvivth  26002  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  dvcnvrelem1  26009  dvcnvre  26011  dvcvx  26012  dvfsumle  26013  dvfsumge  26014  dvfsumabs  26015  dvfsumlem2  26019  dvfsumlem3  26020  dvfsumlem4  26021  dvfsumrlimge0  26022  dvfsumrlim2  26024  ftc1lem1  26027  ftc1lem2  26028  ftc1a  26029  ftc1lem4  26031  ftc2  26036  ftc2ditglem  26037  itgparts  26039  itgsubstlem  26040  itgsubst  26041  itgpowd  26042  degltlem1  26062  deg1ge  26088  coe1mul3  26089  deg1sublt  26100  deg1mul2  26104  deg1tmle  26108  deg1tm  26109  idomrootle  26163  plypf1  26202  taylfvallem1  26347  tayl0  26352  pserulm  26412  psercnlem1  26415  pserdvlem1  26417  pserdvlem2  26418  abelthlem3  26423  abelth  26431  efcvx  26439  logno1  26625  logtayl  26649  xrlimcnp  26957  logfacbnd3  27211  log2sumbnd  27532  pntpbnd2  27575  pntibndlem3  27580  ttgcontlem1  28978  nmooge0  30863  nmoub3i  30869  isblo3i  30897  ubthlem1  30966  minvecolem4  30976  nmopge0  32007  nmfnge0  32023  nmophmi  32127  branmfn  32201  sgnval2  32834  nn0mnfxrd  32850  xaddeq0  32852  xlt2addrd  32858  sgnmul  32934  sgnsub  32936  sgnmulsgn  32941  sgnmulsgp  32942  xmulcand  33006  xreceu  33007  xdivrec  33012  fsumrp0cl  33107  xrge0slmod  33438  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  ply1degltdimlem  33813  ply1degltdim  33814  fldextrspundgdvdslem  33871  extdgfialglem1  33883  cos9thpiminplylem2  33974  cnre2csqlem  34101  tpr2rico  34103  xrge0iifcnv  34124  xrge0iifhom  34128  lmxrge0  34143  esumfsup  34261  esumpcvgval  34269  esumcvg  34277  dya2iocress  34465  dya2iocbrsiga  34466  dya2icobrsiga  34467  dya2icoseg  34468  dya2iocucvr  34475  sxbrsigalem2  34477  omssubaddlem  34490  omssubadd  34491  orvcgteel  34659  dstrvprob  34663  orvclteel  34664  signstcl  34756  signstf  34757  signstf0  34759  signstfvn  34760  signsvtn0  34761  signsvfn  34773  signsvfpn  34776  signsvfnn  34777  ftc2re  34789  cvmliftlem6  35525  cvmliftlem7  35526  cvmliftlem8  35527  cvmliftlem9  35528  cvmliftlem10  35529  cvmliftlem13  35531  ivthALT  36570  iooelexlt  37731  relowlssretop  37732  relowlpssretop  37733  sin2h  37984  cos2h  37985  tan2h  37986  poimirlem30  38024  poimir  38027  heicant  38029  opnmbllem0  38030  mblfinlem1  38031  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  itg2addnclem  38045  itg2addnclem2  38046  itg2gt0cn  38049  ibladdnclem  38050  iblabsnclem  38057  iblabsnc  38058  iblmulc2nc  38059  ftc1cnnclem  38065  ftc1anclem1  38067  ftc1anclem4  38070  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  ftc2nc  38076  areacirclem1  38082  areacirclem5  38086  areacirc  38087  isbnd3  38158  blbnd  38161  prdsbnd  38167  prdsbnd2  38169  cntotbnd  38170  dvrelog3  42557  0nonelalab  42559  dvrelogpow2b  42560  dvle2  42564  aks4d1p1p6  42565  aks4d1p1p5  42567  aks6d1c6lem3  42664  aks6d1c7lem2  42673  unitscyglem5  42691  idomodle  43643  imo72b2  44623  cvgdvgrat  44764  radcnvrat  44765  rfcnpre3  45488  rfcnpre4  45489  absfico  45670  nnxrd  45729  lefldiveq  45747  lttri5d  45754  supxrgere  45785  supxrgelem  45789  supxrge  45790  xralrple2  45806  infxr  45818  infleinflem1  45821  infleinflem2  45822  xralrple4  45824  xralrple3  45825  xrralrecnnle  45834  xrralrecnnge  45841  supxrunb3  45850  unb2ltle  45865  zxrd  45903  gtnelioc  45943  ltnelicc  45949  iooabslt  45951  gtnelicc  45952  eliooshift  45958  iocopn  45972  eliccelioc  45973  iooshift  45974  icoopn  45977  ge0lere  45984  iooiinicc  45994  sqrlearg  46005  iooiinioc  46008  uzinico  46011  preimaiocmnf  46012  uzubioo  46017  fsumge0cl  46025  limciccioolb  46073  lptioo1  46084  limcicciooub  46087  ltmod  46088  lptre2pt  46090  limsupre  46091  limcresiooub  46092  limcresioolb  46093  limcleqr  46094  limsupresico  46150  limsuppnfdlem  46151  limsupub  46154  limsupequzlem  46172  limsupre2lem  46174  limsupre3lem  46182  limsupvaluz2  46188  supcnvlimsup  46190  liminfresico  46221  limsup10exlem  46222  liminflelimsuplem  46225  limsupgtlem  46227  liminfval4  46239  liminfvaluz2  46245  limsupvaluz4  46250  liminflimsupclim  46257  xlimxrre  46281  xlimmnfvlem1  46282  xlimmnfv  46284  xlimpnfvlem1  46286  xlimpnfv  46288  sinaover2ne0  46318  ioccncflimc  46335  icccncfext  46337  icocncflimc  46339  cncfiooicclem1  46343  cncfiooicc  46344  cncfiooiccre  46345  cncfioobdlem  46346  dvbdfbdioolem1  46378  dvbdfbdioolem2  46379  dvbdfbdioo  46380  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc1  46383  ioodvbdlimc2lem  46384  ioodvbdlimc2  46385  ditgeqiooicc  46410  iblsplit  46416  itgcoscmulx  46419  ibliooicc  46421  iblspltprt  46423  itgsincmulx  46424  itgsubsticc  46426  itgioocnicc  46427  iblcncfioo  46428  itgspltprt  46429  itgiccshift  46430  volioore  46440  voliooico  46442  voliooicof  46446  voliccico  46449  stoweidlem34  46484  stoweidlem52  46502  stirlinglem5  46528  dirkercncflem1  46553  dirkercncflem4  46556  fourierdlem4  46561  fourierdlem10  46567  fourierdlem19  46576  fourierdlem20  46577  fourierdlem24  46581  fourierdlem25  46582  fourierdlem26  46583  fourierdlem27  46584  fourierdlem28  46585  fourierdlem31  46588  fourierdlem32  46589  fourierdlem33  46590  fourierdlem35  46592  fourierdlem37  46594  fourierdlem40  46597  fourierdlem41  46598  fourierdlem43  46600  fourierdlem44  46601  fourierdlem46  46602  fourierdlem47  46603  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem51  46607  fourierdlem52  46608  fourierdlem54  46610  fourierdlem57  46613  fourierdlem59  46615  fourierdlem60  46616  fourierdlem61  46617  fourierdlem62  46618  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem68  46624  fourierdlem69  46625  fourierdlem70  46626  fourierdlem72  46628  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem78  46634  fourierdlem79  46635  fourierdlem81  46637  fourierdlem82  46638  fourierdlem84  46640  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem93  46649  fourierdlem94  46650  fourierdlem97  46653  fourierdlem100  46656  fourierdlem101  46657  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem107  46663  fourierdlem109  46665  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  fourierdlem114  46670  sqwvfoura  46678  fouriersw  46681  etransclem23  46707  etransclem46  46730  qndenserrnbllem  46744  rrxsnicc  46750  ioorrnopnlem  46754  ioorrnopnxrlem  46756  salgencntex  46793  sge0cl  46831  sge0fsum  46837  sge0iunmptlemre  46865  sge0isum  46877  sge0ad2en  46881  sge0xaddlem1  46883  sge0xaddlem2  46884  sge0reuz  46897  voliunsge0lem  46922  meassre  46927  omessre  46960  omeiunltfirp  46969  hoissre  46994  hoiprodcl  46997  ovnsubaddlem1  47020  hoiprodcl3  47030  hoidmvcl  47032  hsphoidmvle2  47035  hsphoidmvle  47036  sge0hsphoire  47039  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1lelem3  47043  hoidmv1le  47044  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  ovnhoilem1  47051  ovnhoilem2  47052  ovnhoi  47053  ovnlecvr2  47060  hspdifhsp  47066  hoidifhspdmvle  47070  hoiqssbllem1  47072  hoiqssbllem2  47073  hoiqssbllem3  47074  hspmbllem1  47076  hspmbllem2  47077  volicorege0  47087  ovolval5lem1  47102  ovolval5lem2  47103  iinhoiicclem  47123  iinhoiicc  47124  iunhoiioolem  47125  iunhoiioo  47126  vonioolem2  47131  vonicclem2  47134  vonsn  47141  pimltmnf2f  47147  pimconstlt0  47151  pimgtpnf2f  47155  salpreimagelt  47157  salpreimalegt  47159  preimageiingt  47170  preimaleiinlt  47171  pimrecltneg  47174  issmflem  47177  issmflelem  47194  issmfgtlem  47205  issmfgt  47206  smfaddlem1  47213  issmfgelem  47219  issmfge  47220  smfpimioompt  47236  smfresal  47238  smfrec  47239  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243  smfmullem4  47244  smfpimbor1lem1  47248  smfsuplem1  47261  smflimsuplem4  47273  smfliminflem  47280  smfdmmblpimne  47287  smfpimne  47289  smfpimne2  47290  fsupdm  47292  finfdm  47296  smfinfdmmbllem  47298  bgoldbtbnd  48307  eenglngeehlnmlem2  49236