Theorem 8re 12439

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 12411	. 2 ⊢ 8 = (7 + 1)
2		7re 12436	. . 3 ⊢ 7 ∈ ℝ
3		1re 11308	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2857	1 ⊢ 8 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203  7c7 12402  8c8 12403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411

This theorem is used by:  9re  12442  6lt8  12538  5lt8  12539  4lt8  12540  3lt8  12541  2lt8  12542  1lt8  12543  8lt9  12544  7lt9  12545  8th4div3  12566  8lt10  12952  ef01bndlem  16352  cos2bnd  16356  slotstnscsi  17531  slotsdnscsi  17563  chtub  27539  bposlem8  27618  bposlem9  27619  lgsdir2lem1  27652  lgsdir2lem4  27655  lgsdir2lem5  27656  2lgsoddprmlem1  27735  2lgsoddprmlem2  27736  chebbnd1lem2  27797  chebbnd1lem3  27798  chebbnd1  27799  pntlemf  27932  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  lcmineqlem23  43101  lcmineqlem  43102  3lexlogpow5ineq2  43105  aks4d1p1  43126  8rp  43360  resqrtvalex  44644  imsqrtvalex  44645  fmtnoprmfac2lem1  48650  mod42tp1mod8  48686  nnsum3primesle9  48891  nnsum4primesoddALTV  48894  nnsum4primesevenALTV  48898  bgoldbtbndlem1  48902  tgoldbach  48914