Theorem 8re 12356

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 12328	. 2 ⊢ 8 = (7 + 1)
2		7re 12353	. . 3 ⊢ 7 ∈ ℝ
3		1re 11227	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11243	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2861	1 ⊢ 8 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11118  1c1 11120   + caddc 11122  7c7 12319  8c8 12320

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11177  ax-icn 11178  ax-addcl 11179  ax-addrcl 11180  ax-mulcl 11181  ax-mulrcl 11182  ax-i2m1 11187  ax-1ne0 11188  ax-rrecex 11191  ax-cnre 11192

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328

This theorem is used by:  9re  12359  6lt8  12455  5lt8  12456  4lt8  12457  3lt8  12458  2lt8  12459  1lt8  12460  8lt9  12461  7lt9  12462  8th4div3  12483  8lt10  12869  ef01bndlem  16266  cos2bnd  16270  slotstnscsi  17439  slotsdnscsi  17471  chtub  27431  bposlem8  27510  bposlem9  27511  lgsdir2lem1  27544  lgsdir2lem4  27547  lgsdir2lem5  27548  2lgsoddprmlem1  27627  2lgsoddprmlem2  27628  chebbnd1lem2  27689  chebbnd1lem3  27690  chebbnd1  27691  pntlemf  27824  hgt750lem  35107  hgt750lem2  35108  hgt750leme  35114  lcmineqlem23  42880  lcmineqlem  42881  3lexlogpow5ineq2  42884  aks4d1p1  42905  8rp  43141  resqrtvalex  44448  imsqrtvalex  44449  fmtnoprmfac2lem1  48395  mod42tp1mod8  48431  nnsum3primesle9  48636  nnsum4primesoddALTV  48639  nnsum4primesevenALTV  48643  bgoldbtbndlem1  48647  tgoldbach  48659