Theorem 8re 12149

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 12122	. 2 ⊢ 8 = (7 + 1)
2		7re 12146	. . 3 ⊢ 7 ∈ ℝ
3		1re 11055	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11070	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2834	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7317  ℝcr 10950  1c1 10952   + caddc 10954  7c7 12113  8c8 12114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-i2m1 11019  ax-1ne0 11020  ax-rrecex 11023  ax-cnre 11024

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-iota 6418  df-fv 6474  df-ov 7320  df-2 12116  df-3 12117  df-4 12118  df-5 12119  df-6 12120  df-7 12121  df-8 12122

This theorem is referenced by:  9re  12152  9pos  12166  6lt8  12246  5lt8  12247  4lt8  12248  3lt8  12249  2lt8  12250  1lt8  12251  8lt9  12252  7lt9  12253  8th4div3  12273  8lt10  12649  7lt10  12650  ef01bndlem  15972  cos2bnd  15976  slotstnscsi  17147  slotsdnscsi  17179  sralemOLD  20523  chtub  26443  bposlem8  26522  bposlem9  26523  lgsdir2lem1  26556  lgsdir2lem4  26559  lgsdir2lem5  26560  2lgsoddprmlem1  26639  2lgsoddprmlem2  26640  chebbnd1lem2  26701  chebbnd1lem3  26702  chebbnd1  26703  pntlemf  26836  cchhllemOLD  27391  hgt750lem  32771  hgt750lem2  32772  hgt750leme  32778  lcmineqlem23  40280  lcmineqlem  40281  3lexlogpow5ineq2  40284  aks4d1p1  40305  resqrtvalex  41487  imsqrtvalex  41488  fmtnoprmfac2lem1  45283  mod42tp1mod8  45319  nnsum3primesle9  45511  nnsum4primesoddALTV  45514  nnsum4primesevenALTV  45518  bgoldbtbndlem1  45522  tgoldbach  45534