Theorem rexrd 10426

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 10271  ℝ^*cxr 10410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399  df-un 3796  df-in 3798  df-ss 3805  df-xr 10415

This theorem is referenced by:  xnn0xr  11719  rpxr  12148  rpxrd  12182  max0sub  12339  qextltlem  12345  xralrple  12348  xnegcl  12356  xaddf  12367  xnn0lenn0nn0  12387  xmulf  12414  xadddi  12437  xrub  12454  supxrre  12469  infxrre  12478  ixxub  12508  ixxlb  12509  ioo0  12512  ico0  12533  ioc0  12534  iooshf  12564  icoshftf1o  12610  supicc  12637  supiccub  12638  supicclub  12639  xnn0xrge0  12642  ssfzunsn  12704  addmodid  13037  hashnnn0genn0  13448  elicc4abs  14466  caucvgrlem  14811  fprodge1  15128  pcxcl  15969  pcdvdsb  15977  pcaddlem  15996  ramcl2lem  16117  ramlb  16127  0ram  16128  setsstruct  16295  prdsxmetlem  22581  xblss2ps  22614  xblss2  22615  blss2ps  22616  blss2  22617  blhalf  22618  metustto  22766  metustexhalf  22769  nmoi  22940  nmoix  22941  nmoi2  22942  nmoleub  22943  qdensere  22981  cnblcld  22986  ioo2blex  23005  tgioo  23007  blcvx  23009  zcld  23024  recld2  23025  iccntr  23032  icccmplem1  23033  reconnlem1  23037  reconnlem2  23038  opnreen  23042  metnrmlem3  23072  icoopnst  23146  cnheibor  23162  lebnumii  23173  nmoleub2lem  23321  lmnn  23469  iscau3  23484  minveclem4  23638  ivthlem1  23655  ivthlem2  23656  ivthlem3  23657  ivth2  23659  ivthle  23660  ivthle2  23661  ivthicc  23662  evthicc  23663  cniccbdd  23665  ovolgelb  23684  ovollb2lem  23692  ovolunlem1  23701  ovoliunlem1  23706  ovoliunlem2  23707  ovoliun  23709  ovolscalem1  23717  ovolicc1  23720  ovolicc2lem4  23724  ovolicc2lem5  23725  ovolicc2  23726  ovolicc  23727  nulmbl2  23740  voliunlem2  23755  ioombl1lem4  23765  ioorcl2  23776  uniioombllem1  23785  uniioombllem2a  23786  uniioombllem3  23789  dyaddisjlem  23799  dyadmaxlem  23801  opnmbllem  23805  volivth  23811  vitalilem4  23815  mbfmulc2lem  23851  mbfmax  23853  mbfposr  23856  ismbf3d  23858  mbfaddlem  23864  mbflimsup  23870  mbfi1fseqlem4  23922  itg2lcl  23931  xrge0f  23935  itg2itg1  23940  itg2const2  23945  itg2seq  23946  itg2uba  23947  itg2lea  23948  itg2mulclem  23950  itg2mulc  23951  itg2splitlem  23952  itg2split  23953  itg2monolem2  23955  itg2monolem3  23956  itg2mono  23957  itg2gt0  23964  itg2cnlem1  23965  itg2cnlem2  23966  itg2cn  23967  iblss  24008  itgle  24013  itgeqa  24017  itgioo  24019  ibladdlem  24023  iblabs  24032  iblabsr  24033  iblmulc2  24034  itgsplit  24039  itgspliticc  24040  itgsplitioo  24041  bddmulibl  24042  ditgcl  24059  ditgswap  24060  ditgsplitlem  24061  dvferm1lem  24184  dvferm2lem  24186  dvferm  24188  rollelem  24189  rolle  24190  cmvth  24191  mvth  24192  dvlip  24193  dvlip2  24195  c1liplem1  24196  c1lip1  24197  dveq0  24200  dvgt0lem1  24202  dvivthlem1  24208  dvivth  24210  lhop1lem  24213  lhop1  24214  lhop2  24215  lhop  24216  dvcnvrelem1  24217  dvcnvre  24219  dvcvx  24220  dvfsumle  24221  dvfsumge  24222  dvfsumabs  24223  dvfsumlem2  24227  dvfsumlem3  24228  dvfsumlem4  24229  dvfsumrlimge0  24230  dvfsumrlim2  24232  ftc1lem1  24235  ftc1lem2  24236  ftc1a  24237  ftc1lem4  24239  ftc2  24244  ftc2ditglem  24245  itgparts  24247  itgsubstlem  24248  itgsubst  24249  degltlem1  24269  deg1ge  24295  coe1mul3  24296  deg1sublt  24307  deg1mul2  24311  deg1tmle  24314  deg1tm  24315  plypf1  24405  taylfvallem1  24548  tayl0  24553  pserulm  24613  psercnlem1  24616  pserdvlem1  24618  pserdvlem2  24619  abelthlem3  24624  abelth  24632  efcvx  24640  logno1  24819  logtayl  24843  xrlimcnp  25147  logfacbnd3  25400  log2sumbnd  25685  pntpbnd2  25728  pntibndlem3  25733  ttgcontlem1  26234  nmooge0  28194  nmoub3i  28200  isblo3i  28228  ubthlem1  28298  minvecolem4  28308  nmopge0  29342  nmfnge0  29358  nmophmi  29462  branmfn  29536  xaddeq0  30083  xlt2addrd  30088  xmulcand  30191  xreceu  30192  xdivrec  30197  fsumrp0cl  30257  xrge0slmod  30406  cnre2csqlem  30554  tpr2rico  30556  xrge0iifcnv  30577  xrge0iifhom  30581  lmxrge0  30596  esumfsup  30730  esumpcvgval  30738  esumcvg  30746  dya2iocress  30934  dya2iocbrsiga  30935  dya2icobrsiga  30936  dya2icoseg  30937  dya2iocucvr  30944  sxbrsigalem2  30946  omssubaddlem  30959  omssubadd  30960  orvcgteel  31128  dstrvprob  31132  orvclteel  31133  sgnmul  31203  sgnsub  31205  sgnmulsgn  31210  sgnmulsgp  31211  signstcl  31242  signstf  31243  signstf0  31245  signstfvn  31246  signsvtn0  31247  signsvtn0OLD  31248  signstfvneq0  31250  signsvfn  31261  signsvfpn  31264  signsvfnn  31265  ftc2re  31278  cvmliftlem6  31871  cvmliftlem7  31872  cvmliftlem8  31873  cvmliftlem9  31874  cvmliftlem10  31875  cvmliftlem13  31877  ivthALT  32918  iooelexlt  33805  relowlssretop  33806  relowlpssretop  33807  sin2h  34008  cos2h  34009  tan2h  34010  poimirlem30  34049  poimir  34052  heicant  34054  opnmbllem0  34055  mblfinlem1  34056  mblfinlem2  34057  mblfinlem3  34058  mblfinlem4  34059  ismblfin  34060  itg2addnclem  34070  itg2addnclem2  34071  itg2gt0cn  34074  ibladdnclem  34075  iblabsnclem  34082  iblabsnc  34083  iblmulc2nc  34084  bddiblnc  34089  ftc1cnnclem  34092  ftc1anclem1  34094  ftc1anclem4  34097  ftc1anclem5  34098  ftc1anclem6  34099  ftc1anclem7  34100  ftc1anclem8  34101  ftc1anc  34102  ftc2nc  34103  areacirclem1  34109  areacirclem5  34113  areacirc  34114  isbnd3  34191  blbnd  34194  prdsbnd  34200  prdsbnd2  34202  cntotbnd  34203  idomrootle  38714  idomodle  38715  itgpowd  38740  imo72b2  39413  cvgdvgrat  39450  radcnvrat  39451  rfcnpre3  40107  rfcnpre4  40108  nnxrd  40116  absfico  40313  lefldiveq  40397  lttri5d  40404  supxrgere  40439  supxrgelem  40443  supxrge  40444  xralrple2  40460  infxr  40473  infleinflem1  40476  infleinflem2  40477  xralrple4  40479  xralrple3  40480  xrralrecnnle  40492  xrralrecnnge  40501  supxrunb3  40511  unb2ltle  40530  zxrd  40570  gtnelioc  40606  ltnelicc  40613  iooabslt  40615  gtnelicc  40616  eliooshift  40623  iocopn  40637  eliccelioc  40638  iooshift  40639  icoopn  40642  ge0lere  40649  iooiinicc  40659  sqrlearg  40670  iooiinioc  40673  uzinico  40677  preimaiocmnf  40678  uzubioo  40684  fsumge0cl  40695  limciccioolb  40743  lptioo1  40754  limcicciooub  40759  ltmod  40760  lptre2pt  40762  limsupre  40763  limcresiooub  40764  limcresioolb  40765  limcleqr  40766  limsupresico  40822  limsuppnfdlem  40823  limsupub  40826  limsupequzlem  40844  limsupre2lem  40846  limsupre3lem  40854  limsupvaluz2  40860  supcnvlimsup  40862  liminfresico  40893  limsup10exlem  40894  liminflelimsuplem  40897  limsupgtlem  40899  liminfval4  40911  liminfvaluz2  40917  limsupvaluz4  40922  liminflimsupclim  40929  xlimxrre  40953  xlimmnfvlem1  40954  xlimmnfv  40956  xlimpnfvlem1  40958  xlimpnfv  40960  sinaover2ne0  40989  ioccncflimc  41008  icccncfext  41010  icocncflimc  41012  cncfiooicclem1  41016  cncfiooicc  41017  cncfiooiccre  41018  cncfioobdlem  41019  dvbdfbdioolem1  41053  dvbdfbdioolem2  41054  dvbdfbdioo  41055  ioodvbdlimc1lem1  41056  ioodvbdlimc1lem2  41057  ioodvbdlimc1  41058  ioodvbdlimc2lem  41059  ioodvbdlimc2  41060  ditgeqiooicc  41085  iblsplit  41091  itgcoscmulx  41094  ibliooicc  41096  iblspltprt  41098  itgsincmulx  41099  itgsubsticc  41101  itgioocnicc  41102  iblcncfioo  41103  itgspltprt  41104  itgiccshift  41105  volioore  41116  voliooico  41118  voliooicof  41122  voliccico  41125  stoweidlem34  41160  stoweidlem52  41178  stirlinglem5  41204  dirkercncflem1  41229  dirkercncflem4  41232  fourierdlem4  41237  fourierdlem10  41243  fourierdlem19  41252  fourierdlem20  41253  fourierdlem24  41257  fourierdlem25  41258  fourierdlem26  41259  fourierdlem27  41260  fourierdlem28  41261  fourierdlem31  41264  fourierdlem32  41265  fourierdlem33  41266  fourierdlem35  41268  fourierdlem37  41270  fourierdlem40  41273  fourierdlem41  41274  fourierdlem43  41276  fourierdlem44  41277  fourierdlem46  41278  fourierdlem47  41279  fourierdlem48  41280  fourierdlem49  41281  fourierdlem50  41282  fourierdlem51  41283  fourierdlem52  41284  fourierdlem54  41286  fourierdlem57  41289  fourierdlem59  41291  fourierdlem60  41292  fourierdlem61  41293  fourierdlem62  41294  fourierdlem63  41295  fourierdlem64  41296  fourierdlem65  41297  fourierdlem68  41300  fourierdlem69  41301  fourierdlem70  41302  fourierdlem72  41304  fourierdlem73  41305  fourierdlem74  41306  fourierdlem75  41307  fourierdlem76  41308  fourierdlem78  41310  fourierdlem79  41311  fourierdlem81  41313  fourierdlem82  41314  fourierdlem84  41316  fourierdlem89  41321  fourierdlem90  41322  fourierdlem91  41323  fourierdlem92  41324  fourierdlem93  41325  fourierdlem94  41326  fourierdlem97  41329  fourierdlem100  41332  fourierdlem101  41333  fourierdlem102  41334  fourierdlem103  41335  fourierdlem104  41336  fourierdlem107  41339  fourierdlem109  41341  fourierdlem111  41343  fourierdlem112  41344  fourierdlem113  41345  fourierdlem114  41346  sqwvfoura  41354  fouriersw  41357  etransclem23  41383  etransclem46  41406  qndenserrnbllem  41420  rrxsnicc  41426  ioorrnopnlem  41430  ioorrnopnxrlem  41432  salgencntex  41467  sge0cl  41504  sge0fsum  41510  sge0iunmptlemre  41538  sge0isum  41550  sge0ad2en  41554  sge0xaddlem1  41556  sge0xaddlem2  41557  sge0reuz  41570  voliunsge0lem  41595  meassre  41600  omessre  41633  omeiunltfirp  41642  hoissre  41667  hoiprodcl  41670  ovnsubaddlem1  41693  hoiprodcl3  41703  hoidmvcl  41705  hsphoidmvle2  41708  hsphoidmvle  41709  sge0hsphoire  41712  hoidmv1lelem1  41714  hoidmv1lelem2  41715  hoidmv1lelem3  41716  hoidmv1le  41717  hoidmvlelem1  41718  hoidmvlelem2  41719  hoidmvlelem3  41720  hoidmvlelem4  41721  ovnhoilem1  41724  ovnhoilem2  41725  ovnhoi  41726  ovnlecvr2  41733  hspdifhsp  41739  hoidifhspdmvle  41743  hoiqssbllem1  41745  hoiqssbllem2  41746  hoiqssbllem3  41747  hspmbllem1  41749  hspmbllem2  41750  volicorege0  41760  ovolval5lem1  41775  ovolval5lem2  41776  iinhoiicclem  41796  iinhoiicc  41797  iunhoiioolem  41798  iunhoiioo  41799  vonioolem2  41804  vonicclem2  41807  vonsn  41814  pimltmnf2  41820  pimconstlt0  41823  pimgtpnf2  41826  salpreimagelt  41827  salpreimalegt  41829  preimageiingt  41839  preimaleiinlt  41840  pimrecltneg  41842  issmflem  41845  issmflelem  41862  issmfgtlem  41873  issmfgt  41874  smfaddlem1  41880  issmfgelem  41886  issmfge  41887  smfpimioompt  41902  smfresal  41904  smfrec  41905  smfmullem1  41907  smfmullem2  41908  smfmullem3  41909  smfmullem4  41910  smfpimbor1lem1  41914  smfsuplem1  41926  smflimsuplem4  41938  smfliminflem  41945  bgoldbtbnd  42704  eenglngeehlnmlem2  43456