Theorem rexrd 9664

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 9658	. 2
2		rexrd.1	. 2
3	1, 2	sseldi 3501	1

Syntax hints:  ->wi 4  e.wcel 1818  cr 9512  cxr 9648

This theorem is referenced by:  rpxr  11256  rpxrd  11286  max0sub  11424  qextltlem  11430  xralrple  11433  xnegcl  11441  xaddf  11452  xmulf  11493  xadddi  11516  supxrre  11548  infmxrre  11556  ixxub  11579  ixxlb  11580  ioo0  11583  ico0  11604  ioc0  11605  iooshf  11632  icoshftf1o  11672  supicc  11697  supiccub  11698  supicclub  11699  hashnnn0genn0  12416  elicc4abs  13152  caucvgrlem  13495  pcxcl  14384  pcdvdsb  14392  pcaddlem  14407  ramcl2lem  14527  ramlb  14537  0ram  14538  prdsxmetlem  20871  xblss2ps  20904  xblss2  20905  blss2ps  20906  blss2  20907  blhalf  20908  metusttoOLD  21060  metustto  21061  metustexhalfOLD  21066  metustexhalf  21067  nmoi  21235  nmoix  21236  nmoi2  21237  nmoleub  21238  qdensere  21277  cnblcld  21282  ioo2blex  21299  tgioo  21301  blcvx  21303  zcld  21318  recld2  21319  iccntr  21326  icccmplem1  21327  reconnlem1  21331  reconnlem2  21332  opnreen  21336  metnrmlem3  21365  icoopnst  21439  cnheibor  21455  lebnumii  21466  nmoleub2lem  21597  lmnn  21702  iscau3  21717  minveclem4  21847  ivthlem1  21863  ivthlem2  21864  ivthlem3  21865  ivth2  21867  ivthle  21868  ivthle2  21869  ivthicc  21870  evthicc  21871  cniccbdd  21873  ovolgelb  21891  ovollb2lem  21899  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovoliun  21916  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem4  21931  ovolicc2lem5  21932  ovolicc2  21933  ovolicc  21934  nulmbl2  21947  voliunlem2  21961  ioombl1lem4  21971  ioorcl2  21981  uniioombllem1  21990  uniioombllem2a  21991  uniioombllem3  21994  dyaddisjlem  22004  dyadmaxlem  22006  opnmbllem  22010  volivth  22016  vitalilem4  22020  mbfmulc2lem  22054  mbfmax  22056  mbfposr  22059  ismbf3d  22061  mbfaddlem  22067  mbflimsup  22073  mbfi1fseqlem4  22125  itg2lcl  22134  xrge0f  22138  itg2itg1  22143  itg2const2  22148  itg2seq  22149  itg2uba  22150  itg2lea  22151  itg2mulclem  22153  itg2mulc  22154  itg2splitlem  22155  itg2split  22156  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  itg2cn  22170  iblss  22211  itgle  22216  itgeqa  22220  itgioo  22222  ibladdlem  22226  iblabs  22235  iblabsr  22236  iblmulc2  22237  itgsplit  22242  itgspliticc  22243  itgsplitioo  22244  bddmulibl  22245  ditgcl  22262  ditgswap  22263  ditgsplitlem  22264  dvferm1lem  22385  dvferm2lem  22387  dvferm  22389  rollelem  22390  rolle  22391  cmvth  22392  mvth  22393  dvlip  22394  dvlip2  22396  c1liplem1  22397  c1lip1  22398  dveq0  22401  dvgt0lem1  22403  dvivthlem1  22409  dvivth  22411  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvcnvrelem1  22418  dvcnvre  22420  dvcvx  22421  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsumrlimge0  22431  dvfsumrlim2  22433  ftc1lem1  22436  ftc1lem2  22437  ftc1a  22438  ftc1lem4  22440  ftc2  22445  ftc2ditglem  22446  itgparts  22448  itgsubstlem  22449  itgsubst  22450  degltlem1  22472  deg1ge  22499  coe1mul3  22500  deg1sublt  22511  deg1mul2  22515  deg1tmle  22518  deg1tm  22519  plypf1  22609  taylfvallem1  22752  tayl0  22757  pserulm  22817  psercnlem1  22820  pserdvlem1  22822  pserdvlem2  22823  abelthlem3  22828  abelth  22836  efcvx  22844  logno1  23017  logtayl  23041  xrlimcnp  23298  logfacbnd3  23498  log2sumbnd  23729  pntpbnd2  23772  pntibndlem3  23777  ttgcontlem1  24188  nvlmle  25602  nmooge0  25682  nmoub3i  25688  isblo3i  25716  ubthlem1  25786  minvecolem4  25796  nmopge0  26830  nmfnge0  26846  nmophmi  26950  branmfn  27024  xaddeq0  27573  xlt2addrd  27578  xmulcand  27617  xreceu  27618  xdivrec  27623  fsumrp0cl  27685  xrge0slmod  27834  cnre2csqlem  27892  tpr2rico  27894  xrge0iifcnv  27915  xrge0iifhom  27919  lmxrge0  27934  esumfsup  28076  esumpcvgval  28084  esumcvg  28092  dya2iocress  28245  dya2iocbrsiga  28246  dya2icobrsiga  28247  dya2icoseg  28248  dya2iocucvr  28255  sxbrsigalem2  28257  orvcgteel  28406  dstrvprob  28410  orvclteel  28411  sgnmul  28481  sgnsub  28483  sgnmulsgn  28488  sgnmulsgp  28489  signstcl  28522  signstf  28523  signstf0  28525  signstfvn  28526  signsvtn0  28527  signstfvneq0  28529  signsvfn  28539  signsvfpn  28542  signsvfnn  28543  cvmliftlem6  28735  cvmliftlem7  28736  cvmliftlem8  28737  cvmliftlem9  28738  cvmliftlem10  28739  cvmliftlem13  28741  sin2h  30045  cos2h  30046  tan2h  30047  heicant  30049  opnmbllem0  30050  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  itg2gt0cn  30070  ibladdnclem  30071  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  bddiblnc  30085  ftc1cnnclem  30088  ftc1anclem1  30090  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  ftc2nc  30099  areacirclem1  30107  areacirclem5  30111  areacirc  30112  ivthALT  30153  isbnd3  30280  blbnd  30283  prdsbnd  30289  prdsbnd2  30291  cntotbnd  30292  idomrootle  31152  idomodle  31153  itgpowd  31182  cvgdvgrat  31194  radcnvrat  31195  rfcnpre3  31408  rfcnpre4  31409  nnxrd  31419  lefldiveq  31482  lttri5d  31499  gtnelioc  31523  ltnelicc  31530  iooabslt  31532  gtnelicc  31533  eliooshift  31541  iocopn  31560  eliccelioc  31561  iooshift  31562  icoopn  31565  fprodge1  31598  limciccioolb  31627  lptioo1  31638  limcicciooub  31643  ltmod  31644  lptre2pt  31646  limsupre  31647  limcresiooub  31648  limcresioolb  31649  limcleqr  31650  sinaover2ne0  31668  ioccncflimc  31688  icccncfext  31690  icocncflimc  31692  cncfiooicclem1  31696  cncfiooicc  31697  cncfiooiccre  31698  cncfioobdlem  31699  dvbdfbdioolem1  31725  dvbdfbdioolem2  31726  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc1  31730  ioodvbdlimc2lem  31731  ioodvbdlimc2  31732  ditgeqiooicc  31759  iblsplit  31765  itgcoscmulx  31768  ibliooicc  31770  iblspltprt  31772  itgsincmulx  31773  itgsubsticc  31775  itgioocnicc  31776  iblcncfioo  31777  itgspltprt  31778  itgiccshift  31779  stoweidlem34  31816  stoweidlem52  31834  stirlinglem5  31860  dirkercncflem1  31885  dirkercncflem4  31888  fourierdlem4  31893  fourierdlem10  31899  fourierdlem19  31908  fourierdlem20  31909  fourierdlem24  31913  fourierdlem25  31914  fourierdlem26  31915  fourierdlem27  31916  fourierdlem28  31917  fourierdlem31  31920  fourierdlem32  31921  fourierdlem33  31922  fourierdlem35  31924  fourierdlem37  31926  fourierdlem40  31929  fourierdlem41  31930  fourierdlem43  31932  fourierdlem44  31933  fourierdlem46  31935  fourierdlem47  31936  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem52  31941  fourierdlem54  31943  fourierdlem57  31946  fourierdlem59  31948  fourierdlem60  31949  fourierdlem61  31950  fourierdlem62  31951  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem68  31957  fourierdlem69  31958  fourierdlem70  31959  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem84  31973  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem93  31982  fourierdlem94  31983  fourierdlem97  31986  fourierdlem100  31989  fourierdlem101  31990  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem109  31998  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fourierdlem114  32003  sqwvfoura  32011  fouriersw  32014  etransclem23  32040  etransclem46  32063  imo72b2  37993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-xr 9653