Theorem 8re 12341

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 12314	. 2 ⊢ 8 = (7 + 1)
2		7re 12338	. . 3 ⊢ 7 ∈ ℝ
3		1re 11240	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11255	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2831	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133  1c1 11135   + caddc 11137  7c7 12305  8c8 12306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-i2m1 11202  ax-1ne0 11203  ax-rrecex 11206  ax-cnre 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314

This theorem is referenced by:  9re  12344  9pos  12358  6lt8  12438  5lt8  12439  4lt8  12440  3lt8  12441  2lt8  12442  1lt8  12443  8lt9  12444  7lt9  12445  8th4div3  12466  8lt10  12845  7lt10  12846  ef01bndlem  16207  cos2bnd  16211  slotstnscsi  17379  slotsdnscsi  17411  chtub  27180  bposlem8  27259  bposlem9  27260  lgsdir2lem1  27293  lgsdir2lem4  27296  lgsdir2lem5  27297  2lgsoddprmlem1  27376  2lgsoddprmlem2  27377  chebbnd1lem2  27438  chebbnd1lem3  27439  chebbnd1  27440  pntlemf  27573  hgt750lem  34688  hgt750lem2  34689  hgt750leme  34695  lcmineqlem23  42069  lcmineqlem  42070  3lexlogpow5ineq2  42073  aks4d1p1  42094  8rp  42321  resqrtvalex  43644  imsqrtvalex  43645  fmtnoprmfac2lem1  47560  mod42tp1mod8  47596  nnsum3primesle9  47788  nnsum4primesoddALTV  47791  nnsum4primesevenALTV  47795  bgoldbtbndlem1  47799  tgoldbach  47811