Theorem rexrd 11224

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℝ^*cxr 11207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-xr 11212

This theorem is referenced by:  xnn0xr  12520  rpxr  12961  rpxrd  12996  max0sub  13156  qextltlem  13162  xralrple  13165  xnegcl  13173  xaddf  13184  xnn0lem1lt  13204  xnn0lenn0nn0  13205  xmulf  13232  xadddi  13255  xrub  13272  supxrre  13287  infxrre  13297  ixxub  13327  ixxlb  13328  ioo0  13331  ico0  13352  ioc0  13353  iooshf  13387  icoshftf1o  13435  supicc  13462  supiccub  13463  supicclub  13464  xnn0xrge0  13467  ssfzunsn  13531  addmodid  13884  hashnnn0genn0  14308  hashunsnggt  14359  elicc4abs  15286  caucvgrlem  15639  fprodge1  15961  pcxcl  16832  pcdvdsb  16840  pcaddlem  16859  ramcl2lem  16980  ramlb  16990  0ram  16991  setsstruct  17146  prdsxmetlem  24256  xblss2ps  24289  xblss2  24290  blss2ps  24291  blss2  24292  blhalf  24293  metustto  24441  metustexhalf  24444  nmoi  24616  nmoix  24617  nmoi2  24618  nmoleub  24619  qdensere  24657  cnblcld  24662  ioo2blex  24682  tgioo  24684  blcvx  24686  zcld  24702  recld2  24703  iccntr  24710  icccmplem1  24711  reconnlem1  24715  reconnlem2  24716  opnreen  24720  metnrmlem3  24750  icoopnst  24836  iocopnst  24837  cnheibor  24854  lebnumii  24865  nmoleub2lem  25014  lmnn  25163  iscau3  25178  minveclem4  25332  ivthlem1  25352  ivthlem2  25353  ivthlem3  25354  ivth2  25356  ivthle  25357  ivthle2  25358  ivthicc  25359  evthicc  25360  cniccbdd  25362  ovolgelb  25381  ovollb2lem  25389  ovolunlem1  25398  ovoliunlem1  25403  ovoliunlem2  25404  ovoliun  25406  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem4  25421  ovolicc2lem5  25422  ovolicc2  25423  ovolicc  25424  nulmbl2  25437  voliunlem2  25452  ioombl1lem4  25462  ioorcl2  25473  uniioombllem1  25482  uniioombllem2a  25483  uniioombllem3  25486  dyaddisjlem  25496  dyadmaxlem  25498  opnmbllem  25502  volivth  25508  vitalilem4  25512  mbfmulc2lem  25548  mbfmax  25550  mbfposr  25553  ismbf3d  25555  mbfaddlem  25561  mbflimsup  25567  mbfi1fseqlem4  25619  itg2lcl  25628  xrge0f  25632  itg2itg1  25637  itg2const2  25642  itg2seq  25643  itg2uba  25644  itg2lea  25645  itg2mulclem  25647  itg2mulc  25648  itg2splitlem  25649  itg2split  25650  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  itg2cn  25664  iblss  25706  itgle  25711  itgeqa  25715  itgioo  25717  ibladdlem  25721  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgsplit  25737  itgspliticc  25738  itgsplitioo  25739  bddmulibl  25740  bddiblnc  25743  ditgcl  25759  ditgswap  25760  ditgsplitlem  25761  dvferm1lem  25888  dvferm2lem  25890  dvferm  25892  rollelem  25893  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvlip2  25900  c1liplem1  25901  c1lip1  25902  dveq0  25905  dvgt0lem1  25907  dvivthlem1  25913  dvivth  25915  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  dvcnvrelem1  25922  dvcnvre  25924  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlimge0  25937  dvfsumrlim2  25939  ftc1lem1  25942  ftc1lem2  25943  ftc1a  25944  ftc1lem4  25946  ftc2  25951  ftc2ditglem  25952  itgparts  25954  itgsubstlem  25955  itgsubst  25956  itgpowd  25957  degltlem1  25977  deg1ge  26003  coe1mul3  26004  deg1sublt  26015  deg1mul2  26019  deg1tmle  26023  deg1tm  26024  idomrootle  26078  plypf1  26117  taylfvallem1  26264  tayl0  26269  pserulm  26331  psercnlem1  26335  pserdvlem1  26337  pserdvlem2  26338  abelthlem3  26343  abelth  26351  efcvx  26359  logno1  26545  logtayl  26569  xrlimcnp  26878  logfacbnd3  27134  log2sumbnd  27455  pntpbnd2  27498  pntibndlem3  27503  ttgcontlem1  28812  nmooge0  30696  nmoub3i  30702  isblo3i  30730  ubthlem1  30799  minvecolem4  30809  nmopge0  31840  nmfnge0  31856  nmophmi  31960  branmfn  32034  sgnval2  32658  xaddeq0  32676  xlt2addrd  32682  sgnmul  32760  sgnsub  32762  sgnmulsgn  32767  sgnmulsgp  32768  xmulcand  32841  xreceu  32842  xdivrec  32847  fsumrp0cl  32962  xrge0slmod  33319  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  ply1degltdimlem  33618  ply1degltdim  33619  fldextrspundgdvdslem  33675  cos9thpiminplylem2  33773  cnre2csqlem  33900  tpr2rico  33902  xrge0iifcnv  33923  xrge0iifhom  33927  lmxrge0  33942  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  dya2iocress  34265  dya2iocbrsiga  34266  dya2icobrsiga  34267  dya2icoseg  34268  dya2iocucvr  34275  sxbrsigalem2  34277  omssubaddlem  34290  omssubadd  34291  orvcgteel  34459  dstrvprob  34463  orvclteel  34464  signstcl  34556  signstf  34557  signstf0  34559  signstfvn  34560  signsvtn0  34561  signsvfn  34573  signsvfpn  34576  signsvfnn  34577  ftc2re  34589  cvmliftlem6  35277  cvmliftlem7  35278  cvmliftlem8  35279  cvmliftlem9  35280  cvmliftlem10  35281  cvmliftlem13  35283  ivthALT  36323  iooelexlt  37350  relowlssretop  37351  relowlpssretop  37352  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem30  37644  poimir  37647  heicant  37649  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem  37665  itg2addnclem2  37666  itg2gt0cn  37669  ibladdnclem  37670  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  ftc1cnnclem  37685  ftc1anclem1  37687  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  ftc2nc  37696  areacirclem1  37702  areacirclem5  37706  areacirc  37707  isbnd3  37778  blbnd  37781  prdsbnd  37787  prdsbnd2  37789  cntotbnd  37790  dvrelog3  42053  0nonelalab  42055  dvrelogpow2b  42056  dvle2  42060  aks4d1p1p6  42061  aks4d1p1p5  42063  aks6d1c6lem3  42160  aks6d1c7lem2  42169  unitscyglem5  42187  idomodle  43180  imo72b2  44161  cvgdvgrat  44302  radcnvrat  44303  rfcnpre3  45027  rfcnpre4  45028  absfico  45212  nnxrd  45272  lefldiveq  45290  lttri5d  45297  supxrgere  45329  supxrgelem  45333  supxrge  45334  xralrple2  45350  infxr  45363  infleinflem1  45366  infleinflem2  45367  xralrple4  45369  xralrple3  45370  xrralrecnnle  45379  xrralrecnnge  45386  supxrunb3  45395  unb2ltle  45411  zxrd  45449  gtnelioc  45489  ltnelicc  45495  iooabslt  45497  gtnelicc  45498  eliooshift  45504  iocopn  45518  eliccelioc  45519  iooshift  45520  icoopn  45523  ge0lere  45530  iooiinicc  45540  sqrlearg  45551  iooiinioc  45554  uzinico  45557  preimaiocmnf  45558  uzubioo  45563  fsumge0cl  45571  limciccioolb  45619  lptioo1  45630  limcicciooub  45635  ltmod  45636  lptre2pt  45638  limsupre  45639  limcresiooub  45640  limcresioolb  45641  limcleqr  45642  limsupresico  45698  limsuppnfdlem  45699  limsupub  45702  limsupequzlem  45720  limsupre2lem  45722  limsupre3lem  45730  limsupvaluz2  45736  supcnvlimsup  45738  liminfresico  45769  limsup10exlem  45770  liminflelimsuplem  45773  limsupgtlem  45775  liminfval4  45787  liminfvaluz2  45793  limsupvaluz4  45798  liminflimsupclim  45805  xlimxrre  45829  xlimmnfvlem1  45830  xlimmnfv  45832  xlimpnfvlem1  45834  xlimpnfv  45836  sinaover2ne0  45866  ioccncflimc  45883  icccncfext  45885  icocncflimc  45887  cncfiooicclem1  45891  cncfiooicc  45892  cncfiooiccre  45893  cncfioobdlem  45894  dvbdfbdioolem1  45926  dvbdfbdioolem2  45927  dvbdfbdioo  45928  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc1  45931  ioodvbdlimc2lem  45932  ioodvbdlimc2  45933  ditgeqiooicc  45958  iblsplit  45964  itgcoscmulx  45967  ibliooicc  45969  iblspltprt  45971  itgsincmulx  45972  itgsubsticc  45974  itgioocnicc  45975  iblcncfioo  45976  itgspltprt  45977  itgiccshift  45978  volioore  45988  voliooico  45990  voliooicof  45994  voliccico  45997  stoweidlem34  46032  stoweidlem52  46050  stirlinglem5  46076  dirkercncflem1  46101  dirkercncflem4  46104  fourierdlem4  46109  fourierdlem10  46115  fourierdlem19  46124  fourierdlem20  46125  fourierdlem24  46129  fourierdlem25  46130  fourierdlem26  46131  fourierdlem27  46132  fourierdlem28  46133  fourierdlem31  46136  fourierdlem32  46137  fourierdlem33  46138  fourierdlem35  46140  fourierdlem37  46142  fourierdlem40  46145  fourierdlem41  46146  fourierdlem43  46148  fourierdlem44  46149  fourierdlem46  46150  fourierdlem47  46151  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem52  46156  fourierdlem54  46158  fourierdlem57  46161  fourierdlem59  46163  fourierdlem60  46164  fourierdlem61  46165  fourierdlem62  46166  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem68  46172  fourierdlem69  46173  fourierdlem70  46174  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem84  46188  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem93  46197  fourierdlem94  46198  fourierdlem97  46201  fourierdlem100  46204  fourierdlem101  46205  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem109  46213  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fourierdlem114  46218  sqwvfoura  46226  fouriersw  46229  etransclem23  46255  etransclem46  46278  qndenserrnbllem  46292  rrxsnicc  46298  ioorrnopnlem  46302  ioorrnopnxrlem  46304  salgencntex  46341  sge0cl  46379  sge0fsum  46385  sge0iunmptlemre  46413  sge0isum  46425  sge0ad2en  46429  sge0xaddlem1  46431  sge0xaddlem2  46432  sge0reuz  46445  voliunsge0lem  46470  meassre  46475  omessre  46508  omeiunltfirp  46517  hoissre  46542  hoiprodcl  46545  ovnsubaddlem1  46568  hoiprodcl3  46578  hoidmvcl  46580  hsphoidmvle2  46583  hsphoidmvle  46584  sge0hsphoire  46587  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  ovnhoilem1  46599  ovnhoilem2  46600  ovnhoi  46601  ovnlecvr2  46608  hspdifhsp  46614  hoidifhspdmvle  46618  hoiqssbllem1  46620  hoiqssbllem2  46621  hoiqssbllem3  46622  hspmbllem1  46624  hspmbllem2  46625  volicorege0  46635  ovolval5lem1  46650  ovolval5lem2  46651  iinhoiicclem  46671  iinhoiicc  46672  iunhoiioolem  46673  iunhoiioo  46674  vonioolem2  46679  vonicclem2  46682  vonsn  46689  pimltmnf2f  46695  pimconstlt0  46699  pimgtpnf2f  46703  salpreimagelt  46705  salpreimalegt  46707  preimageiingt  46718  preimaleiinlt  46719  pimrecltneg  46722  issmflem  46725  issmflelem  46742  issmfgtlem  46753  issmfgt  46754  smfaddlem1  46761  issmfgelem  46767  issmfge  46768  smfpimioompt  46784  smfresal  46786  smfrec  46787  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  smfmullem4  46792  smfpimbor1lem1  46796  smfsuplem1  46809  smflimsuplem4  46821  smfliminflem  46828  smfdmmblpimne  46835  smfpimne  46837  smfpimne2  46838  fsupdm  46840  finfdm  46844  smfinfdmmbllem  46846  bgoldbtbnd  47810  eenglngeehlnmlem2  48727