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

Theorem rexrd 9968
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 9962 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sseldi 3566 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cr 9814  *cxr 9952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-xr 9957
This theorem is referenced by:  xnn0xr  11245  rpxr  11716  rpxrd  11749  max0sub  11901  qextltlem  11907  xralrple  11910  xnegcl  11918  xaddf  11929  xmulf  11974  xadddi  11997  supxrre  12029  infxrre  12038  ixxub  12067  ixxlb  12068  ioo0  12071  ico0  12092  ioc0  12093  iooshf  12123  icoshftf1o  12166  supicc  12191  supiccub  12192  supicclub  12193  xnn0xrge0  12196  addmodid  12580  hashnnn0genn0  12993  elicc4abs  13907  caucvgrlem  14251  fprodge1  14565  pcxcl  15403  pcdvdsb  15411  pcaddlem  15430  ramcl2lem  15551  ramlb  15561  0ram  15562  prdsxmetlem  21983  xblss2ps  22016  xblss2  22017  blss2ps  22018  blss2  22019  blhalf  22020  metustto  22168  metustexhalf  22171  nmoi  22342  nmoix  22343  nmoi2  22344  nmoleub  22345  qdensere  22383  cnblcld  22388  ioo2blex  22405  tgioo  22407  blcvx  22409  zcld  22424  recld2  22425  iccntr  22432  icccmplem1  22433  reconnlem1  22437  reconnlem2  22438  opnreen  22442  metnrmlem3  22472  icoopnst  22546  cnheibor  22562  lebnumii  22573  nmoleub2lem  22722  lmnn  22869  iscau3  22884  minveclem4  23011  ivthlem1  23027  ivthlem2  23028  ivthlem3  23029  ivth2  23031  ivthle  23032  ivthle2  23033  ivthicc  23034  evthicc  23035  cniccbdd  23037  ovolgelb  23055  ovollb2lem  23063  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovoliun  23080  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicc2  23097  ovolicc  23098  nulmbl2  23111  voliunlem2  23126  ioombl1lem4  23136  ioorcl2  23146  uniioombllem1  23155  uniioombllem2a  23156  uniioombllem3  23159  dyaddisjlem  23169  dyadmaxlem  23171  opnmbllem  23175  volivth  23181  vitalilem4  23186  mbfmulc2lem  23220  mbfmax  23222  mbfposr  23225  ismbf3d  23227  mbfaddlem  23233  mbflimsup  23239  mbfi1fseqlem4  23291  itg2lcl  23300  xrge0f  23304  itg2itg1  23309  itg2const2  23314  itg2seq  23315  itg2uba  23316  itg2lea  23317  itg2mulclem  23319  itg2mulc  23320  itg2splitlem  23321  itg2split  23322  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  itg2cn  23336  iblss  23377  itgle  23382  itgeqa  23386  itgioo  23388  ibladdlem  23392  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgsplit  23408  itgspliticc  23409  itgsplitioo  23410  bddmulibl  23411  ditgcl  23428  ditgswap  23429  ditgsplitlem  23430  dvferm1lem  23551  dvferm2lem  23553  dvferm  23555  rollelem  23556  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlip2  23562  c1liplem1  23563  c1lip1  23564  dveq0  23567  dvgt0lem1  23569  dvivthlem1  23575  dvivth  23577  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  dvcnvrelem1  23584  dvcnvre  23586  dvcvx  23587  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlimge0  23597  dvfsumrlim2  23599  ftc1lem1  23602  ftc1lem2  23603  ftc1a  23604  ftc1lem4  23606  ftc2  23611  ftc2ditglem  23612  itgparts  23614  itgsubstlem  23615  itgsubst  23616  degltlem1  23636  deg1ge  23662  coe1mul3  23663  deg1sublt  23674  deg1mul2  23678  deg1tmle  23681  deg1tm  23682  plypf1  23772  taylfvallem1  23915  tayl0  23920  pserulm  23980  psercnlem1  23983  pserdvlem1  23985  pserdvlem2  23986  abelthlem3  23991  abelth  23999  efcvx  24007  logno1  24182  logtayl  24206  xrlimcnp  24495  logfacbnd3  24748  log2sumbnd  25033  pntpbnd2  25076  pntibndlem3  25081  ttgcontlem1  25565  nmooge0  27006  nmoub3i  27012  isblo3i  27040  ubthlem1  27110  minvecolem4  27120  nmopge0  28154  nmfnge0  28170  nmophmi  28274  branmfn  28348  xaddeq0  28907  xlt2addrd  28913  xmulcand  28960  xreceu  28961  xdivrec  28966  fsumrp0cl  29026  xrge0slmod  29175  cnre2csqlem  29284  tpr2rico  29286  xrge0iifcnv  29307  xrge0iifhom  29311  lmxrge0  29326  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  dya2iocress  29663  dya2iocbrsiga  29664  dya2icobrsiga  29665  dya2icoseg  29666  dya2iocucvr  29673  sxbrsigalem2  29675  omssubaddlem  29688  omssubadd  29689  orvcgteel  29856  dstrvprob  29860  orvclteel  29861  sgnmul  29931  sgnsub  29933  sgnmulsgn  29938  sgnmulsgp  29939  signstcl  29968  signstf  29969  signstf0  29971  signstfvn  29972  signsvtn0  29973  signstfvneq0  29975  signsvfn  29985  signsvfpn  29988  signsvfnn  29989  cvmliftlem6  30526  cvmliftlem7  30527  cvmliftlem8  30528  cvmliftlem9  30529  cvmliftlem10  30530  cvmliftlem13  30532  ivthALT  31500  iooelexlt  32386  relowlssretop  32387  relowlpssretop  32388  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem30  32609  poimir  32612  heicant  32614  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnclem2  32632  itg2gt0cn  32635  ibladdnclem  32636  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  bddiblnc  32650  ftc1cnnclem  32653  ftc1anclem1  32655  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  ftc2nc  32664  areacirclem1  32670  areacirclem5  32674  areacirc  32675  isbnd3  32753  blbnd  32756  prdsbnd  32762  prdsbnd2  32764  cntotbnd  32765  idomrootle  36792  idomodle  36793  itgpowd  36819  imo72b2  37497  cvgdvgrat  37534  radcnvrat  37535  rfcnpre3  38215  rfcnpre4  38216  nnxrd  38224  absfico  38405  lefldiveq  38446  lttri5d  38454  supxrgere  38490  supxrgelem  38494  supxrge  38495  xralrple2  38511  infxr  38524  infleinflem1  38527  infleinflem2  38528  xralrple4  38530  xralrple3  38531  xrralrecnnle  38543  xrralrecnnge  38554  gtnelioc  38559  ltnelicc  38566  iooabslt  38568  gtnelicc  38569  eliooshift  38576  iocopn  38593  eliccelioc  38594  iooshift  38595  icoopn  38598  ge0lere  38606  iooiinicc  38616  sqrlearg  38627  iooiinioc  38630  fsumge0cl  38640  limciccioolb  38688  lptioo1  38699  limcicciooub  38704  ltmod  38705  lptre2pt  38707  limsupre  38708  limcresiooub  38709  limcresioolb  38710  limcleqr  38711  sinaover2ne0  38751  ioccncflimc  38771  icccncfext  38773  icocncflimc  38775  cncfiooicclem1  38779  cncfiooicc  38780  cncfiooiccre  38781  cncfioobdlem  38782  dvbdfbdioolem1  38818  dvbdfbdioolem2  38819  dvbdfbdioo  38820  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc1  38823  ioodvbdlimc2lem  38824  ioodvbdlimc2  38825  ditgeqiooicc  38852  iblsplit  38858  itgcoscmulx  38861  ibliooicc  38863  iblspltprt  38865  itgsincmulx  38866  itgsubsticc  38868  itgioocnicc  38869  iblcncfioo  38870  itgspltprt  38871  itgiccshift  38872  volioore  38883  voliooico  38885  voliooicof  38889  voliccico  38892  stoweidlem34  38927  stoweidlem52  38945  stirlinglem5  38971  dirkercncflem1  38996  dirkercncflem4  38999  fourierdlem4  39004  fourierdlem10  39010  fourierdlem19  39019  fourierdlem20  39020  fourierdlem24  39024  fourierdlem25  39025  fourierdlem26  39026  fourierdlem27  39027  fourierdlem28  39028  fourierdlem31  39031  fourierdlem32  39032  fourierdlem33  39033  fourierdlem35  39035  fourierdlem37  39037  fourierdlem40  39040  fourierdlem41  39041  fourierdlem43  39043  fourierdlem44  39044  fourierdlem46  39045  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem52  39051  fourierdlem54  39053  fourierdlem57  39056  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem68  39067  fourierdlem69  39068  fourierdlem70  39069  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem84  39083  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem94  39093  fourierdlem97  39096  fourierdlem100  39099  fourierdlem101  39100  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem109  39108  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fourierdlem114  39113  sqwvfoura  39121  fouriersw  39124  etransclem23  39150  etransclem46  39173  qndenserrnbllem  39190  rrxsnicc  39196  ioorrnopnlem  39200  ioorrnopnxrlem  39202  salgencntex  39237  sge0cl  39274  sge0fsum  39280  sge0iunmptlemre  39308  sge0isum  39320  sge0ad2en  39324  sge0xaddlem1  39326  sge0xaddlem2  39327  sge0reuz  39340  voliunsge0lem  39365  meassre  39370  omessre  39400  omeiunltfirp  39409  hoissre  39434  hoiprodcl  39437  ovnsubaddlem1  39460  hoiprodcl3  39470  hoidmvcl  39472  hsphoidmvle2  39475  hsphoidmvle  39476  sge0hsphoire  39479  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  ovnhoilem1  39491  ovnhoilem2  39492  ovnhoi  39493  ovnlecvr2  39500  hspdifhsp  39506  hoidifhspdmvle  39510  hoiqssbllem1  39512  hoiqssbllem2  39513  hoiqssbllem3  39514  hspmbllem1  39516  hspmbllem2  39517  volicorege0  39527  ovolval5lem1  39542  ovolval5lem2  39543  iinhoiicclem  39564  iinhoiicc  39565  iunhoiioolem  39566  iunhoiioo  39567  vonioolem2  39572  vonicclem2  39575  vonsn  39582  pimltmnf2  39588  pimconstlt0  39591  pimgtpnf2  39594  salpreimagelt  39595  salpreimalegt  39597  preimageiingt  39607  preimaleiinlt  39608  pimrecltneg  39610  issmflem  39613  issmflelem  39631  issmfgtlem  39642  issmfgt  39643  smfaddlem1  39649  issmfgelem  39655  issmfge  39656  smfpimioompt  39671  smfresal  39673  smfrec  39674  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  smfmullem4  39679  smfpimbor1lem1  39683  bgoldbtbnd  40225
  Copyright terms: Public domain W3C validator