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

Theorem rexrd 10347
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 10341 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sseldi 3761 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  cr 10192  *cxr 10331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739  df-in 3741  df-ss 3748  df-xr 10336
This theorem is referenced by:  xnn0xr  11619  rpxr  12044  rpxrd  12076  max0sub  12234  qextltlem  12240  xralrple  12243  xnegcl  12251  xaddf  12262  xnn0lenn0nn0  12282  xmulf  12309  xadddi  12332  supxrre  12364  infxrre  12373  ixxub  12403  ixxlb  12404  ioo0  12407  ico0  12428  ioc0  12429  iooshf  12459  icoshftf1o  12505  supicc  12532  supiccub  12533  supicclub  12534  xnn0xrge0  12537  ssfzunsn  12599  addmodid  12931  hashnnn0genn0  13340  elicc4abs  14358  caucvgrlem  14702  fprodge1  15022  pcxcl  15858  pcdvdsb  15866  pcaddlem  15885  ramcl2lem  16006  ramlb  16016  0ram  16017  setsstruct  16185  prdsxmetlem  22466  xblss2ps  22499  xblss2  22500  blss2ps  22501  blss2  22502  blhalf  22503  metustto  22651  metustexhalf  22654  nmoi  22825  nmoix  22826  nmoi2  22827  nmoleub  22828  qdensere  22866  cnblcld  22871  ioo2blex  22890  tgioo  22892  blcvx  22894  zcld  22909  recld2  22910  iccntr  22917  icccmplem1  22918  reconnlem1  22922  reconnlem2  22923  opnreen  22927  metnrmlem3  22957  icoopnst  23031  cnheibor  23047  lebnumii  23058  nmoleub2lem  23206  lmnn  23354  iscau3  23369  minveclem4  23506  ivthlem1  23523  ivthlem2  23524  ivthlem3  23525  ivth2  23527  ivthle  23528  ivthle2  23529  ivthicc  23530  evthicc  23531  cniccbdd  23533  ovolgelb  23552  ovollb2lem  23560  ovolunlem1  23569  ovoliunlem1  23574  ovoliunlem2  23575  ovoliun  23577  ovolscalem1  23585  ovolicc1  23588  ovolicc2lem4  23592  ovolicc2lem5  23593  ovolicc2  23594  ovolicc  23595  nulmbl2  23608  voliunlem2  23623  ioombl1lem4  23633  ioorcl2  23644  uniioombllem1  23653  uniioombllem2a  23654  uniioombllem3  23657  dyaddisjlem  23667  dyadmaxlem  23669  opnmbllem  23673  volivth  23679  vitalilem4  23683  mbfmulc2lem  23719  mbfmax  23721  mbfposr  23724  ismbf3d  23726  mbfaddlem  23732  mbflimsup  23738  mbfi1fseqlem4  23790  itg2lcl  23799  xrge0f  23803  itg2itg1  23808  itg2const2  23813  itg2seq  23814  itg2uba  23815  itg2lea  23816  itg2mulclem  23818  itg2mulc  23819  itg2splitlem  23820  itg2split  23821  itg2monolem2  23823  itg2monolem3  23824  itg2mono  23825  itg2gt0  23832  itg2cnlem1  23833  itg2cnlem2  23834  itg2cn  23835  iblss  23876  itgle  23881  itgeqa  23885  itgioo  23887  ibladdlem  23891  iblabs  23900  iblabsr  23901  iblmulc2  23902  itgsplit  23907  itgspliticc  23908  itgsplitioo  23909  bddmulibl  23910  ditgcl  23927  ditgswap  23928  ditgsplitlem  23929  dvferm1lem  24052  dvferm2lem  24054  dvferm  24056  rollelem  24057  rolle  24058  cmvth  24059  mvth  24060  dvlip  24061  dvlip2  24063  c1liplem1  24064  c1lip1  24065  dveq0  24068  dvgt0lem1  24070  dvivthlem1  24076  dvivth  24078  lhop1lem  24081  lhop1  24082  lhop2  24083  lhop  24084  dvcnvrelem1  24085  dvcnvre  24087  dvcvx  24088  dvfsumle  24089  dvfsumge  24090  dvfsumabs  24091  dvfsumlem2  24095  dvfsumlem3  24096  dvfsumlem4  24097  dvfsumrlimge0  24098  dvfsumrlim2  24100  ftc1lem1  24103  ftc1lem2  24104  ftc1a  24105  ftc1lem4  24107  ftc2  24112  ftc2ditglem  24113  itgparts  24115  itgsubstlem  24116  itgsubst  24117  degltlem1  24137  deg1ge  24163  coe1mul3  24164  deg1sublt  24175  deg1mul2  24179  deg1tmle  24182  deg1tm  24183  plypf1  24273  taylfvallem1  24416  tayl0  24421  pserulm  24481  psercnlem1  24484  pserdvlem1  24486  pserdvlem2  24487  abelthlem3  24492  abelth  24500  efcvx  24508  logno1  24687  logtayl  24711  xrlimcnp  25000  logfacbnd3  25253  log2sumbnd  25538  pntpbnd2  25581  pntibndlem3  25586  ttgcontlem1  26070  nmooge0  28099  nmoub3i  28105  isblo3i  28133  ubthlem1  28203  minvecolem4  28213  nmopge0  29247  nmfnge0  29263  nmophmi  29367  branmfn  29441  xaddeq0  29988  xlt2addrd  29993  xmulcand  30097  xreceu  30098  xdivrec  30103  fsumrp0cl  30163  xrge0slmod  30312  cnre2csqlem  30424  tpr2rico  30426  xrge0iifcnv  30447  xrge0iifhom  30451  lmxrge0  30466  esumfsup  30600  esumpcvgval  30608  esumcvg  30616  dya2iocress  30804  dya2iocbrsiga  30805  dya2icobrsiga  30806  dya2icoseg  30807  dya2iocucvr  30814  sxbrsigalem2  30816  omssubaddlem  30829  omssubadd  30830  orvcgteel  30998  dstrvprob  31002  orvclteel  31003  sgnmul  31073  sgnsub  31075  sgnmulsgn  31080  sgnmulsgp  31081  signstcl  31112  signstf  31113  signstf0  31115  signstfvn  31116  signsvtn0  31117  signsvtn0OLD  31118  signstfvneq0  31120  signsvfn  31131  signsvfpn  31134  signsvfnn  31135  ftc2re  31148  cvmliftlem6  31741  cvmliftlem7  31742  cvmliftlem8  31743  cvmliftlem9  31744  cvmliftlem10  31745  cvmliftlem13  31747  ivthALT  32794  iooelexlt  33664  relowlssretop  33665  relowlpssretop  33666  sin2h  33844  cos2h  33845  tan2h  33846  poimirlem30  33884  poimir  33887  heicant  33889  opnmbllem0  33890  mblfinlem1  33891  mblfinlem2  33892  mblfinlem3  33893  mblfinlem4  33894  ismblfin  33895  itg2addnclem  33905  itg2addnclem2  33906  itg2gt0cn  33909  ibladdnclem  33910  iblabsnclem  33917  iblabsnc  33918  iblmulc2nc  33919  bddiblnc  33924  ftc1cnnclem  33927  ftc1anclem1  33929  ftc1anclem4  33932  ftc1anclem5  33933  ftc1anclem6  33934  ftc1anclem7  33935  ftc1anclem8  33936  ftc1anc  33937  ftc2nc  33938  areacirclem1  33944  areacirclem5  33948  areacirc  33949  isbnd3  34026  blbnd  34029  prdsbnd  34035  prdsbnd2  34037  cntotbnd  34038  idomrootle  38474  idomodle  38475  itgpowd  38500  imo72b2  39173  cvgdvgrat  39210  radcnvrat  39211  rfcnpre3  39868  rfcnpre4  39869  nnxrd  39877  absfico  40079  lefldiveq  40169  lttri5d  40176  supxrgere  40211  supxrgelem  40215  supxrge  40216  xralrple2  40232  infxr  40245  infleinflem1  40248  infleinflem2  40249  xralrple4  40251  xralrple3  40252  xrralrecnnle  40264  xrralrecnnge  40274  supxrunb3  40284  unb2ltle  40303  zxrd  40343  gtnelioc  40378  ltnelicc  40385  iooabslt  40387  gtnelicc  40388  eliooshift  40395  iocopn  40409  eliccelioc  40410  iooshift  40411  icoopn  40414  ge0lere  40421  iooiinicc  40431  sqrlearg  40442  iooiinioc  40445  uzinico  40449  preimaiocmnf  40450  uzubioo  40456  fsumge0cl  40467  limciccioolb  40515  lptioo1  40526  limcicciooub  40531  ltmod  40532  lptre2pt  40534  limsupre  40535  limcresiooub  40536  limcresioolb  40537  limcleqr  40538  limsupresico  40594  limsuppnfdlem  40595  limsupub  40598  limsupequzlem  40616  limsupre2lem  40618  limsupre3lem  40626  limsupvaluz2  40632  supcnvlimsup  40634  liminfresico  40665  limsup10exlem  40666  liminflelimsuplem  40669  limsupgtlem  40671  liminfval4  40683  liminfvaluz2  40689  limsupvaluz4  40694  liminflimsupclim  40701  xlimxrre  40719  xlimmnfvlem1  40720  xlimmnfv  40722  xlimpnfvlem1  40724  xlimpnfv  40726  sinaover2ne0  40741  ioccncflimc  40760  icccncfext  40762  icocncflimc  40764  cncfiooicclem1  40768  cncfiooicc  40769  cncfiooiccre  40770  cncfioobdlem  40771  dvbdfbdioolem1  40805  dvbdfbdioolem2  40806  dvbdfbdioo  40807  ioodvbdlimc1lem1  40808  ioodvbdlimc1lem2  40809  ioodvbdlimc1  40810  ioodvbdlimc2lem  40811  ioodvbdlimc2  40812  ditgeqiooicc  40837  iblsplit  40843  itgcoscmulx  40846  ibliooicc  40848  iblspltprt  40850  itgsincmulx  40851  itgsubsticc  40853  itgioocnicc  40854  iblcncfioo  40855  itgspltprt  40856  itgiccshift  40857  volioore  40868  voliooico  40870  voliooicof  40874  voliccico  40877  stoweidlem34  40912  stoweidlem52  40930  stirlinglem5  40956  dirkercncflem1  40981  dirkercncflem4  40984  fourierdlem4  40989  fourierdlem10  40995  fourierdlem19  41004  fourierdlem20  41005  fourierdlem24  41009  fourierdlem25  41010  fourierdlem26  41011  fourierdlem27  41012  fourierdlem28  41013  fourierdlem31  41016  fourierdlem32  41017  fourierdlem33  41018  fourierdlem35  41020  fourierdlem37  41022  fourierdlem40  41025  fourierdlem41  41026  fourierdlem43  41028  fourierdlem44  41029  fourierdlem46  41030  fourierdlem47  41031  fourierdlem48  41032  fourierdlem49  41033  fourierdlem50  41034  fourierdlem51  41035  fourierdlem52  41036  fourierdlem54  41038  fourierdlem57  41041  fourierdlem59  41043  fourierdlem60  41044  fourierdlem61  41045  fourierdlem62  41046  fourierdlem63  41047  fourierdlem64  41048  fourierdlem65  41049  fourierdlem68  41052  fourierdlem69  41053  fourierdlem70  41054  fourierdlem72  41056  fourierdlem73  41057  fourierdlem74  41058  fourierdlem75  41059  fourierdlem76  41060  fourierdlem78  41062  fourierdlem79  41063  fourierdlem81  41065  fourierdlem82  41066  fourierdlem84  41068  fourierdlem89  41073  fourierdlem90  41074  fourierdlem91  41075  fourierdlem92  41076  fourierdlem93  41077  fourierdlem94  41078  fourierdlem97  41081  fourierdlem100  41084  fourierdlem101  41085  fourierdlem102  41086  fourierdlem103  41087  fourierdlem104  41088  fourierdlem107  41091  fourierdlem109  41093  fourierdlem111  41095  fourierdlem112  41096  fourierdlem113  41097  fourierdlem114  41098  sqwvfoura  41106  fouriersw  41109  etransclem23  41135  etransclem46  41158  qndenserrnbllem  41175  rrxsnicc  41181  ioorrnopnlem  41185  ioorrnopnxrlem  41187  salgencntex  41222  sge0cl  41259  sge0fsum  41265  sge0iunmptlemre  41293  sge0isum  41305  sge0ad2en  41309  sge0xaddlem1  41311  sge0xaddlem2  41312  sge0reuz  41325  voliunsge0lem  41350  meassre  41355  omessre  41388  omeiunltfirp  41397  hoissre  41422  hoiprodcl  41425  ovnsubaddlem1  41448  hoiprodcl3  41458  hoidmvcl  41460  hsphoidmvle2  41463  hsphoidmvle  41464  sge0hsphoire  41467  hoidmv1lelem1  41469  hoidmv1lelem2  41470  hoidmv1lelem3  41471  hoidmv1le  41472  hoidmvlelem1  41473  hoidmvlelem2  41474  hoidmvlelem3  41475  hoidmvlelem4  41476  ovnhoilem1  41479  ovnhoilem2  41480  ovnhoi  41481  ovnlecvr2  41488  hspdifhsp  41494  hoidifhspdmvle  41498  hoiqssbllem1  41500  hoiqssbllem2  41501  hoiqssbllem3  41502  hspmbllem1  41504  hspmbllem2  41505  volicorege0  41515  ovolval5lem1  41530  ovolval5lem2  41531  iinhoiicclem  41551  iinhoiicc  41552  iunhoiioolem  41553  iunhoiioo  41554  vonioolem2  41559  vonicclem2  41562  vonsn  41569  pimltmnf2  41575  pimconstlt0  41578  pimgtpnf2  41581  salpreimagelt  41582  salpreimalegt  41584  preimageiingt  41594  preimaleiinlt  41595  pimrecltneg  41597  issmflem  41600  issmflelem  41617  issmfgtlem  41628  issmfgt  41629  smfaddlem1  41635  issmfgelem  41641  issmfge  41642  smfpimioompt  41657  smfresal  41659  smfrec  41660  smfmullem1  41662  smfmullem2  41663  smfmullem3  41664  smfmullem4  41665  smfpimbor1lem1  41669  smfsuplem1  41681  smflimsuplem4  41693  smfliminflem  41700  bgoldbtbnd  42397
  Copyright terms: Public domain W3C validator