Theorem 8re 12277

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 12250	. 2 ⊢ 8 = (7 + 1)
2		7re 12274	. . 3 ⊢ 7 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  7c7 12241  8c8 12242

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250

This theorem is referenced by:  9re  12280  9pos  12294  6lt8  12369  5lt8  12370  4lt8  12371  3lt8  12372  2lt8  12373  1lt8  12374  8lt9  12375  7lt9  12376  8th4div3  12397  8lt10  12776  7lt10  12777  ef01bndlem  16151  cos2bnd  16155  slotstnscsi  17323  slotsdnscsi  17355  chtub  27175  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  lgsdir2lem4  27291  lgsdir2lem5  27292  2lgsoddprmlem1  27371  2lgsoddprmlem2  27372  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  pntlemf  27568  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  lcmineqlem23  42490  lcmineqlem  42491  3lexlogpow5ineq2  42494  aks4d1p1  42515  8rp  42735  resqrtvalex  44072  imsqrtvalex  44073  fmtnoprmfac2lem1  48029  mod42tp1mod8  48065  nnsum3primesle9  48270  nnsum4primesoddALTV  48273  nnsum4primesevenALTV  48277  bgoldbtbndlem1  48281  tgoldbach  48293