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

Theorem ressxr 10673
Description: The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
ressxr ℝ ⊆ ℝ*

Proof of Theorem ressxr
StepHypRef Expression
1 ssun1 4145 . 2 ℝ ⊆ (ℝ ∪ {+∞, -∞})
2 df-xr 10667 . 2 * = (ℝ ∪ {+∞, -∞})
31, 2sseqtrri 4001 1 ℝ ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  cun 3931  wss 3933  {cpr 4559  cr 10524  +∞cpnf 10660  -∞cmnf 10661  *cxr 10662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-xr 10667
This theorem is referenced by:  rexpssxrxp  10674  rexr  10675  0xr  10676  rexrd  10679  ltrelxr  10690  supxrre  12708  supxrbnd  12709  supxrgtmnf  12710  supxrre1  12711  supxrre2  12712  infxrre  12717  iooval2  12759  fzval2  12883  uzsup  13219  hashxrcl  13706  seqcoll  13810  limsupval2  14825  limsupgre  14826  limsupbnd2  14828  rlimuni  14895  rlimcld2  14923  rlimno1  14998  isercolllem2  15010  isercoll  15012  caucvgrlem  15017  summolem2a  15060  prodmolem2a  15276  ramtlecl  16324  ramxrcl  16341  ismet2  22870  prdsmet  22907  qtopbas  23295  tgqioo  23335  re2ndc  23336  xrsmopn  23347  metdcn2  23374  metdscn2  23392  bndth  23489  ovolunlem1a  24024  ovolunlem1  24025  ovoliunlem1  24030  ovoliun  24033  ovolicc2lem4  24048  voliunlem2  24079  voliunlem3  24080  opnmblALT  24131  vitalilem4  24139  mbfimaopnlem  24183  itg2le  24267  itg2seq  24270  dvfsumrlim  24555  itgsubst  24573  mdegleb  24585  mdeglt  24586  mdegldg  24587  mdegxrcl  24588  mdegcl  24590  mdegaddle  24595  mdegmullem  24599  deg1mul3le  24637  ig1pdvds  24697  aannenlem2  24845  taylfval  24874  radcnvcl  24932  radcnvlt1  24933  radcnvle  24935  xrlimcnp  25473  nmoxr  28470  nmooge0  28471  nmoolb  28475  nmoubi  28476  nmlno0lem  28497  nmopxr  29570  nmfnxr  29583  nmoplb  29611  nmopub  29612  nmfnlb  29628  nmfnleub  29629  nmlnop0iALT  29699  nmopun  29718  branmfn  29809  pjnmopi  29852  xlt2addrd  30408  xreceu  30525  rexdiv  30529  xrsmulgzz  30592  esumcst  31221  icorempo  34514  mblfinlem2  34811  itg2addnc  34827  prdsbnd  34952  rrnequiv  34994  hbtlem2  39602  binomcxplemdvbinom  40562  binomcxplemcvg  40563  binomcxplemnotnn0  40565  suplesup  41483  frexr  41531  zssxr  41546  ssrexr  41582  uzxrd  41614  supminfxr  41616  rpssxr  41633  elicores  41685  ressiocsup  41706  ressioosup  41707  ressiooinf  41709  uzinico  41712  limsupre  41798  limsupresico  41857  limsuppnfdlem  41858  limsupmnflem  41877  limsupvaluz2  41895  supcnvlimsup  41897  liminfresico  41928  volicoff  42157  volicofmpt  42159  fourierdlem52  42320  fourierdlem103  42371  fourierdlem104  42372  etransclem48  42444  ioorrnopnlem  42466  fsumlesge0  42536  sge0cl  42540  sge0supre  42548  sge0less  42551  sge0split  42568  sge0seq  42605  hoicvr  42707  volicorescl  42712  ovolval2lem  42802  ovolval5lem2  42812  ovnovollem1  42815  ovnovollem2  42816  iinhoiicclem  42832  iunhoiioolem  42834  iccvonmbllem  42837  vonioolem2  42840  vonioo  42841  vonicclem2  42843  vonicc  42844  pimdecfgtioc  42870  pimincfltioc  42871  pimdecfgtioo  42872  pimincfltioo  42873  smflimsuplem4  42974
  Copyright terms: Public domain W3C validator