Theorem 8re 12452

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 12424	. 2 ⊢ 8 = (7 + 1)
2		7re 12449	. . 3 ⊢ 7 ∈ ℝ
3		1re 11321	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11337	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2860	1 ⊢ 8 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7430  ℝcr 11212  1c1 11214   + caddc 11216  7c7 12415  8c8 12416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-i2m1 11281  ax-1ne0 11282  ax-rrecex 11285  ax-cnre 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433  df-2 12418  df-3 12419  df-4 12420  df-5 12421  df-6 12422  df-7 12423  df-8 12424

This theorem is used by:  9re  12455  6lt8  12551  5lt8  12552  4lt8  12553  3lt8  12554  2lt8  12555  1lt8  12556  8lt9  12557  7lt9  12558  8th4div3  12579  8lt10  12965  ef01bndlem  16367  cos2bnd  16371  slotstnscsi  17546  slotsdnscsi  17578  chtub  27554  bposlem8  27633  bposlem9  27634  lgsdir2lem1  27667  lgsdir2lem4  27670  lgsdir2lem5  27671  2lgsoddprmlem1  27750  2lgsoddprmlem2  27751  chebbnd1lem2  27812  chebbnd1lem3  27813  chebbnd1  27814  pntlemf  27947  hgt750lem  35336  hgt750lem2  35337  hgt750leme  35343  lcmineqlem23  43247  lcmineqlem  43248  3lexlogpow5ineq2  43251  aks4d1p1  43272  8rp  43506  resqrtvalex  44791  imsqrtvalex  44792  fmtnoprmfac2lem1  48796  mod42tp1mod8  48832  nnsum3primesle9  49037  nnsum4primesoddALTV  49040  nnsum4primesevenALTV  49044  bgoldbtbndlem1  49048  tgoldbach  49060