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

Theorem rexrd 9942
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 9936 . 2 ℝ ⊆ ℝ*
2 rexrd.1 . 2 (𝜑𝐴 ∈ ℝ)
31, 2sseldi 3562 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cr 9788  *cxr 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-un 3541  df-in 3543  df-ss 3550  df-xr 9931
This theorem is referenced by:  rpxr  11669  rpxrd  11702  max0sub  11857  qextltlem  11863  xralrple  11866  xnegcl  11874  xaddf  11885  xmulf  11928  xadddi  11951  supxrre  11982  infxrre  11991  ixxub  12020  ixxlb  12021  ioo0  12024  ico0  12045  ioc0  12046  iooshf  12076  icoshftf1o  12119  supicc  12144  supiccub  12145  supicclub  12146  addmodid  12532  hashnnn0genn0  12942  elicc4abs  13850  caucvgrlem  14194  fprodge1  14508  pcxcl  15346  pcdvdsb  15354  pcaddlem  15373  ramcl2lem  15494  ramlb  15504  0ram  15505  prdsxmetlem  21921  xblss2ps  21954  xblss2  21955  blss2ps  21956  blss2  21957  blhalf  21958  metustto  22106  metustexhalf  22109  nmoi  22271  nmoix  22272  nmoi2  22273  nmoleub  22274  qdensere  22312  cnblcld  22317  ioo2blex  22334  tgioo  22336  blcvx  22338  zcld  22353  recld2  22354  iccntr  22361  icccmplem1  22362  reconnlem1  22366  reconnlem2  22367  opnreen  22371  metnrmlem3  22400  icoopnst  22474  cnheibor  22490  lebnumii  22501  nmoleub2lem  22650  lmnn  22784  iscau3  22799  minveclem4  22925  ivthlem1  22941  ivthlem2  22942  ivthlem3  22943  ivth2  22945  ivthle  22946  ivthle2  22947  ivthicc  22948  evthicc  22949  cniccbdd  22951  ovolgelb  22969  ovollb2lem  22977  ovolunlem1  22986  ovoliunlem1  22991  ovoliunlem2  22992  ovoliun  22994  ovolscalem1  23002  ovolicc1  23005  ovolicc2lem4  23009  ovolicc2lem5  23010  ovolicc2  23011  ovolicc  23012  nulmbl2  23025  voliunlem2  23040  ioombl1lem4  23050  ioorcl2  23060  uniioombllem1  23069  uniioombllem2a  23070  uniioombllem3  23073  dyaddisjlem  23083  dyadmaxlem  23085  opnmbllem  23089  volivth  23095  vitalilem4  23100  mbfmulc2lem  23134  mbfmax  23136  mbfposr  23139  ismbf3d  23141  mbfaddlem  23147  mbflimsup  23153  mbfi1fseqlem4  23205  itg2lcl  23214  xrge0f  23218  itg2itg1  23223  itg2const2  23228  itg2seq  23229  itg2uba  23230  itg2lea  23231  itg2mulclem  23233  itg2mulc  23234  itg2splitlem  23235  itg2split  23236  itg2monolem2  23238  itg2monolem3  23239  itg2mono  23240  itg2gt0  23247  itg2cnlem1  23248  itg2cnlem2  23249  itg2cn  23250  iblss  23291  itgle  23296  itgeqa  23300  itgioo  23302  ibladdlem  23306  iblabs  23315  iblabsr  23316  iblmulc2  23317  itgsplit  23322  itgspliticc  23323  itgsplitioo  23324  bddmulibl  23325  ditgcl  23342  ditgswap  23343  ditgsplitlem  23344  dvferm1lem  23465  dvferm2lem  23467  dvferm  23469  rollelem  23470  rolle  23471  cmvth  23472  mvth  23473  dvlip  23474  dvlip2  23476  c1liplem1  23477  c1lip1  23478  dveq0  23481  dvgt0lem1  23483  dvivthlem1  23489  dvivth  23491  lhop1lem  23494  lhop1  23495  lhop2  23496  lhop  23497  dvcnvrelem1  23498  dvcnvre  23500  dvcvx  23501  dvfsumle  23502  dvfsumge  23503  dvfsumabs  23504  dvfsumlem2  23508  dvfsumlem3  23509  dvfsumlem4  23510  dvfsumrlimge0  23511  dvfsumrlim2  23513  ftc1lem1  23516  ftc1lem2  23517  ftc1a  23518  ftc1lem4  23520  ftc2  23525  ftc2ditglem  23526  itgparts  23528  itgsubstlem  23529  itgsubst  23530  degltlem1  23550  deg1ge  23576  coe1mul3  23577  deg1sublt  23588  deg1mul2  23592  deg1tmle  23595  deg1tm  23596  plypf1  23686  taylfvallem1  23829  tayl0  23834  pserulm  23894  psercnlem1  23897  pserdvlem1  23899  pserdvlem2  23900  abelthlem3  23905  abelth  23913  efcvx  23921  logno1  24096  logtayl  24120  xrlimcnp  24409  logfacbnd3  24662  log2sumbnd  24947  pntpbnd2  24990  pntibndlem3  24995  ttgcontlem1  25480  nvlmle  26729  nmooge0  26809  nmoub3i  26815  isblo3i  26843  ubthlem1  26913  minvecolem4  26923  nmopge0  27957  nmfnge0  27973  nmophmi  28077  branmfn  28151  xaddeq0  28710  xlt2addrd  28716  xmulcand  28763  xreceu  28764  xdivrec  28769  fsumrp0cl  28829  xrge0slmod  28978  cnre2csqlem  29087  tpr2rico  29089  xrge0iifcnv  29110  xrge0iifhom  29114  lmxrge0  29129  esumfsup  29262  esumpcvgval  29270  esumcvg  29278  dya2iocress  29466  dya2iocbrsiga  29467  dya2icobrsiga  29468  dya2icoseg  29469  dya2iocucvr  29476  sxbrsigalem2  29478  omssubaddlem  29491  omssubadd  29492  orvcgteel  29659  dstrvprob  29663  orvclteel  29664  sgnmul  29734  sgnsub  29736  sgnmulsgn  29741  sgnmulsgp  29742  signstcl  29771  signstf  29772  signstf0  29774  signstfvn  29775  signsvtn0  29776  signstfvneq0  29778  signsvfn  29788  signsvfpn  29791  signsvfnn  29792  cvmliftlem6  30329  cvmliftlem7  30330  cvmliftlem8  30331  cvmliftlem9  30332  cvmliftlem10  30333  cvmliftlem13  30335  ivthALT  31303  iooelexlt  32186  relowlssretop  32187  relowlpssretop  32188  sin2h  32369  cos2h  32370  tan2h  32371  poimirlem30  32409  poimir  32412  heicant  32414  opnmbllem0  32415  mblfinlem1  32416  mblfinlem2  32417  mblfinlem3  32418  mblfinlem4  32419  ismblfin  32420  itg2addnclem  32431  itg2addnclem2  32432  itg2gt0cn  32435  ibladdnclem  32436  iblabsnclem  32443  iblabsnc  32444  iblmulc2nc  32445  bddiblnc  32450  ftc1cnnclem  32453  ftc1anclem1  32455  ftc1anclem4  32458  ftc1anclem5  32459  ftc1anclem6  32460  ftc1anclem7  32461  ftc1anclem8  32462  ftc1anc  32463  ftc2nc  32464  areacirclem1  32470  areacirclem5  32474  areacirc  32475  isbnd3  32553  blbnd  32556  prdsbnd  32562  prdsbnd2  32564  cntotbnd  32565  idomrootle  36592  idomodle  36593  itgpowd  36619  imo72b2  37297  cvgdvgrat  37334  radcnvrat  37335  rfcnpre3  38015  rfcnpre4  38016  nnxrd  38024  absfico  38205  lefldiveq  38246  lttri5d  38254  supxrgere  38291  supxrgelem  38295  supxrge  38296  xralrple2  38312  infxr  38325  infleinflem1  38328  infleinflem2  38329  xralrple4  38331  xralrple3  38332  xrralrecnnle  38344  xrralrecnnge  38355  gtnelioc  38360  ltnelicc  38367  iooabslt  38369  gtnelicc  38370  eliooshift  38377  iocopn  38394  eliccelioc  38395  iooshift  38396  icoopn  38399  ge0lere  38407  iooiinicc  38417  sqrlearg  38428  iooiinioc  38431  fsumge0cl  38441  limciccioolb  38489  lptioo1  38500  limcicciooub  38505  ltmod  38506  lptre2pt  38508  limsupre  38509  limcresiooub  38510  limcresioolb  38511  limcleqr  38512  sinaover2ne0  38552  ioccncflimc  38572  icccncfext  38574  icocncflimc  38576  cncfiooicclem1  38580  cncfiooicc  38581  cncfiooiccre  38582  cncfioobdlem  38583  dvbdfbdioolem1  38619  dvbdfbdioolem2  38620  dvbdfbdioo  38621  ioodvbdlimc1lem1  38622  ioodvbdlimc1lem2  38623  ioodvbdlimc1  38624  ioodvbdlimc2lem  38625  ioodvbdlimc2  38626  ditgeqiooicc  38653  iblsplit  38659  itgcoscmulx  38662  ibliooicc  38664  iblspltprt  38666  itgsincmulx  38667  itgsubsticc  38669  itgioocnicc  38670  iblcncfioo  38671  itgspltprt  38672  itgiccshift  38673  volioore  38684  voliooico  38686  voliooicof  38690  voliccico  38693  stoweidlem34  38728  stoweidlem52  38746  stirlinglem5  38772  dirkercncflem1  38797  dirkercncflem4  38800  fourierdlem4  38805  fourierdlem10  38811  fourierdlem19  38820  fourierdlem20  38821  fourierdlem24  38825  fourierdlem25  38826  fourierdlem26  38827  fourierdlem27  38828  fourierdlem28  38829  fourierdlem31  38832  fourierdlem32  38833  fourierdlem33  38834  fourierdlem35  38836  fourierdlem37  38838  fourierdlem40  38841  fourierdlem41  38842  fourierdlem43  38844  fourierdlem44  38845  fourierdlem46  38846  fourierdlem47  38847  fourierdlem48  38848  fourierdlem49  38849  fourierdlem50  38850  fourierdlem51  38851  fourierdlem52  38852  fourierdlem54  38854  fourierdlem57  38857  fourierdlem59  38859  fourierdlem60  38860  fourierdlem61  38861  fourierdlem62  38862  fourierdlem63  38863  fourierdlem64  38864  fourierdlem65  38865  fourierdlem68  38868  fourierdlem69  38869  fourierdlem70  38870  fourierdlem72  38872  fourierdlem73  38873  fourierdlem74  38874  fourierdlem75  38875  fourierdlem76  38876  fourierdlem78  38878  fourierdlem79  38879  fourierdlem81  38881  fourierdlem82  38882  fourierdlem84  38884  fourierdlem89  38889  fourierdlem90  38890  fourierdlem91  38891  fourierdlem92  38892  fourierdlem93  38893  fourierdlem94  38894  fourierdlem97  38897  fourierdlem100  38900  fourierdlem101  38901  fourierdlem102  38902  fourierdlem103  38903  fourierdlem104  38904  fourierdlem107  38907  fourierdlem109  38909  fourierdlem111  38911  fourierdlem112  38912  fourierdlem113  38913  fourierdlem114  38914  sqwvfoura  38922  fouriersw  38925  etransclem23  38951  etransclem46  38974  qndenserrnbllem  38991  rrxsnicc  38997  ioorrnopnlem  39001  ioorrnopnxrlem  39003  salgencntex  39038  sge0cl  39075  sge0fsum  39081  sge0iunmptlemre  39109  sge0isum  39121  sge0ad2en  39125  sge0xaddlem1  39127  sge0xaddlem2  39128  sge0reuz  39141  voliunsge0lem  39166  meassre  39171  omessre  39201  omeiunltfirp  39210  hoissre  39235  hoiprodcl  39238  ovnsubaddlem1  39261  hoiprodcl3  39271  hoidmvcl  39273  hsphoidmvle2  39276  hsphoidmvle  39277  sge0hsphoire  39280  hoidmv1lelem1  39282  hoidmv1lelem2  39283  hoidmv1lelem3  39284  hoidmv1le  39285  hoidmvlelem1  39286  hoidmvlelem2  39287  hoidmvlelem3  39288  hoidmvlelem4  39289  ovnhoilem1  39292  ovnhoilem2  39293  ovnhoi  39294  ovnlecvr2  39301  hspdifhsp  39307  hoidifhspdmvle  39311  hoiqssbllem1  39313  hoiqssbllem2  39314  hoiqssbllem3  39315  hspmbllem1  39317  hspmbllem2  39318  volicorege0  39328  ovolval5lem1  39343  ovolval5lem2  39344  iinhoiicclem  39365  iinhoiicc  39366  iunhoiioolem  39367  iunhoiioo  39368  vonioolem2  39373  vonicclem2  39376  vonsn  39383  pimltmnf2  39389  pimconstlt0  39392  pimgtpnf2  39395  salpreimagelt  39396  salpreimalegt  39398  preimageiingt  39408  preimaleiinlt  39409  pimrecltneg  39411  issmflem  39414  issmflelem  39432  issmfgtlem  39443  issmfgt  39444  smfaddlem1  39450  issmfgelem  39456  issmfge  39457  smfpimioompt  39472  smfresal  39474  smfrec  39475  smfmullem1  39477  smfmullem2  39478  smfmullem3  39479  smfmullem4  39480  smfpimbor1lem1  39484  bgoldbtbnd  40027  xnn0xr  40201  xnn0xrge0  40202
  Copyright terms: Public domain W3C validator