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

Theorem 8re 11065
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 11045 . 2 8 = (7 + 1)
2 7re 11063 . . 3 7 ∈ ℝ
3 1re 9999 . . 3 1 ∈ ℝ
42, 3readdcli 10013 . 2 (7 + 1) ∈ ℝ
51, 4eqeltri 2694 1 8 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  (class class class)co 6615  cr 9895  1c1 9897   + caddc 9899  7c7 11035  8c8 11036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-i2m1 9964  ax-1ne0 9965  ax-rrecex 9968  ax-cnre 9969
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045
This theorem is referenced by:  8cn  11066  9re  11067  9pos  11082  6lt8  11176  5lt8  11177  4lt8  11178  3lt8  11179  2lt8  11180  1lt8  11181  8lt9  11182  7lt9  11183  8lt10OLD  11191  7lt10OLD  11192  8th4div3  11212  8lt10  11634  7lt10  11635  ef01bndlem  14858  cos2bnd  14862  sralem  19117  chtub  24871  bposlem8  24950  bposlem9  24951  lgsdir2lem1  24984  lgsdir2lem4  24987  lgsdir2lem5  24988  2lgsoddprmlem1  25067  2lgsoddprmlem2  25068  chebbnd1lem2  25093  chebbnd1lem3  25094  chebbnd1  25095  pntlemf  25228  cchhllem  25701  fmtnoprmfac2lem1  40807  mod42tp1mod8  40848  nnsum3primesle9  41001  nnsum4primesoddALTV  41004  nnsum4primesevenALTV  41008  bgoldbtbndlem1  41012  tgoldbach  41023  tgoldbachOLD  41030
  Copyright terms: Public domain W3C validator