Theorem 8re 12389

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 12362	. 2 ⊢ 8 = (7 + 1)
2		7re 12386	. . 3 ⊢ 7 ∈ ℝ
3		1re 11290	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11305	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2840	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183  1c1 11185   + caddc 11187  7c7 12353  8c8 12354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362

This theorem is referenced by:  9re  12392  9pos  12406  6lt8  12486  5lt8  12487  4lt8  12488  3lt8  12489  2lt8  12490  1lt8  12491  8lt9  12492  7lt9  12493  8th4div3  12513  8lt10  12890  7lt10  12891  ef01bndlem  16232  cos2bnd  16236  slotstnscsi  17419  slotsdnscsi  17451  sralemOLD  21199  chtub  27274  bposlem8  27353  bposlem9  27354  lgsdir2lem1  27387  lgsdir2lem4  27390  lgsdir2lem5  27391  2lgsoddprmlem1  27470  2lgsoddprmlem2  27471  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  pntlemf  27667  cchhllemOLD  28920  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  lcmineqlem23  42008  lcmineqlem  42009  3lexlogpow5ineq2  42012  aks4d1p1  42033  8rp  42291  resqrtvalex  43607  imsqrtvalex  43608  fmtnoprmfac2lem1  47440  mod42tp1mod8  47476  nnsum3primesle9  47668  nnsum4primesoddALTV  47671  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  tgoldbach  47691