Theorem 8re 12315

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 12287	. 2 ⊢ 8 = (7 + 1)
2		7re 12312	. . 3 ⊢ 7 ∈ ℝ
3		1re 11182	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11198	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7397  ℝcr 11073  1c1 11075   + caddc 11077  7c7 12278  8c8 12279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-i2m1 11142  ax-1ne0 11143  ax-rrecex 11146  ax-cnre 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6478  df-fv 6530  df-ov 7400  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287

This theorem is referenced by:  9re  12318  6lt8  12414  5lt8  12415  4lt8  12416  3lt8  12417  2lt8  12418  1lt8  12419  8lt9  12420  7lt9  12421  8th4div3  12442  8lt10  12827  ef01bndlem  16217  cos2bnd  16221  slotstnscsi  17390  slotsdnscsi  17422  chtub  27277  bposlem8  27356  bposlem9  27357  lgsdir2lem1  27390  lgsdir2lem4  27393  lgsdir2lem5  27394  2lgsoddprmlem1  27473  2lgsoddprmlem2  27474  chebbnd1lem2  27535  chebbnd1lem3  27536  chebbnd1  27537  pntlemf  27670  hgt750lem  34946  hgt750lem2  34947  hgt750leme  34953  lcmineqlem23  42669  lcmineqlem  42670  3lexlogpow5ineq2  42673  aks4d1p1  42694  8rp  42913  resqrtvalex  44222  imsqrtvalex  44223  fmtnoprmfac2lem1  48176  mod42tp1mod8  48212  nnsum3primesle9  48417  nnsum4primesoddALTV  48420  nnsum4primesevenALTV  48424  bgoldbtbndlem1  48428  tgoldbach  48440