Theorem 8re 12271

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 12244	. 2 ⊢ 8 = (7 + 1)
2		7re 12268	. . 3 ⊢ 7 ∈ ℝ
3		1re 11138	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11154	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  7c7 12235  8c8 12236

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 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244

This theorem is referenced by:  9re  12274  9pos  12288  6lt8  12363  5lt8  12364  4lt8  12365  3lt8  12366  2lt8  12367  1lt8  12368  8lt9  12369  7lt9  12370  8th4div3  12391  8lt10  12770  7lt10  12771  ef01bndlem  16145  cos2bnd  16149  slotstnscsi  17317  slotsdnscsi  17349  chtub  27192  bposlem8  27271  bposlem9  27272  lgsdir2lem1  27305  lgsdir2lem4  27308  lgsdir2lem5  27309  2lgsoddprmlem1  27388  2lgsoddprmlem2  27389  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  pntlemf  27585  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  lcmineqlem23  42507  lcmineqlem  42508  3lexlogpow5ineq2  42511  aks4d1p1  42532  8rp  42752  resqrtvalex  44093  imsqrtvalex  44094  fmtnoprmfac2lem1  48044  mod42tp1mod8  48080  nnsum3primesle9  48285  nnsum4primesoddALTV  48288  nnsum4primesevenALTV  48292  bgoldbtbndlem1  48296  tgoldbach  48308