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

Theorem rexrd 11206
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 11200 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sselid 3943 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  *cxr 11189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-un 3916  df-in 3918  df-ss 3928  df-xr 11194
This theorem is referenced by:  xnn0xr  12491  rpxr  12925  rpxrd  12959  max0sub  13116  qextltlem  13122  xralrple  13125  xnegcl  13133  xaddf  13144  xnn0lem1lt  13164  xnn0lenn0nn0  13165  xmulf  13192  xadddi  13215  xrub  13232  supxrre  13247  infxrre  13256  ixxub  13286  ixxlb  13287  ioo0  13290  ico0  13311  ioc0  13312  iooshf  13344  icoshftf1o  13392  supicc  13419  supiccub  13420  supicclub  13421  xnn0xrge0  13424  ssfzunsn  13488  addmodid  13825  hashnnn0genn0  14244  hashunsnggt  14295  elicc4abs  15205  caucvgrlem  15558  fprodge1  15879  pcxcl  16734  pcdvdsb  16742  pcaddlem  16761  ramcl2lem  16882  ramlb  16892  0ram  16893  setsstruct  17049  prdsxmetlem  23724  xblss2ps  23757  xblss2  23758  blss2ps  23759  blss2  23760  blhalf  23761  metustto  23912  metustexhalf  23915  nmoi  24095  nmoix  24096  nmoi2  24097  nmoleub  24098  qdensere  24136  cnblcld  24141  ioo2blex  24160  tgioo  24162  blcvx  24164  zcld  24179  recld2  24180  iccntr  24187  icccmplem1  24188  reconnlem1  24192  reconnlem2  24193  opnreen  24197  metnrmlem3  24227  icoopnst  24305  iocopnst  24306  cnheibor  24321  lebnumii  24332  nmoleub2lem  24480  lmnn  24630  iscau3  24645  minveclem4  24799  ivthlem1  24818  ivthlem2  24819  ivthlem3  24820  ivth2  24822  ivthle  24823  ivthle2  24824  ivthicc  24825  evthicc  24826  cniccbdd  24828  ovolgelb  24847  ovollb2lem  24855  ovolunlem1  24864  ovoliunlem1  24869  ovoliunlem2  24870  ovoliun  24872  ovolscalem1  24880  ovolicc1  24883  ovolicc2lem4  24887  ovolicc2lem5  24888  ovolicc2  24889  ovolicc  24890  nulmbl2  24903  voliunlem2  24918  ioombl1lem4  24928  ioorcl2  24939  uniioombllem1  24948  uniioombllem2a  24949  uniioombllem3  24952  dyaddisjlem  24962  dyadmaxlem  24964  opnmbllem  24968  volivth  24974  vitalilem4  24978  mbfmulc2lem  25014  mbfmax  25016  mbfposr  25019  ismbf3d  25021  mbfaddlem  25027  mbflimsup  25033  mbfi1fseqlem4  25086  itg2lcl  25095  xrge0f  25099  itg2itg1  25104  itg2const2  25109  itg2seq  25110  itg2uba  25111  itg2lea  25112  itg2mulclem  25114  itg2mulc  25115  itg2splitlem  25116  itg2split  25117  itg2monolem2  25119  itg2monolem3  25120  itg2mono  25121  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  itg2cn  25131  iblss  25172  itgle  25177  itgeqa  25181  itgioo  25183  ibladdlem  25187  iblabs  25196  iblabsr  25197  iblmulc2  25198  itgsplit  25203  itgspliticc  25204  itgsplitioo  25205  bddmulibl  25206  bddiblnc  25209  ditgcl  25225  ditgswap  25226  ditgsplitlem  25227  dvferm1lem  25351  dvferm2lem  25353  dvferm  25355  rollelem  25356  rolle  25357  cmvth  25358  mvth  25359  dvlip  25360  dvlip2  25362  c1liplem1  25363  c1lip1  25364  dveq0  25367  dvgt0lem1  25369  dvivthlem1  25375  dvivth  25377  lhop1lem  25380  lhop1  25381  lhop2  25382  lhop  25383  dvcnvrelem1  25384  dvcnvre  25386  dvcvx  25387  dvfsumle  25388  dvfsumge  25389  dvfsumabs  25390  dvfsumlem2  25394  dvfsumlem3  25395  dvfsumlem4  25396  dvfsumrlimge0  25397  dvfsumrlim2  25399  ftc1lem1  25402  ftc1lem2  25403  ftc1a  25404  ftc1lem4  25406  ftc2  25411  ftc2ditglem  25412  itgparts  25414  itgsubstlem  25415  itgsubst  25416  itgpowd  25417  degltlem1  25440  deg1ge  25466  coe1mul3  25467  deg1sublt  25478  deg1mul2  25482  deg1tmle  25485  deg1tm  25486  plypf1  25576  taylfvallem1  25719  tayl0  25724  pserulm  25784  psercnlem1  25787  pserdvlem1  25789  pserdvlem2  25790  abelthlem3  25795  abelth  25803  efcvx  25811  logno1  25994  logtayl  26018  xrlimcnp  26321  logfacbnd3  26574  log2sumbnd  26895  pntpbnd2  26938  pntibndlem3  26943  ttgcontlem1  27836  nmooge0  29712  nmoub3i  29718  isblo3i  29746  ubthlem1  29815  minvecolem4  29825  nmopge0  30856  nmfnge0  30872  nmophmi  30976  branmfn  31050  xaddeq0  31661  xlt2addrd  31666  xmulcand  31780  xreceu  31781  xdivrec  31786  fsumrp0cl  31889  xrge0slmod  32143  cnre2csqlem  32494  tpr2rico  32496  xrge0iifcnv  32517  xrge0iifhom  32521  lmxrge0  32536  esumfsup  32672  esumpcvgval  32680  esumcvg  32688  dya2iocress  32877  dya2iocbrsiga  32878  dya2icobrsiga  32879  dya2icoseg  32880  dya2iocucvr  32887  sxbrsigalem2  32889  omssubaddlem  32902  omssubadd  32903  orvcgteel  33070  dstrvprob  33074  orvclteel  33075  sgnmul  33145  sgnsub  33147  sgnmulsgn  33152  sgnmulsgp  33153  signstcl  33180  signstf  33181  signstf0  33183  signstfvn  33184  signsvtn0  33185  signsvfn  33197  signsvfpn  33200  signsvfnn  33201  ftc2re  33214  cvmliftlem6  33887  cvmliftlem7  33888  cvmliftlem8  33889  cvmliftlem9  33890  cvmliftlem10  33891  cvmliftlem13  33893  ivthALT  34810  iooelexlt  35836  relowlssretop  35837  relowlpssretop  35838  sin2h  36071  cos2h  36072  tan2h  36073  poimirlem30  36111  poimir  36114  heicant  36116  opnmbllem0  36117  mblfinlem1  36118  mblfinlem2  36119  mblfinlem3  36120  mblfinlem4  36121  ismblfin  36122  itg2addnclem  36132  itg2addnclem2  36133  itg2gt0cn  36136  ibladdnclem  36137  iblabsnclem  36144  iblabsnc  36145  iblmulc2nc  36146  ftc1cnnclem  36152  ftc1anclem1  36154  ftc1anclem4  36157  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  ftc2nc  36163  areacirclem1  36169  areacirclem5  36173  areacirc  36174  isbnd3  36246  blbnd  36249  prdsbnd  36255  prdsbnd2  36257  cntotbnd  36258  dvrelog3  40525  0nonelalab  40527  dvrelogpow2b  40528  dvle2  40532  aks4d1p1p6  40533  aks4d1p1p5  40535  idomrootle  41525  idomodle  41526  imo72b2  42452  cvgdvgrat  42600  radcnvrat  42601  rfcnpre3  43245  rfcnpre4  43246  absfico  43446  nnxrd  43514  lefldiveq  43533  lttri5d  43540  supxrgere  43574  supxrgelem  43578  supxrge  43579  xralrple2  43595  infxr  43608  infleinflem1  43611  infleinflem2  43612  xralrple4  43614  xralrple3  43615  xrralrecnnle  43624  xrralrecnnge  43632  supxrunb3  43641  unb2ltle  43657  zxrd  43695  gtnelioc  43736  ltnelicc  43742  iooabslt  43744  gtnelicc  43745  eliooshift  43751  iocopn  43765  eliccelioc  43766  iooshift  43767  icoopn  43770  ge0lere  43777  iooiinicc  43787  sqrlearg  43798  iooiinioc  43801  uzinico  43805  preimaiocmnf  43806  uzubioo  43812  fsumge0cl  43821  limciccioolb  43869  lptioo1  43880  limcicciooub  43885  ltmod  43886  lptre2pt  43888  limsupre  43889  limcresiooub  43890  limcresioolb  43891  limcleqr  43892  limsupresico  43948  limsuppnfdlem  43949  limsupub  43952  limsupequzlem  43970  limsupre2lem  43972  limsupre3lem  43980  limsupvaluz2  43986  supcnvlimsup  43988  liminfresico  44019  limsup10exlem  44020  liminflelimsuplem  44023  limsupgtlem  44025  liminfval4  44037  liminfvaluz2  44043  limsupvaluz4  44048  liminflimsupclim  44055  xlimxrre  44079  xlimmnfvlem1  44080  xlimmnfv  44082  xlimpnfvlem1  44084  xlimpnfv  44086  sinaover2ne0  44116  ioccncflimc  44133  icccncfext  44135  icocncflimc  44137  cncfiooicclem1  44141  cncfiooicc  44142  cncfiooiccre  44143  cncfioobdlem  44144  dvbdfbdioolem1  44176  dvbdfbdioolem2  44177  dvbdfbdioo  44178  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc1  44181  ioodvbdlimc2lem  44182  ioodvbdlimc2  44183  ditgeqiooicc  44208  iblsplit  44214  itgcoscmulx  44217  ibliooicc  44219  iblspltprt  44221  itgsincmulx  44222  itgsubsticc  44224  itgioocnicc  44225  iblcncfioo  44226  itgspltprt  44227  itgiccshift  44228  volioore  44238  voliooico  44240  voliooicof  44244  voliccico  44247  stoweidlem34  44282  stoweidlem52  44300  stirlinglem5  44326  dirkercncflem1  44351  dirkercncflem4  44354  fourierdlem4  44359  fourierdlem10  44365  fourierdlem19  44374  fourierdlem20  44375  fourierdlem24  44379  fourierdlem25  44380  fourierdlem26  44381  fourierdlem27  44382  fourierdlem28  44383  fourierdlem31  44386  fourierdlem32  44387  fourierdlem33  44388  fourierdlem35  44390  fourierdlem37  44392  fourierdlem40  44395  fourierdlem41  44396  fourierdlem43  44398  fourierdlem44  44399  fourierdlem46  44400  fourierdlem47  44401  fourierdlem48  44402  fourierdlem49  44403  fourierdlem50  44404  fourierdlem51  44405  fourierdlem52  44406  fourierdlem54  44408  fourierdlem57  44411  fourierdlem59  44413  fourierdlem60  44414  fourierdlem61  44415  fourierdlem62  44416  fourierdlem63  44417  fourierdlem64  44418  fourierdlem65  44419  fourierdlem68  44422  fourierdlem69  44423  fourierdlem70  44424  fourierdlem72  44426  fourierdlem73  44427  fourierdlem74  44428  fourierdlem75  44429  fourierdlem76  44430  fourierdlem78  44432  fourierdlem79  44433  fourierdlem81  44435  fourierdlem82  44436  fourierdlem84  44438  fourierdlem89  44443  fourierdlem90  44444  fourierdlem91  44445  fourierdlem92  44446  fourierdlem93  44447  fourierdlem94  44448  fourierdlem97  44451  fourierdlem100  44454  fourierdlem101  44455  fourierdlem102  44456  fourierdlem103  44457  fourierdlem104  44458  fourierdlem107  44461  fourierdlem109  44463  fourierdlem111  44465  fourierdlem112  44466  fourierdlem113  44467  fourierdlem114  44468  sqwvfoura  44476  fouriersw  44479  etransclem23  44505  etransclem46  44528  qndenserrnbllem  44542  rrxsnicc  44548  ioorrnopnlem  44552  ioorrnopnxrlem  44554  salgencntex  44591  sge0cl  44629  sge0fsum  44635  sge0iunmptlemre  44663  sge0isum  44675  sge0ad2en  44679  sge0xaddlem1  44681  sge0xaddlem2  44682  sge0reuz  44695  voliunsge0lem  44720  meassre  44725  omessre  44758  omeiunltfirp  44767  hoissre  44792  hoiprodcl  44795  ovnsubaddlem1  44818  hoiprodcl3  44828  hoidmvcl  44830  hsphoidmvle2  44833  hsphoidmvle  44834  sge0hsphoire  44837  hoidmv1lelem1  44839  hoidmv1lelem2  44840  hoidmv1lelem3  44841  hoidmv1le  44842  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem4  44846  ovnhoilem1  44849  ovnhoilem2  44850  ovnhoi  44851  ovnlecvr2  44858  hspdifhsp  44864  hoidifhspdmvle  44868  hoiqssbllem1  44870  hoiqssbllem2  44871  hoiqssbllem3  44872  hspmbllem1  44874  hspmbllem2  44875  volicorege0  44885  ovolval5lem1  44900  ovolval5lem2  44901  iinhoiicclem  44921  iinhoiicc  44922  iunhoiioolem  44923  iunhoiioo  44924  vonioolem2  44929  vonicclem2  44932  vonsn  44939  pimltmnf2f  44945  pimconstlt0  44949  pimgtpnf2f  44953  salpreimagelt  44955  salpreimalegt  44957  preimageiingt  44968  preimaleiinlt  44969  pimrecltneg  44972  issmflem  44975  issmflelem  44992  issmfgtlem  45003  issmfgt  45004  smfaddlem1  45011  issmfgelem  45017  issmfge  45018  smfpimioompt  45034  smfresal  45036  smfrec  45037  smfmullem1  45039  smfmullem2  45040  smfmullem3  45041  smfmullem4  45042  smfpimbor1lem1  45046  smfsuplem1  45059  smflimsuplem4  45071  smfliminflem  45078  smfdmmblpimne  45085  smfpimne  45087  smfpimne2  45088  fsupdm  45090  finfdm  45094  smfinfdmmbllem  45096  bgoldbtbnd  46008  eenglngeehlnmlem2  46831
  Copyright terms: Public domain W3C validator