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

Theorem rexrd 10907
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 10901 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sselid 3912 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  cr 10752  *cxr 10890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3422  df-un 3885  df-in 3887  df-ss 3897  df-xr 10895
This theorem is referenced by:  xnn0xr  12191  rpxr  12619  rpxrd  12653  max0sub  12810  qextltlem  12816  xralrple  12819  xnegcl  12827  xaddf  12838  xnn0lem1lt  12858  xnn0lenn0nn0  12859  xmulf  12886  xadddi  12909  xrub  12926  supxrre  12941  infxrre  12950  ixxub  12980  ixxlb  12981  ioo0  12984  ico0  13005  ioc0  13006  iooshf  13038  icoshftf1o  13086  supicc  13113  supiccub  13114  supicclub  13115  xnn0xrge0  13118  ssfzunsn  13182  addmodid  13516  hashnnn0genn0  13933  hashunsnggt  13985  elicc4abs  14907  caucvgrlem  15260  fprodge1  15581  pcxcl  16438  pcdvdsb  16446  pcaddlem  16465  ramcl2lem  16586  ramlb  16596  0ram  16597  setsstruct  16753  prdsxmetlem  23290  xblss2ps  23323  xblss2  23324  blss2ps  23325  blss2  23326  blhalf  23327  metustto  23475  metustexhalf  23478  nmoi  23650  nmoix  23651  nmoi2  23652  nmoleub  23653  qdensere  23691  cnblcld  23696  ioo2blex  23715  tgioo  23717  blcvx  23719  zcld  23734  recld2  23735  iccntr  23742  icccmplem1  23743  reconnlem1  23747  reconnlem2  23748  opnreen  23752  metnrmlem3  23782  icoopnst  23860  iocopnst  23861  cnheibor  23876  lebnumii  23887  nmoleub2lem  24035  lmnn  24184  iscau3  24199  minveclem4  24353  ivthlem1  24372  ivthlem2  24373  ivthlem3  24374  ivth2  24376  ivthle  24377  ivthle2  24378  ivthicc  24379  evthicc  24380  cniccbdd  24382  ovolgelb  24401  ovollb2lem  24409  ovolunlem1  24418  ovoliunlem1  24423  ovoliunlem2  24424  ovoliun  24426  ovolscalem1  24434  ovolicc1  24437  ovolicc2lem4  24441  ovolicc2lem5  24442  ovolicc2  24443  ovolicc  24444  nulmbl2  24457  voliunlem2  24472  ioombl1lem4  24482  ioorcl2  24493  uniioombllem1  24502  uniioombllem2a  24503  uniioombllem3  24506  dyaddisjlem  24516  dyadmaxlem  24518  opnmbllem  24522  volivth  24528  vitalilem4  24532  mbfmulc2lem  24568  mbfmax  24570  mbfposr  24573  ismbf3d  24575  mbfaddlem  24581  mbflimsup  24587  mbfi1fseqlem4  24640  itg2lcl  24649  xrge0f  24653  itg2itg1  24658  itg2const2  24663  itg2seq  24664  itg2uba  24665  itg2lea  24666  itg2mulclem  24668  itg2mulc  24669  itg2splitlem  24670  itg2split  24671  itg2monolem2  24673  itg2monolem3  24674  itg2mono  24675  itg2gt0  24682  itg2cnlem1  24683  itg2cnlem2  24684  itg2cn  24685  iblss  24726  itgle  24731  itgeqa  24735  itgioo  24737  ibladdlem  24741  iblabs  24750  iblabsr  24751  iblmulc2  24752  itgsplit  24757  itgspliticc  24758  itgsplitioo  24759  bddmulibl  24760  bddiblnc  24763  ditgcl  24779  ditgswap  24780  ditgsplitlem  24781  dvferm1lem  24905  dvferm2lem  24907  dvferm  24909  rollelem  24910  rolle  24911  cmvth  24912  mvth  24913  dvlip  24914  dvlip2  24916  c1liplem1  24917  c1lip1  24918  dveq0  24921  dvgt0lem1  24923  dvivthlem1  24929  dvivth  24931  lhop1lem  24934  lhop1  24935  lhop2  24936  lhop  24937  dvcnvrelem1  24938  dvcnvre  24940  dvcvx  24941  dvfsumle  24942  dvfsumge  24943  dvfsumabs  24944  dvfsumlem2  24948  dvfsumlem3  24949  dvfsumlem4  24950  dvfsumrlimge0  24951  dvfsumrlim2  24953  ftc1lem1  24956  ftc1lem2  24957  ftc1a  24958  ftc1lem4  24960  ftc2  24965  ftc2ditglem  24966  itgparts  24968  itgsubstlem  24969  itgsubst  24970  itgpowd  24971  degltlem1  24994  deg1ge  25020  coe1mul3  25021  deg1sublt  25032  deg1mul2  25036  deg1tmle  25039  deg1tm  25040  plypf1  25130  taylfvallem1  25273  tayl0  25278  pserulm  25338  psercnlem1  25341  pserdvlem1  25343  pserdvlem2  25344  abelthlem3  25349  abelth  25357  efcvx  25365  logno1  25548  logtayl  25572  xrlimcnp  25875  logfacbnd3  26128  log2sumbnd  26449  pntpbnd2  26492  pntibndlem3  26497  ttgcontlem1  27000  nmooge0  28872  nmoub3i  28878  isblo3i  28906  ubthlem1  28975  minvecolem4  28985  nmopge0  30016  nmfnge0  30032  nmophmi  30136  branmfn  30210  xaddeq0  30820  xlt2addrd  30825  xmulcand  30939  xreceu  30940  xdivrec  30945  fsumrp0cl  31047  xrge0slmod  31286  cnre2csqlem  31598  tpr2rico  31600  xrge0iifcnv  31621  xrge0iifhom  31625  lmxrge0  31640  esumfsup  31774  esumpcvgval  31782  esumcvg  31790  dya2iocress  31977  dya2iocbrsiga  31978  dya2icobrsiga  31979  dya2icoseg  31980  dya2iocucvr  31987  sxbrsigalem2  31989  omssubaddlem  32002  omssubadd  32003  orvcgteel  32170  dstrvprob  32174  orvclteel  32175  sgnmul  32245  sgnsub  32247  sgnmulsgn  32252  sgnmulsgp  32253  signstcl  32280  signstf  32281  signstf0  32283  signstfvn  32284  signsvtn0  32285  signsvfn  32297  signsvfpn  32300  signsvfnn  32301  ftc2re  32314  cvmliftlem6  32988  cvmliftlem7  32989  cvmliftlem8  32990  cvmliftlem9  32991  cvmliftlem10  32992  cvmliftlem13  32994  ivthALT  34287  iooelexlt  35296  relowlssretop  35297  relowlpssretop  35298  sin2h  35530  cos2h  35531  tan2h  35532  poimirlem30  35570  poimir  35573  heicant  35575  opnmbllem0  35576  mblfinlem1  35577  mblfinlem2  35578  mblfinlem3  35579  mblfinlem4  35580  ismblfin  35581  itg2addnclem  35591  itg2addnclem2  35592  itg2gt0cn  35595  ibladdnclem  35596  iblabsnclem  35603  iblabsnc  35604  iblmulc2nc  35605  ftc1cnnclem  35611  ftc1anclem1  35613  ftc1anclem4  35616  ftc1anclem5  35617  ftc1anclem6  35618  ftc1anclem7  35619  ftc1anclem8  35620  ftc1anc  35621  ftc2nc  35622  areacirclem1  35628  areacirclem5  35632  areacirc  35633  isbnd3  35705  blbnd  35708  prdsbnd  35714  prdsbnd2  35716  cntotbnd  35717  dvrelog3  39832  0nonelalab  39834  dvrelogpow2b  39835  dvle2  39839  aks4d1p1p6  39840  aks4d1p1p5  39842  idomrootle  40751  idomodle  40752  imo72b2  41489  cvgdvgrat  41632  radcnvrat  41633  rfcnpre3  42277  rfcnpre4  42278  nnxrd  42286  absfico  42459  lefldiveq  42532  lttri5d  42539  supxrgere  42573  supxrgelem  42577  supxrge  42578  xralrple2  42594  infxr  42607  infleinflem1  42610  infleinflem2  42611  xralrple4  42613  xralrple3  42614  xrralrecnnle  42623  xrralrecnnge  42631  supxrunb3  42640  unb2ltle  42656  zxrd  42696  gtnelioc  42732  ltnelicc  42738  iooabslt  42740  gtnelicc  42741  eliooshift  42747  iocopn  42761  eliccelioc  42762  iooshift  42763  icoopn  42766  ge0lere  42773  iooiinicc  42783  sqrlearg  42794  iooiinioc  42797  uzinico  42801  preimaiocmnf  42802  uzubioo  42808  fsumge0cl  42817  limciccioolb  42865  lptioo1  42876  limcicciooub  42881  ltmod  42882  lptre2pt  42884  limsupre  42885  limcresiooub  42886  limcresioolb  42887  limcleqr  42888  limsupresico  42944  limsuppnfdlem  42945  limsupub  42948  limsupequzlem  42966  limsupre2lem  42968  limsupre3lem  42976  limsupvaluz2  42982  supcnvlimsup  42984  liminfresico  43015  limsup10exlem  43016  liminflelimsuplem  43019  limsupgtlem  43021  liminfval4  43033  liminfvaluz2  43039  limsupvaluz4  43044  liminflimsupclim  43051  xlimxrre  43075  xlimmnfvlem1  43076  xlimmnfv  43078  xlimpnfvlem1  43080  xlimpnfv  43082  sinaover2ne0  43112  ioccncflimc  43129  icccncfext  43131  icocncflimc  43133  cncfiooicclem1  43137  cncfiooicc  43138  cncfiooiccre  43139  cncfioobdlem  43140  dvbdfbdioolem1  43172  dvbdfbdioolem2  43173  dvbdfbdioo  43174  ioodvbdlimc1lem1  43175  ioodvbdlimc1lem2  43176  ioodvbdlimc1  43177  ioodvbdlimc2lem  43178  ioodvbdlimc2  43179  ditgeqiooicc  43204  iblsplit  43210  itgcoscmulx  43213  ibliooicc  43215  iblspltprt  43217  itgsincmulx  43218  itgsubsticc  43220  itgioocnicc  43221  iblcncfioo  43222  itgspltprt  43223  itgiccshift  43224  volioore  43234  voliooico  43236  voliooicof  43240  voliccico  43243  stoweidlem34  43278  stoweidlem52  43296  stirlinglem5  43322  dirkercncflem1  43347  dirkercncflem4  43350  fourierdlem4  43355  fourierdlem10  43361  fourierdlem19  43370  fourierdlem20  43371  fourierdlem24  43375  fourierdlem25  43376  fourierdlem26  43377  fourierdlem27  43378  fourierdlem28  43379  fourierdlem31  43382  fourierdlem32  43383  fourierdlem33  43384  fourierdlem35  43386  fourierdlem37  43388  fourierdlem40  43391  fourierdlem41  43392  fourierdlem43  43394  fourierdlem44  43395  fourierdlem46  43396  fourierdlem47  43397  fourierdlem48  43398  fourierdlem49  43399  fourierdlem50  43400  fourierdlem51  43401  fourierdlem52  43402  fourierdlem54  43404  fourierdlem57  43407  fourierdlem59  43409  fourierdlem60  43410  fourierdlem61  43411  fourierdlem62  43412  fourierdlem63  43413  fourierdlem64  43414  fourierdlem65  43415  fourierdlem68  43418  fourierdlem69  43419  fourierdlem70  43420  fourierdlem72  43422  fourierdlem73  43423  fourierdlem74  43424  fourierdlem75  43425  fourierdlem76  43426  fourierdlem78  43428  fourierdlem79  43429  fourierdlem81  43431  fourierdlem82  43432  fourierdlem84  43434  fourierdlem89  43439  fourierdlem90  43440  fourierdlem91  43441  fourierdlem92  43442  fourierdlem93  43443  fourierdlem94  43444  fourierdlem97  43447  fourierdlem100  43450  fourierdlem101  43451  fourierdlem102  43452  fourierdlem103  43453  fourierdlem104  43454  fourierdlem107  43457  fourierdlem109  43459  fourierdlem111  43461  fourierdlem112  43462  fourierdlem113  43463  fourierdlem114  43464  sqwvfoura  43472  fouriersw  43475  etransclem23  43501  etransclem46  43524  qndenserrnbllem  43538  rrxsnicc  43544  ioorrnopnlem  43548  ioorrnopnxrlem  43550  salgencntex  43585  sge0cl  43622  sge0fsum  43628  sge0iunmptlemre  43656  sge0isum  43668  sge0ad2en  43672  sge0xaddlem1  43674  sge0xaddlem2  43675  sge0reuz  43688  voliunsge0lem  43713  meassre  43718  omessre  43751  omeiunltfirp  43760  hoissre  43785  hoiprodcl  43788  ovnsubaddlem1  43811  hoiprodcl3  43821  hoidmvcl  43823  hsphoidmvle2  43826  hsphoidmvle  43827  sge0hsphoire  43830  hoidmv1lelem1  43832  hoidmv1lelem2  43833  hoidmv1lelem3  43834  hoidmv1le  43835  hoidmvlelem1  43836  hoidmvlelem2  43837  hoidmvlelem3  43838  hoidmvlelem4  43839  ovnhoilem1  43842  ovnhoilem2  43843  ovnhoi  43844  ovnlecvr2  43851  hspdifhsp  43857  hoidifhspdmvle  43861  hoiqssbllem1  43863  hoiqssbllem2  43864  hoiqssbllem3  43865  hspmbllem1  43867  hspmbllem2  43868  volicorege0  43878  ovolval5lem1  43893  ovolval5lem2  43894  iinhoiicclem  43914  iinhoiicc  43915  iunhoiioolem  43916  iunhoiioo  43917  vonioolem2  43922  vonicclem2  43925  vonsn  43932  pimltmnf2  43938  pimconstlt0  43941  pimgtpnf2  43944  salpreimagelt  43945  salpreimalegt  43947  preimageiingt  43957  preimaleiinlt  43958  pimrecltneg  43960  issmflem  43963  issmflelem  43980  issmfgtlem  43991  issmfgt  43992  smfaddlem1  43998  issmfgelem  44004  issmfge  44005  smfpimioompt  44020  smfresal  44022  smfrec  44023  smfmullem1  44025  smfmullem2  44026  smfmullem3  44027  smfmullem4  44028  smfpimbor1lem1  44032  smfsuplem1  44044  smflimsuplem4  44056  smfliminflem  44063  bgoldbtbnd  44962  eenglngeehlnmlem2  45785
  Copyright terms: Public domain W3C validator