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

Theorem rexrd 10127
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 10121 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sseldi 3634 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cr 9973  *cxr 10111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-xr 10116
This theorem is referenced by:  xnn0xr  11406  rpxr  11878  rpxrd  11911  max0sub  12065  qextltlem  12071  xralrple  12074  xnegcl  12082  xaddf  12093  xnn0lenn0nn0  12113  xmulf  12140  xadddi  12163  supxrre  12195  infxrre  12204  ixxub  12234  ixxlb  12235  ioo0  12238  ico0  12259  ioc0  12260  iooshf  12290  icoshftf1o  12333  supicc  12358  supiccub  12359  supicclub  12360  xnn0xrge0  12363  ssfzunsn  12425  addmodid  12758  hashnnn0genn0  13171  elicc4abs  14103  caucvgrlem  14447  fprodge1  14770  pcxcl  15612  pcdvdsb  15620  pcaddlem  15639  ramcl2lem  15760  ramlb  15770  0ram  15771  setsstruct  15945  prdsxmetlem  22220  xblss2ps  22253  xblss2  22254  blss2ps  22255  blss2  22256  blhalf  22257  metustto  22405  metustexhalf  22408  nmoi  22579  nmoix  22580  nmoi2  22581  nmoleub  22582  qdensere  22620  cnblcld  22625  ioo2blex  22644  tgioo  22646  blcvx  22648  zcld  22663  recld2  22664  iccntr  22671  icccmplem1  22672  reconnlem1  22676  reconnlem2  22677  opnreen  22681  metnrmlem3  22711  icoopnst  22785  cnheibor  22801  lebnumii  22812  nmoleub2lem  22960  lmnn  23107  iscau3  23122  minveclem4  23249  ivthlem1  23266  ivthlem2  23267  ivthlem3  23268  ivth2  23270  ivthle  23271  ivthle2  23272  ivthicc  23273  evthicc  23274  cniccbdd  23276  ovolgelb  23294  ovollb2lem  23302  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovoliun  23319  ovolscalem1  23327  ovolicc1  23330  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicc2  23336  ovolicc  23337  nulmbl2  23350  voliunlem2  23365  ioombl1lem4  23375  ioorcl2  23386  uniioombllem1  23395  uniioombllem2a  23396  uniioombllem3  23399  dyaddisjlem  23409  dyadmaxlem  23411  opnmbllem  23415  volivth  23421  vitalilem4  23425  mbfmulc2lem  23459  mbfmax  23461  mbfposr  23464  ismbf3d  23466  mbfaddlem  23472  mbflimsup  23478  mbfi1fseqlem4  23530  itg2lcl  23539  xrge0f  23543  itg2itg1  23548  itg2const2  23553  itg2seq  23554  itg2uba  23555  itg2lea  23556  itg2mulclem  23558  itg2mulc  23559  itg2splitlem  23560  itg2split  23561  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  itg2cn  23575  iblss  23616  itgle  23621  itgeqa  23625  itgioo  23627  ibladdlem  23631  iblabs  23640  iblabsr  23641  iblmulc2  23642  itgsplit  23647  itgspliticc  23648  itgsplitioo  23649  bddmulibl  23650  ditgcl  23667  ditgswap  23668  ditgsplitlem  23669  dvferm1lem  23792  dvferm2lem  23794  dvferm  23796  rollelem  23797  rolle  23798  cmvth  23799  mvth  23800  dvlip  23801  dvlip2  23803  c1liplem1  23804  c1lip1  23805  dveq0  23808  dvgt0lem1  23810  dvivthlem1  23816  dvivth  23818  lhop1lem  23821  lhop1  23822  lhop2  23823  lhop  23824  dvcnvrelem1  23825  dvcnvre  23827  dvcvx  23828  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsumrlimge0  23838  dvfsumrlim2  23840  ftc1lem1  23843  ftc1lem2  23844  ftc1a  23845  ftc1lem4  23847  ftc2  23852  ftc2ditglem  23853  itgparts  23855  itgsubstlem  23856  itgsubst  23857  degltlem1  23877  deg1ge  23903  coe1mul3  23904  deg1sublt  23915  deg1mul2  23919  deg1tmle  23922  deg1tm  23923  plypf1  24013  taylfvallem1  24156  tayl0  24161  pserulm  24221  psercnlem1  24224  pserdvlem1  24226  pserdvlem2  24227  abelthlem3  24232  abelth  24240  efcvx  24248  logno1  24427  logtayl  24451  xrlimcnp  24740  logfacbnd3  24993  log2sumbnd  25278  pntpbnd2  25321  pntibndlem3  25326  ttgcontlem1  25810  nmooge0  27750  nmoub3i  27756  isblo3i  27784  ubthlem1  27854  minvecolem4  27864  nmopge0  28898  nmfnge0  28914  nmophmi  29018  branmfn  29092  xaddeq0  29646  xlt2addrd  29651  xmulcand  29757  xreceu  29758  xdivrec  29763  fsumrp0cl  29823  xrge0slmod  29972  cnre2csqlem  30084  tpr2rico  30086  xrge0iifcnv  30107  xrge0iifhom  30111  lmxrge0  30126  esumfsup  30260  esumpcvgval  30268  esumcvg  30276  dya2iocress  30464  dya2iocbrsiga  30465  dya2icobrsiga  30466  dya2icoseg  30467  dya2iocucvr  30474  sxbrsigalem2  30476  omssubaddlem  30489  omssubadd  30490  orvcgteel  30657  dstrvprob  30661  orvclteel  30662  sgnmul  30732  sgnsub  30734  sgnmulsgn  30739  sgnmulsgp  30740  signstcl  30770  signstf  30771  signstf0  30773  signstfvn  30774  signsvtn0  30775  signstfvneq0  30777  signsvfn  30787  signsvfpn  30790  signsvfnn  30791  ftc2re  30804  cvmliftlem6  31398  cvmliftlem7  31399  cvmliftlem8  31400  cvmliftlem9  31401  cvmliftlem10  31402  cvmliftlem13  31404  ivthALT  32455  iooelexlt  33340  relowlssretop  33341  relowlpssretop  33342  sin2h  33529  cos2h  33530  tan2h  33531  poimirlem30  33569  poimir  33572  heicant  33574  opnmbllem0  33575  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnclem2  33592  itg2gt0cn  33595  ibladdnclem  33596  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  bddiblnc  33610  ftc1cnnclem  33613  ftc1anclem1  33615  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  ftc2nc  33624  areacirclem1  33630  areacirclem5  33634  areacirc  33635  isbnd3  33713  blbnd  33716  prdsbnd  33722  prdsbnd2  33724  cntotbnd  33725  idomrootle  38090  idomodle  38091  itgpowd  38117  imo72b2  38792  cvgdvgrat  38829  radcnvrat  38830  rfcnpre3  39506  rfcnpre4  39507  nnxrd  39515  absfico  39724  lefldiveq  39819  lttri5d  39827  supxrgere  39862  supxrgelem  39866  supxrge  39867  xralrple2  39883  infxr  39896  infleinflem1  39899  infleinflem2  39900  xralrple4  39902  xralrple3  39903  xrralrecnnle  39915  xrralrecnnge  39926  supxrunb3  39936  unb2ltle  39955  zxrd  39995  gtnelioc  40030  ltnelicc  40037  iooabslt  40039  gtnelicc  40040  eliooshift  40047  iocopn  40064  eliccelioc  40065  iooshift  40066  icoopn  40069  ge0lere  40077  iooiinicc  40087  sqrlearg  40098  iooiinioc  40101  uzinico  40105  preimaiocmnf  40106  uzubioo  40112  fsumge0cl  40123  limciccioolb  40171  lptioo1  40182  limcicciooub  40187  ltmod  40188  lptre2pt  40190  limsupre  40191  limcresiooub  40192  limcresioolb  40193  limcleqr  40194  limsupresico  40250  limsuppnfdlem  40251  limsupub  40254  limsupequzlem  40272  limsupre2lem  40274  limsupre3lem  40282  limsupvaluz2  40288  supcnvlimsup  40290  liminfresico  40321  limsup10exlem  40322  liminflelimsuplem  40325  limsupgtlem  40327  liminfval4  40339  liminfvaluz2  40345  limsupvaluz4  40350  liminflimsupclim  40357  xlimxrre  40375  xlimmnfvlem1  40376  xlimmnfv  40378  xlimpnfvlem1  40380  xlimpnfv  40382  sinaover2ne0  40397  ioccncflimc  40416  icccncfext  40418  icocncflimc  40420  cncfiooicclem1  40424  cncfiooicc  40425  cncfiooiccre  40426  cncfioobdlem  40427  dvbdfbdioolem1  40461  dvbdfbdioolem2  40462  dvbdfbdioo  40463  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc1  40466  ioodvbdlimc2lem  40467  ioodvbdlimc2  40468  ditgeqiooicc  40494  iblsplit  40500  itgcoscmulx  40503  ibliooicc  40505  iblspltprt  40507  itgsincmulx  40508  itgsubsticc  40510  itgioocnicc  40511  iblcncfioo  40512  itgspltprt  40513  itgiccshift  40514  volioore  40525  voliooico  40527  voliooicof  40531  voliccico  40534  stoweidlem34  40569  stoweidlem52  40587  stirlinglem5  40613  dirkercncflem1  40638  dirkercncflem4  40641  fourierdlem4  40646  fourierdlem10  40652  fourierdlem19  40661  fourierdlem20  40662  fourierdlem24  40666  fourierdlem25  40667  fourierdlem26  40668  fourierdlem27  40669  fourierdlem28  40670  fourierdlem31  40673  fourierdlem32  40674  fourierdlem33  40675  fourierdlem35  40677  fourierdlem37  40679  fourierdlem40  40682  fourierdlem41  40683  fourierdlem43  40685  fourierdlem44  40686  fourierdlem46  40687  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem52  40693  fourierdlem54  40695  fourierdlem57  40698  fourierdlem59  40700  fourierdlem60  40701  fourierdlem61  40702  fourierdlem62  40703  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem68  40709  fourierdlem69  40710  fourierdlem70  40711  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem84  40725  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem93  40734  fourierdlem94  40735  fourierdlem97  40738  fourierdlem100  40741  fourierdlem101  40742  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem109  40750  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fourierdlem114  40755  sqwvfoura  40763  fouriersw  40766  etransclem23  40792  etransclem46  40815  qndenserrnbllem  40832  rrxsnicc  40838  ioorrnopnlem  40842  ioorrnopnxrlem  40844  salgencntex  40879  sge0cl  40916  sge0fsum  40922  sge0iunmptlemre  40950  sge0isum  40962  sge0ad2en  40966  sge0xaddlem1  40968  sge0xaddlem2  40969  sge0reuz  40982  voliunsge0lem  41007  meassre  41012  omessre  41045  omeiunltfirp  41054  hoissre  41079  hoiprodcl  41082  ovnsubaddlem1  41105  hoiprodcl3  41115  hoidmvcl  41117  hsphoidmvle2  41120  hsphoidmvle  41121  sge0hsphoire  41124  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  ovnhoilem1  41136  ovnhoilem2  41137  ovnhoi  41138  ovnlecvr2  41145  hspdifhsp  41151  hoidifhspdmvle  41155  hoiqssbllem1  41157  hoiqssbllem2  41158  hoiqssbllem3  41159  hspmbllem1  41161  hspmbllem2  41162  volicorege0  41172  ovolval5lem1  41187  ovolval5lem2  41188  iinhoiicclem  41208  iinhoiicc  41209  iunhoiioolem  41210  iunhoiioo  41211  vonioolem2  41216  vonicclem2  41219  vonsn  41226  pimltmnf2  41232  pimconstlt0  41235  pimgtpnf2  41238  salpreimagelt  41239  salpreimalegt  41241  preimageiingt  41251  preimaleiinlt  41252  pimrecltneg  41254  issmflem  41257  issmflelem  41274  issmfgtlem  41285  issmfgt  41286  smfaddlem1  41292  issmfgelem  41298  issmfge  41299  smfpimioompt  41314  smfresal  41316  smfrec  41317  smfmullem1  41319  smfmullem2  41320  smfmullem3  41321  smfmullem4  41322  smfpimbor1lem1  41326  smfsuplem1  41338  smflimsuplem4  41350  smfliminflem  41357  bgoldbtbnd  42022
  Copyright terms: Public domain W3C validator