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

Theorem 8re 11732
Description: The number 8 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
8re 8 ∈ ℝ

Proof of Theorem 8re
StepHypRef Expression
1 df-8 11705 . 2 8 = (7 + 1)
2 7re 11729 . . 3 7 ∈ ℝ
3 1re 10641 . . 3 1 ∈ ℝ
42, 3readdcli 10656 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2912 1 8 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  (class class class)co 7151  cr 10536  1c1 10538   + caddc 10540  7c7 11696  8c8 11697
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ne 3015  df-ral 3138  df-rex 3139  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5054  df-iota 6304  df-fv 6353  df-ov 7154  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705
This theorem is referenced by:  9re  11735  9pos  11749  6lt8  11829  5lt8  11830  4lt8  11831  3lt8  11832  2lt8  11833  1lt8  11834  8lt9  11835  7lt9  11836  8th4div3  11856  8lt10  12229  7lt10  12230  ef01bndlem  15539  cos2bnd  15543  sralem  19951  chtub  25805  bposlem8  25884  bposlem9  25885  lgsdir2lem1  25918  lgsdir2lem4  25921  lgsdir2lem5  25922  2lgsoddprmlem1  26001  2lgsoddprmlem2  26002  chebbnd1lem2  26063  chebbnd1lem3  26064  chebbnd1  26065  pntlemf  26198  cchhllem  26690  hgt750lem  32007  hgt750lem2  32008  hgt750leme  32014  lcmineqlem23  39314  lcmineqlem  39315  resqrtvalex  40289  imsqrtvalex  40290  fmtnoprmfac2lem1  44036  mod42tp1mod8  44073  nnsum3primesle9  44265  nnsum4primesoddALTV  44268  nnsum4primesevenALTV  44272  bgoldbtbndlem1  44276  tgoldbach  44288
  Copyright terms: Public domain W3C validator