Theorem 8re 9227

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 9207	. 2 ⊢ 8 = (7 + 1)
2		7re 9225	. . 3 ⊢ 7 ∈ ℝ
3		1re 8177	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8191	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2304	1 ⊢ 8 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  ℝcr 8030  1c1 8032   + caddc 8034  7c7 9198  8c8 9199

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 8125  ax-addrcl 8128

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

This theorem is referenced by:  8cn  9228  9re  9229  9pos  9246  6lt8  9334  5lt8  9335  4lt8  9336  3lt8  9337  2lt8  9338  1lt8  9339  8lt9  9340  7lt9  9341  8th4div3  9362  8lt10  9741  7lt10  9742  ef01bndlem  12316  cos2bnd  12320  slotstnscsi  13277  slotsdnscsi  13305  2lgsoddprmlem1  15833  2lgsoddprmlem2  15834  2lgsoddprmlem3a  15835  2lgsoddprmlem3b  15836  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838