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

Theorem ressxr 10678
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 4102 . 2 ℝ ⊆ (ℝ ∪ {+∞, -∞})
2 df-xr 10672 . 2 * = (ℝ ∪ {+∞, -∞})
31, 2sseqtrri 3955 1 ℝ ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  cun 3882  wss 3884  {cpr 4530  cr 10529  +∞cpnf 10665  -∞cmnf 10666  *cxr 10667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-xr 10672
This theorem is referenced by:  rexpssxrxp  10679  rexr  10680  0xr  10681  rexrd  10684  ltrelxr  10695  supxrre  12712  supxrbnd  12713  supxrgtmnf  12714  supxrre1  12715  supxrre2  12716  infxrre  12721  iooval2  12763  fzval2  12892  uzsup  13230  hashxrcl  13718  seqcoll  13822  limsupval2  14832  limsupgre  14833  limsupbnd2  14835  rlimuni  14902  rlimcld2  14930  rlimno1  15005  isercolllem2  15017  isercoll  15019  caucvgrlem  15024  summolem2a  15067  prodmolem2a  15283  ramtlecl  16329  ramxrcl  16346  ismet2  22943  prdsmet  22980  qtopbas  23368  tgqioo  23408  re2ndc  23409  xrsmopn  23420  metdcn2  23447  metdscn2  23465  bndth  23566  ovolunlem1a  24103  ovolunlem1  24104  ovoliunlem1  24109  ovoliun  24112  ovolicc2lem4  24127  voliunlem2  24158  voliunlem3  24159  opnmblALT  24210  vitalilem4  24218  mbfimaopnlem  24262  itg2le  24346  itg2seq  24349  dvfsumrlim  24637  itgsubst  24655  mdegleb  24668  mdeglt  24669  mdegldg  24670  mdegxrcl  24671  mdegcl  24673  mdegaddle  24678  mdegmullem  24682  deg1mul3le  24720  ig1pdvds  24780  aannenlem2  24928  taylfval  24957  radcnvcl  25015  radcnvlt1  25016  radcnvle  25018  xrlimcnp  25557  nmoxr  28552  nmooge0  28553  nmoolb  28557  nmoubi  28558  nmlno0lem  28579  nmopxr  29652  nmfnxr  29665  nmoplb  29693  nmopub  29694  nmfnlb  29710  nmfnleub  29711  nmlnop0iALT  29781  nmopun  29800  branmfn  29891  pjnmopi  29934  xlt2addrd  30511  xreceu  30627  rexdiv  30631  xrsmulgzz  30715  esumcst  31430  icorempo  34763  mblfinlem2  35088  itg2addnc  35104  prdsbnd  35224  rrnequiv  35266  hbtlem2  40055  binomcxplemdvbinom  41044  binomcxplemcvg  41045  binomcxplemnotnn0  41047  suplesup  41958  frexr  42006  zssxr  42021  ssrexr  42056  uzxrd  42088  supminfxr  42090  rpssxr  42107  elicores  42157  ressiocsup  42178  ressioosup  42179  ressiooinf  42181  uzinico  42184  limsupre  42270  limsupresico  42329  limsupmnflem  42349  limsupvaluz2  42367  supcnvlimsup  42369  liminfresico  42400  volicoff  42624  volicofmpt  42626  fourierdlem52  42787  fourierdlem103  42838  fourierdlem104  42839  etransclem48  42911  ioorrnopnlem  42933  fsumlesge0  43003  sge0cl  43007  sge0supre  43015  sge0less  43018  sge0split  43035  sge0seq  43072  hoicvr  43174  volicorescl  43179  ovolval2lem  43269  ovolval5lem2  43279  ovnovollem1  43282  ovnovollem2  43283  iinhoiicclem  43299  iunhoiioolem  43301  iccvonmbllem  43304  vonioolem2  43307  vonioo  43308  vonicclem2  43310  vonicc  43311  pimdecfgtioc  43337  pimincfltioc  43338  pimdecfgtioo  43339  pimincfltioo  43340  smflimsuplem4  43441
  Copyright terms: Public domain W3C validator