Theorem 8re 12258

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  1c1 11045   + caddc 11047  7c7 12222  8c8 12223

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 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231

This theorem is referenced by:  9re  12261  9pos  12275  6lt8  12350  5lt8  12351  4lt8  12352  3lt8  12353  2lt8  12354  1lt8  12355  8lt9  12356  7lt9  12357  8th4div3  12378  8lt10  12757  7lt10  12758  ef01bndlem  16128  cos2bnd  16132  slotstnscsi  17299  slotsdnscsi  17331  chtub  27156  bposlem8  27235  bposlem9  27236  lgsdir2lem1  27269  lgsdir2lem4  27272  lgsdir2lem5  27273  2lgsoddprmlem1  27352  2lgsoddprmlem2  27353  chebbnd1lem2  27414  chebbnd1lem3  27415  chebbnd1  27416  pntlemf  27549  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  lcmineqlem23  42032  lcmineqlem  42033  3lexlogpow5ineq2  42036  aks4d1p1  42057  8rp  42284  resqrtvalex  43627  imsqrtvalex  43628  fmtnoprmfac2lem1  47560  mod42tp1mod8  47596  nnsum3primesle9  47788  nnsum4primesoddALTV  47791  nnsum4primesevenALTV  47795  bgoldbtbndlem1  47799  tgoldbach  47811