Theorem 8re 12304

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 12277	. 2 ⊢ 8 = (7 + 1)
2		7re 12301	. . 3 ⊢ 7 ∈ ℝ
3		1re 11210	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11225	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2829	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7405  ℝcr 11105  1c1 11107   + caddc 11109  7c7 12268  8c8 12269

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277

This theorem is referenced by:  9re  12307  9pos  12321  6lt8  12401  5lt8  12402  4lt8  12403  3lt8  12404  2lt8  12405  1lt8  12406  8lt9  12407  7lt9  12408  8th4div3  12428  8lt10  12805  7lt10  12806  ef01bndlem  16123  cos2bnd  16127  slotstnscsi  17301  slotsdnscsi  17333  sralemOLD  20783  chtub  26704  bposlem8  26783  bposlem9  26784  lgsdir2lem1  26817  lgsdir2lem4  26820  lgsdir2lem5  26821  2lgsoddprmlem1  26900  2lgsoddprmlem2  26901  chebbnd1lem2  26962  chebbnd1lem3  26963  chebbnd1  26964  pntlemf  27097  cchhllemOLD  28134  hgt750lem  33651  hgt750lem2  33652  hgt750leme  33658  lcmineqlem23  40904  lcmineqlem  40905  3lexlogpow5ineq2  40908  aks4d1p1  40929  resqrtvalex  42381  imsqrtvalex  42382  fmtnoprmfac2lem1  46220  mod42tp1mod8  46256  nnsum3primesle9  46448  nnsum4primesoddALTV  46451  nnsum4primesevenALTV  46455  bgoldbtbndlem1  46459  tgoldbach  46471