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

Theorem rexrd 10679
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 10673 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sseldi 3962 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cr 10524  *cxr 10662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-xr 10667
This theorem is referenced by:  xnn0xr  11960  rpxr  12386  rpxrd  12420  max0sub  12577  qextltlem  12583  xralrple  12586  xnegcl  12594  xaddf  12605  xnn0lem1lt  12625  xnn0lenn0nn0  12626  xmulf  12653  xadddi  12676  xrub  12693  supxrre  12708  infxrre  12717  ixxub  12747  ixxlb  12748  ioo0  12751  ico0  12772  ioc0  12773  iooshf  12803  icoshftf1o  12848  supicc  12874  supiccub  12875  supicclub  12876  xnn0xrge0  12879  ssfzunsn  12941  addmodid  13275  hashnnn0genn0  13691  hashunsnggt  13743  elicc4abs  14667  caucvgrlem  15017  fprodge1  15337  pcxcl  16185  pcdvdsb  16193  pcaddlem  16212  ramcl2lem  16333  ramlb  16343  0ram  16344  setsstruct  16511  prdsxmetlem  22905  xblss2ps  22938  xblss2  22939  blss2ps  22940  blss2  22941  blhalf  22942  metustto  23090  metustexhalf  23093  nmoi  23264  nmoix  23265  nmoi2  23266  nmoleub  23267  qdensere  23305  cnblcld  23310  ioo2blex  23329  tgioo  23331  blcvx  23333  zcld  23348  recld2  23349  iccntr  23356  icccmplem1  23357  reconnlem1  23361  reconnlem2  23362  opnreen  23366  metnrmlem3  23396  icoopnst  23470  iocopnst  23471  cnheibor  23486  lebnumii  23497  nmoleub2lem  23645  lmnn  23793  iscau3  23808  minveclem4  23962  ivthlem1  23979  ivthlem2  23980  ivthlem3  23981  ivth2  23983  ivthle  23984  ivthle2  23985  ivthicc  23986  evthicc  23987  cniccbdd  23989  ovolgelb  24008  ovollb2lem  24016  ovolunlem1  24025  ovoliunlem1  24030  ovoliunlem2  24031  ovoliun  24033  ovolscalem1  24041  ovolicc1  24044  ovolicc2lem4  24048  ovolicc2lem5  24049  ovolicc2  24050  ovolicc  24051  nulmbl2  24064  voliunlem2  24079  ioombl1lem4  24089  ioorcl2  24100  uniioombllem1  24109  uniioombllem2a  24110  uniioombllem3  24113  dyaddisjlem  24123  dyadmaxlem  24125  opnmbllem  24129  volivth  24135  vitalilem4  24139  mbfmulc2lem  24175  mbfmax  24177  mbfposr  24180  ismbf3d  24182  mbfaddlem  24188  mbflimsup  24194  mbfi1fseqlem4  24246  itg2lcl  24255  xrge0f  24259  itg2itg1  24264  itg2const2  24269  itg2seq  24270  itg2uba  24271  itg2lea  24272  itg2mulclem  24274  itg2mulc  24275  itg2splitlem  24276  itg2split  24277  itg2monolem2  24279  itg2monolem3  24280  itg2mono  24281  itg2gt0  24288  itg2cnlem1  24289  itg2cnlem2  24290  itg2cn  24291  iblss  24332  itgle  24337  itgeqa  24341  itgioo  24343  ibladdlem  24347  iblabs  24356  iblabsr  24357  iblmulc2  24358  itgsplit  24363  itgspliticc  24364  itgsplitioo  24365  bddmulibl  24366  ditgcl  24383  ditgswap  24384  ditgsplitlem  24385  dvferm1lem  24508  dvferm2lem  24510  dvferm  24512  rollelem  24513  rolle  24514  cmvth  24515  mvth  24516  dvlip  24517  dvlip2  24519  c1liplem1  24520  c1lip1  24521  dveq0  24524  dvgt0lem1  24526  dvivthlem1  24532  dvivth  24534  lhop1lem  24537  lhop1  24538  lhop2  24539  lhop  24540  dvcnvrelem1  24541  dvcnvre  24543  dvcvx  24544  dvfsumle  24545  dvfsumge  24546  dvfsumabs  24547  dvfsumlem2  24551  dvfsumlem3  24552  dvfsumlem4  24553  dvfsumrlimge0  24554  dvfsumrlim2  24556  ftc1lem1  24559  ftc1lem2  24560  ftc1a  24561  ftc1lem4  24563  ftc2  24568  ftc2ditglem  24569  itgparts  24571  itgsubstlem  24572  itgsubst  24573  degltlem1  24593  deg1ge  24619  coe1mul3  24620  deg1sublt  24631  deg1mul2  24635  deg1tmle  24638  deg1tm  24639  plypf1  24729  taylfvallem1  24872  tayl0  24877  pserulm  24937  psercnlem1  24940  pserdvlem1  24942  pserdvlem2  24943  abelthlem3  24948  abelth  24956  efcvx  24964  logno1  25146  logtayl  25170  xrlimcnp  25473  logfacbnd3  25726  log2sumbnd  26047  pntpbnd2  26090  pntibndlem3  26095  ttgcontlem1  26598  nmooge0  28471  nmoub3i  28477  isblo3i  28505  ubthlem1  28574  minvecolem4  28584  nmopge0  29615  nmfnge0  29631  nmophmi  29735  branmfn  29809  xaddeq0  30403  xlt2addrd  30408  xmulcand  30524  xreceu  30525  xdivrec  30530  fsumrp0cl  30609  xrge0slmod  30844  cnre2csqlem  31052  tpr2rico  31054  xrge0iifcnv  31075  xrge0iifhom  31079  lmxrge0  31094  esumfsup  31228  esumpcvgval  31236  esumcvg  31244  dya2iocress  31431  dya2iocbrsiga  31432  dya2icobrsiga  31433  dya2icoseg  31434  dya2iocucvr  31441  sxbrsigalem2  31443  omssubaddlem  31456  omssubadd  31457  orvcgteel  31624  dstrvprob  31628  orvclteel  31629  sgnmul  31699  sgnsub  31701  sgnmulsgn  31706  sgnmulsgp  31707  signstcl  31734  signstf  31735  signstf0  31737  signstfvn  31738  signsvtn0  31739  signsvfn  31751  signsvfpn  31754  signsvfnn  31755  ftc2re  31768  cvmliftlem6  32434  cvmliftlem7  32435  cvmliftlem8  32436  cvmliftlem9  32437  cvmliftlem10  32438  cvmliftlem13  32440  ivthALT  33580  iooelexlt  34525  relowlssretop  34526  relowlpssretop  34527  sin2h  34763  cos2h  34764  tan2h  34765  poimirlem30  34803  poimir  34806  heicant  34808  opnmbllem0  34809  mblfinlem1  34810  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  ismblfin  34814  itg2addnclem  34824  itg2addnclem2  34825  itg2gt0cn  34828  ibladdnclem  34829  iblabsnclem  34836  iblabsnc  34837  iblmulc2nc  34838  bddiblnc  34843  ftc1cnnclem  34846  ftc1anclem1  34848  ftc1anclem4  34851  ftc1anclem5  34852  ftc1anclem6  34853  ftc1anclem7  34854  ftc1anclem8  34855  ftc1anc  34856  ftc2nc  34857  areacirclem1  34863  areacirclem5  34867  areacirc  34868  isbnd3  34943  blbnd  34946  prdsbnd  34952  prdsbnd2  34954  cntotbnd  34955  idomrootle  39673  idomodle  39674  itgpowd  39699  imo72b2  40403  cvgdvgrat  40522  radcnvrat  40523  rfcnpre3  41167  rfcnpre4  41168  nnxrd  41176  absfico  41357  lefldiveq  41435  lttri5d  41442  supxrgere  41477  supxrgelem  41481  supxrge  41482  xralrple2  41498  infxr  41511  infleinflem1  41514  infleinflem2  41515  xralrple4  41517  xralrple3  41518  xrralrecnnle  41529  xrralrecnnge  41538  supxrunb3  41548  unb2ltle  41565  zxrd  41605  gtnelioc  41641  ltnelicc  41648  iooabslt  41650  gtnelicc  41651  eliooshift  41658  iocopn  41672  eliccelioc  41673  iooshift  41674  icoopn  41677  ge0lere  41684  iooiinicc  41694  sqrlearg  41705  iooiinioc  41708  uzinico  41712  preimaiocmnf  41713  uzubioo  41719  fsumge0cl  41730  limciccioolb  41778  lptioo1  41789  limcicciooub  41794  ltmod  41795  lptre2pt  41797  limsupre  41798  limcresiooub  41799  limcresioolb  41800  limcleqr  41801  limsupresico  41857  limsuppnfdlem  41858  limsupub  41861  limsupequzlem  41879  limsupre2lem  41881  limsupre3lem  41889  limsupvaluz2  41895  supcnvlimsup  41897  liminfresico  41928  limsup10exlem  41929  liminflelimsuplem  41932  limsupgtlem  41934  liminfval4  41946  liminfvaluz2  41952  limsupvaluz4  41957  liminflimsupclim  41964  xlimxrre  41988  xlimmnfvlem1  41989  xlimmnfv  41991  xlimpnfvlem1  41993  xlimpnfv  41995  sinaover2ne0  42025  ioccncflimc  42044  icccncfext  42046  icocncflimc  42048  cncfiooicclem1  42052  cncfiooicc  42053  cncfiooiccre  42054  cncfioobdlem  42055  dvbdfbdioolem1  42089  dvbdfbdioolem2  42090  dvbdfbdioo  42091  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  ioodvbdlimc1  42094  ioodvbdlimc2lem  42095  ioodvbdlimc2  42096  ditgeqiooicc  42121  iblsplit  42127  itgcoscmulx  42130  ibliooicc  42132  iblspltprt  42134  itgsincmulx  42135  itgsubsticc  42137  itgioocnicc  42138  iblcncfioo  42139  itgspltprt  42140  itgiccshift  42141  volioore  42152  voliooico  42154  voliooicof  42158  voliccico  42161  stoweidlem34  42196  stoweidlem52  42214  stirlinglem5  42240  dirkercncflem1  42265  dirkercncflem4  42268  fourierdlem4  42273  fourierdlem10  42279  fourierdlem19  42288  fourierdlem20  42289  fourierdlem24  42293  fourierdlem25  42294  fourierdlem26  42295  fourierdlem27  42296  fourierdlem28  42297  fourierdlem31  42300  fourierdlem32  42301  fourierdlem33  42302  fourierdlem35  42304  fourierdlem37  42306  fourierdlem40  42309  fourierdlem41  42310  fourierdlem43  42312  fourierdlem44  42313  fourierdlem46  42314  fourierdlem47  42315  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem51  42319  fourierdlem52  42320  fourierdlem54  42322  fourierdlem57  42325  fourierdlem59  42327  fourierdlem60  42328  fourierdlem61  42329  fourierdlem62  42330  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem68  42336  fourierdlem69  42337  fourierdlem70  42338  fourierdlem72  42340  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem78  42346  fourierdlem79  42347  fourierdlem81  42349  fourierdlem82  42350  fourierdlem84  42352  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  fourierdlem92  42360  fourierdlem93  42361  fourierdlem94  42362  fourierdlem97  42365  fourierdlem100  42368  fourierdlem101  42369  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem107  42375  fourierdlem109  42377  fourierdlem111  42379  fourierdlem112  42380  fourierdlem113  42381  fourierdlem114  42382  sqwvfoura  42390  fouriersw  42393  etransclem23  42419  etransclem46  42442  qndenserrnbllem  42456  rrxsnicc  42462  ioorrnopnlem  42466  ioorrnopnxrlem  42468  salgencntex  42503  sge0cl  42540  sge0fsum  42546  sge0iunmptlemre  42574  sge0isum  42586  sge0ad2en  42590  sge0xaddlem1  42592  sge0xaddlem2  42593  sge0reuz  42606  voliunsge0lem  42631  meassre  42636  omessre  42669  omeiunltfirp  42678  hoissre  42703  hoiprodcl  42706  ovnsubaddlem1  42729  hoiprodcl3  42739  hoidmvcl  42741  hsphoidmvle2  42744  hsphoidmvle  42745  sge0hsphoire  42748  hoidmv1lelem1  42750  hoidmv1lelem2  42751  hoidmv1lelem3  42752  hoidmv1le  42753  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem4  42757  ovnhoilem1  42760  ovnhoilem2  42761  ovnhoi  42762  ovnlecvr2  42769  hspdifhsp  42775  hoidifhspdmvle  42779  hoiqssbllem1  42781  hoiqssbllem2  42782  hoiqssbllem3  42783  hspmbllem1  42785  hspmbllem2  42786  volicorege0  42796  ovolval5lem1  42811  ovolval5lem2  42812  iinhoiicclem  42832  iinhoiicc  42833  iunhoiioolem  42834  iunhoiioo  42835  vonioolem2  42840  vonicclem2  42843  vonsn  42850  pimltmnf2  42856  pimconstlt0  42859  pimgtpnf2  42862  salpreimagelt  42863  salpreimalegt  42865  preimageiingt  42875  preimaleiinlt  42876  pimrecltneg  42878  issmflem  42881  issmflelem  42898  issmfgtlem  42909  issmfgt  42910  smfaddlem1  42916  issmfgelem  42922  issmfge  42923  smfpimioompt  42938  smfresal  42940  smfrec  42941  smfmullem1  42943  smfmullem2  42944  smfmullem3  42945  smfmullem4  42946  smfpimbor1lem1  42950  smfsuplem1  42962  smflimsuplem4  42974  smfliminflem  42981  bgoldbtbnd  43851  eenglngeehlnmlem2  44653
  Copyright terms: Public domain W3C validator