Theorem 8re 9228

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 9208	. 2 ⊢ 8 = (7 + 1)
2		7re 9226	. . 3 ⊢ 7 ∈ ℝ
3		1re 8178	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8192	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031  1c1 8033   + caddc 8035  7c7 9199  8c8 9200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9202  df-3 9203  df-4 9204  df-5 9205  df-6 9206  df-7 9207  df-8 9208

This theorem is referenced by:  8cn  9229  9re  9230  9pos  9247  6lt8  9335  5lt8  9336  4lt8  9337  3lt8  9338  2lt8  9339  1lt8  9340  8lt9  9341  7lt9  9342  8th4div3  9363  8lt10  9742  7lt10  9743  ef01bndlem  12335  cos2bnd  12339  slotstnscsi  13296  slotsdnscsi  13324  2lgsoddprmlem1  15853  2lgsoddprmlem2  15854  2lgsoddprmlem3a  15855  2lgsoddprmlem3b  15856  2lgsoddprmlem3c  15857  2lgsoddprmlem3d  15858