Theorem 8re 12243

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 12216	. 2 ⊢ 8 = (7 + 1)
2		7re 12240	. . 3 ⊢ 7 ∈ ℝ
3		1re 11134	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11149	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11027  1c1 11029   + caddc 11031  7c7 12207  8c8 12208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216

This theorem is referenced by:  9re  12246  9pos  12260  6lt8  12335  5lt8  12336  4lt8  12337  3lt8  12338  2lt8  12339  1lt8  12340  8lt9  12341  7lt9  12342  8th4div3  12363  8lt10  12741  7lt10  12742  ef01bndlem  16111  cos2bnd  16115  slotstnscsi  17282  slotsdnscsi  17314  chtub  27181  bposlem8  27260  bposlem9  27261  lgsdir2lem1  27294  lgsdir2lem4  27297  lgsdir2lem5  27298  2lgsoddprmlem1  27377  2lgsoddprmlem2  27378  chebbnd1lem2  27439  chebbnd1lem3  27440  chebbnd1  27441  pntlemf  27574  hgt750lem  34810  hgt750lem2  34811  hgt750leme  34817  lcmineqlem23  42327  lcmineqlem  42328  3lexlogpow5ineq2  42331  aks4d1p1  42352  8rp  42579  resqrtvalex  43907  imsqrtvalex  43908  fmtnoprmfac2lem1  47833  mod42tp1mod8  47869  nnsum3primesle9  48061  nnsum4primesoddALTV  48064  nnsum4primesevenALTV  48068  bgoldbtbndlem1  48072  tgoldbach  48084