Theorem 8re 12363

Description: The number 8 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
8re	⊢ 8 ∈ ℝ

Proof of Theorem 8re

Step	Hyp	Ref	Expression
1		df-8 12336	. 2 ⊢ 8 = (7 + 1)
2		7re 12360	. . 3 ⊢ 7 ∈ ℝ
3		1re 11262	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11277	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2836	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℝcr 11155  1c1 11157   + caddc 11159  7c7 12327  8c8 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-i2m1 11224  ax-1ne0 11225  ax-rrecex 11228  ax-cnre 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336

This theorem is referenced by:  9re  12366  9pos  12380  6lt8  12460  5lt8  12461  4lt8  12462  3lt8  12463  2lt8  12464  1lt8  12465  8lt9  12466  7lt9  12467  8th4div3  12488  8lt10  12867  7lt10  12868  ef01bndlem  16221  cos2bnd  16225  slotstnscsi  17405  slotsdnscsi  17437  sralemOLD  21177  chtub  27257  bposlem8  27336  bposlem9  27337  lgsdir2lem1  27370  lgsdir2lem4  27373  lgsdir2lem5  27374  2lgsoddprmlem1  27453  2lgsoddprmlem2  27454  chebbnd1lem2  27515  chebbnd1lem3  27516  chebbnd1  27517  pntlemf  27650  cchhllemOLD  28903  hgt750lem  34667  hgt750lem2  34668  hgt750leme  34674  lcmineqlem23  42053  lcmineqlem  42054  3lexlogpow5ineq2  42057  aks4d1p1  42078  8rp  42342  resqrtvalex  43663  imsqrtvalex  43664  fmtnoprmfac2lem1  47558  mod42tp1mod8  47594  nnsum3primesle9  47786  nnsum4primesoddALTV  47789  nnsum4primesevenALTV  47793  bgoldbtbndlem1  47797  tgoldbach  47809