Theorem 8re 12282

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 12255	. 2 ⊢ 8 = (7 + 1)
2		7re 12279	. . 3 ⊢ 7 ∈ ℝ
3		1re 11174	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  7c7 12246  8c8 12247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255

This theorem is referenced by:  9re  12285  9pos  12299  6lt8  12374  5lt8  12375  4lt8  12376  3lt8  12377  2lt8  12378  1lt8  12379  8lt9  12380  7lt9  12381  8th4div3  12402  8lt10  12781  7lt10  12782  ef01bndlem  16152  cos2bnd  16156  slotstnscsi  17323  slotsdnscsi  17355  chtub  27123  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  lgsdir2lem4  27239  lgsdir2lem5  27240  2lgsoddprmlem1  27319  2lgsoddprmlem2  27320  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  pntlemf  27516  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  lcmineqlem23  42039  lcmineqlem  42040  3lexlogpow5ineq2  42043  aks4d1p1  42064  8rp  42291  resqrtvalex  43634  imsqrtvalex  43635  fmtnoprmfac2lem1  47567  mod42tp1mod8  47603  nnsum3primesle9  47795  nnsum4primesoddALTV  47798  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  tgoldbach  47818