MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexrd Structured version   Visualization version   GIF version

Theorem rexrd 10086
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
StepHypRef Expression
1 ressxr 10080 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sseldi 3599 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  cr 9932  *cxr 10070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-un 3577  df-in 3579  df-ss 3586  df-xr 10075
This theorem is referenced by:  xnn0xr  11365  rpxr  11837  rpxrd  11870  max0sub  12024  qextltlem  12030  xralrple  12033  xnegcl  12041  xaddf  12052  xnn0lenn0nn0  12072  xmulf  12099  xadddi  12122  supxrre  12154  infxrre  12163  ixxub  12193  ixxlb  12194  ioo0  12197  ico0  12218  ioc0  12219  iooshf  12249  icoshftf1o  12292  supicc  12317  supiccub  12318  supicclub  12319  xnn0xrge0  12322  ssfzunsn  12384  addmodid  12713  hashnnn0genn0  13126  elicc4abs  14053  caucvgrlem  14397  fprodge1  14720  pcxcl  15559  pcdvdsb  15567  pcaddlem  15586  ramcl2lem  15707  ramlb  15717  0ram  15718  setsstruct  15892  prdsxmetlem  22167  xblss2ps  22200  xblss2  22201  blss2ps  22202  blss2  22203  blhalf  22204  metustto  22352  metustexhalf  22355  nmoi  22526  nmoix  22527  nmoi2  22528  nmoleub  22529  qdensere  22567  cnblcld  22572  ioo2blex  22591  tgioo  22593  blcvx  22595  zcld  22610  recld2  22611  iccntr  22618  icccmplem1  22619  reconnlem1  22623  reconnlem2  22624  opnreen  22628  metnrmlem3  22658  icoopnst  22732  cnheibor  22748  lebnumii  22759  nmoleub2lem  22908  lmnn  23055  iscau3  23070  minveclem4  23197  ivthlem1  23214  ivthlem2  23215  ivthlem3  23216  ivth2  23218  ivthle  23219  ivthle2  23220  ivthicc  23221  evthicc  23222  cniccbdd  23224  ovolgelb  23242  ovollb2lem  23250  ovolunlem1  23259  ovoliunlem1  23264  ovoliunlem2  23265  ovoliun  23267  ovolscalem1  23275  ovolicc1  23278  ovolicc2lem4  23282  ovolicc2lem5  23283  ovolicc2  23284  ovolicc  23285  nulmbl2  23298  voliunlem2  23313  ioombl1lem4  23323  ioorcl2  23334  uniioombllem1  23343  uniioombllem2a  23344  uniioombllem3  23347  dyaddisjlem  23357  dyadmaxlem  23359  opnmbllem  23363  volivth  23369  vitalilem4  23374  mbfmulc2lem  23408  mbfmax  23410  mbfposr  23413  ismbf3d  23415  mbfaddlem  23421  mbflimsup  23427  mbfi1fseqlem4  23479  itg2lcl  23488  xrge0f  23492  itg2itg1  23497  itg2const2  23502  itg2seq  23503  itg2uba  23504  itg2lea  23505  itg2mulclem  23507  itg2mulc  23508  itg2splitlem  23509  itg2split  23510  itg2monolem2  23512  itg2monolem3  23513  itg2mono  23514  itg2gt0  23521  itg2cnlem1  23522  itg2cnlem2  23523  itg2cn  23524  iblss  23565  itgle  23570  itgeqa  23574  itgioo  23576  ibladdlem  23580  iblabs  23589  iblabsr  23590  iblmulc2  23591  itgsplit  23596  itgspliticc  23597  itgsplitioo  23598  bddmulibl  23599  ditgcl  23616  ditgswap  23617  ditgsplitlem  23618  dvferm1lem  23741  dvferm2lem  23743  dvferm  23745  rollelem  23746  rolle  23747  cmvth  23748  mvth  23749  dvlip  23750  dvlip2  23752  c1liplem1  23753  c1lip1  23754  dveq0  23757  dvgt0lem1  23759  dvivthlem1  23765  dvivth  23767  lhop1lem  23770  lhop1  23771  lhop2  23772  lhop  23773  dvcnvrelem1  23774  dvcnvre  23776  dvcvx  23777  dvfsumle  23778  dvfsumge  23779  dvfsumabs  23780  dvfsumlem2  23784  dvfsumlem3  23785  dvfsumlem4  23786  dvfsumrlimge0  23787  dvfsumrlim2  23789  ftc1lem1  23792  ftc1lem2  23793  ftc1a  23794  ftc1lem4  23796  ftc2  23801  ftc2ditglem  23802  itgparts  23804  itgsubstlem  23805  itgsubst  23806  degltlem1  23826  deg1ge  23852  coe1mul3  23853  deg1sublt  23864  deg1mul2  23868  deg1tmle  23871  deg1tm  23872  plypf1  23962  taylfvallem1  24105  tayl0  24110  pserulm  24170  psercnlem1  24173  pserdvlem1  24175  pserdvlem2  24176  abelthlem3  24181  abelth  24189  efcvx  24197  logno1  24376  logtayl  24400  xrlimcnp  24689  logfacbnd3  24942  log2sumbnd  25227  pntpbnd2  25270  pntibndlem3  25275  ttgcontlem1  25759  nmooge0  27606  nmoub3i  27612  isblo3i  27640  ubthlem1  27710  minvecolem4  27720  nmopge0  28754  nmfnge0  28770  nmophmi  28874  branmfn  28948  xaddeq0  29503  xlt2addrd  29508  xmulcand  29614  xreceu  29615  xdivrec  29620  fsumrp0cl  29680  xrge0slmod  29829  cnre2csqlem  29941  tpr2rico  29943  xrge0iifcnv  29964  xrge0iifhom  29968  lmxrge0  29983  esumfsup  30117  esumpcvgval  30125  esumcvg  30133  dya2iocress  30321  dya2iocbrsiga  30322  dya2icobrsiga  30323  dya2icoseg  30324  dya2iocucvr  30331  sxbrsigalem2  30333  omssubaddlem  30346  omssubadd  30347  orvcgteel  30514  dstrvprob  30518  orvclteel  30519  sgnmul  30589  sgnsub  30591  sgnmulsgn  30596  sgnmulsgp  30597  signstcl  30627  signstf  30628  signstf0  30630  signstfvn  30631  signsvtn0  30632  signstfvneq0  30634  signsvfn  30644  signsvfpn  30647  signsvfnn  30648  ftc2re  30661  cvmliftlem6  31257  cvmliftlem7  31258  cvmliftlem8  31259  cvmliftlem9  31260  cvmliftlem10  31261  cvmliftlem13  31263  ivthALT  32314  iooelexlt  33190  relowlssretop  33191  relowlpssretop  33192  sin2h  33379  cos2h  33380  tan2h  33381  poimirlem30  33419  poimir  33422  heicant  33424  opnmbllem0  33425  mblfinlem1  33426  mblfinlem2  33427  mblfinlem3  33428  mblfinlem4  33429  ismblfin  33430  itg2addnclem  33441  itg2addnclem2  33442  itg2gt0cn  33445  ibladdnclem  33446  iblabsnclem  33453  iblabsnc  33454  iblmulc2nc  33455  bddiblnc  33460  ftc1cnnclem  33463  ftc1anclem1  33465  ftc1anclem4  33468  ftc1anclem5  33469  ftc1anclem6  33470  ftc1anclem7  33471  ftc1anclem8  33472  ftc1anc  33473  ftc2nc  33474  areacirclem1  33480  areacirclem5  33484  areacirc  33485  isbnd3  33563  blbnd  33566  prdsbnd  33572  prdsbnd2  33574  cntotbnd  33575  idomrootle  37599  idomodle  37600  itgpowd  37626  imo72b2  38301  cvgdvgrat  38338  radcnvrat  38339  rfcnpre3  39018  rfcnpre4  39019  nnxrd  39027  absfico  39232  lefldiveq  39324  lttri5d  39332  supxrgere  39368  supxrgelem  39372  supxrge  39373  xralrple2  39389  infxr  39402  infleinflem1  39405  infleinflem2  39406  xralrple4  39408  xralrple3  39409  xrralrecnnle  39421  xrralrecnnge  39432  supxrunb3  39442  unb2ltle  39461  zxrd  39501  gtnelioc  39521  ltnelicc  39528  iooabslt  39530  gtnelicc  39531  eliooshift  39538  iocopn  39555  eliccelioc  39556  iooshift  39557  icoopn  39560  ge0lere  39568  iooiinicc  39578  sqrlearg  39589  iooiinioc  39592  uzinico  39596  preimaiocmnf  39597  uzubioo  39603  fsumge0cl  39611  limciccioolb  39659  lptioo1  39670  limcicciooub  39675  ltmod  39676  lptre2pt  39678  limsupre  39679  limcresiooub  39680  limcresioolb  39681  limcleqr  39682  limsupresico  39738  limsuppnfdlem  39739  limsupub  39742  limsupequzlem  39760  limsupre2lem  39762  limsupre3lem  39770  limsupvaluz2  39776  supcnvlimsup  39778  liminfresico  39803  limsup10exlem  39804  liminflelimsuplem  39807  limsupgtlem  39809  liminfval4  39821  liminfvaluz2  39827  limsupvaluz4  39832  liminflimsupclim  39839  sinaover2ne0  39848  ioccncflimc  39867  icccncfext  39869  icocncflimc  39871  cncfiooicclem1  39875  cncfiooicc  39876  cncfiooiccre  39877  cncfioobdlem  39878  dvbdfbdioolem1  39912  dvbdfbdioolem2  39913  dvbdfbdioo  39914  ioodvbdlimc1lem1  39915  ioodvbdlimc1lem2  39916  ioodvbdlimc1  39917  ioodvbdlimc2lem  39918  ioodvbdlimc2  39919  ditgeqiooicc  39945  iblsplit  39951  itgcoscmulx  39954  ibliooicc  39956  iblspltprt  39958  itgsincmulx  39959  itgsubsticc  39961  itgioocnicc  39962  iblcncfioo  39963  itgspltprt  39964  itgiccshift  39965  volioore  39976  voliooico  39978  voliooicof  39982  voliccico  39985  stoweidlem34  40020  stoweidlem52  40038  stirlinglem5  40064  dirkercncflem1  40089  dirkercncflem4  40092  fourierdlem4  40097  fourierdlem10  40103  fourierdlem19  40112  fourierdlem20  40113  fourierdlem24  40117  fourierdlem25  40118  fourierdlem26  40119  fourierdlem27  40120  fourierdlem28  40121  fourierdlem31  40124  fourierdlem32  40125  fourierdlem33  40126  fourierdlem35  40128  fourierdlem37  40130  fourierdlem40  40133  fourierdlem41  40134  fourierdlem43  40136  fourierdlem44  40137  fourierdlem46  40138  fourierdlem47  40139  fourierdlem48  40140  fourierdlem49  40141  fourierdlem50  40142  fourierdlem51  40143  fourierdlem52  40144  fourierdlem54  40146  fourierdlem57  40149  fourierdlem59  40151  fourierdlem60  40152  fourierdlem61  40153  fourierdlem62  40154  fourierdlem63  40155  fourierdlem64  40156  fourierdlem65  40157  fourierdlem68  40160  fourierdlem69  40161  fourierdlem70  40162  fourierdlem72  40164  fourierdlem73  40165  fourierdlem74  40166  fourierdlem75  40167  fourierdlem76  40168  fourierdlem78  40170  fourierdlem79  40171  fourierdlem81  40173  fourierdlem82  40174  fourierdlem84  40176  fourierdlem89  40181  fourierdlem90  40182  fourierdlem91  40183  fourierdlem92  40184  fourierdlem93  40185  fourierdlem94  40186  fourierdlem97  40189  fourierdlem100  40192  fourierdlem101  40193  fourierdlem102  40194  fourierdlem103  40195  fourierdlem104  40196  fourierdlem107  40199  fourierdlem109  40201  fourierdlem111  40203  fourierdlem112  40204  fourierdlem113  40205  fourierdlem114  40206  sqwvfoura  40214  fouriersw  40217  etransclem23  40243  etransclem46  40266  qndenserrnbllem  40283  rrxsnicc  40289  ioorrnopnlem  40293  ioorrnopnxrlem  40295  salgencntex  40330  sge0cl  40367  sge0fsum  40373  sge0iunmptlemre  40401  sge0isum  40413  sge0ad2en  40417  sge0xaddlem1  40419  sge0xaddlem2  40420  sge0reuz  40433  voliunsge0lem  40458  meassre  40463  omessre  40493  omeiunltfirp  40502  hoissre  40527  hoiprodcl  40530  ovnsubaddlem1  40553  hoiprodcl3  40563  hoidmvcl  40565  hsphoidmvle2  40568  hsphoidmvle  40569  sge0hsphoire  40572  hoidmv1lelem1  40574  hoidmv1lelem2  40575  hoidmv1lelem3  40576  hoidmv1le  40577  hoidmvlelem1  40578  hoidmvlelem2  40579  hoidmvlelem3  40580  hoidmvlelem4  40581  ovnhoilem1  40584  ovnhoilem2  40585  ovnhoi  40586  ovnlecvr2  40593  hspdifhsp  40599  hoidifhspdmvle  40603  hoiqssbllem1  40605  hoiqssbllem2  40606  hoiqssbllem3  40607  hspmbllem1  40609  hspmbllem2  40610  volicorege0  40620  ovolval5lem1  40635  ovolval5lem2  40636  iinhoiicclem  40656  iinhoiicc  40657  iunhoiioolem  40658  iunhoiioo  40659  vonioolem2  40664  vonicclem2  40667  vonsn  40674  pimltmnf2  40680  pimconstlt0  40683  pimgtpnf2  40686  salpreimagelt  40687  salpreimalegt  40689  preimageiingt  40699  preimaleiinlt  40700  pimrecltneg  40702  issmflem  40705  issmflelem  40722  issmfgtlem  40733  issmfgt  40734  smfaddlem1  40740  issmfgelem  40746  issmfge  40747  smfpimioompt  40762  smfresal  40764  smfrec  40765  smfmullem1  40767  smfmullem2  40768  smfmullem3  40769  smfmullem4  40770  smfpimbor1lem1  40774  smfsuplem1  40786  smflimsuplem4  40798  smfliminflem  40805  bgoldbtbnd  41468
  Copyright terms: Public domain W3C validator