Theorem 8re 9322

Description: The number 8 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
8re	|- 8 e. RR

Proof of Theorem 8re

Step	Hyp	Ref	Expression
1		df-8 9302	. 2 |- 8 = ( 7 + 1 )
2		7re 9320	. . 3 |- 7 e. RR
3		1re 8273	. . 3 |- 1 e. RR
4	2, 3	readdcli 8287	. 2 |- ( 7 + 1 ) e. RR
5	1, 4	eqeltri 2305	1 |- 8 e. RR

Syntax hints:   e. wcel 2203  (class class class)co 6050   RRcr 8126   1c1 8128   + caddc 8130   7c7 9293   8c8 9294

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9296  df-3 9297  df-4 9298  df-5 9299  df-6 9300  df-7 9301  df-8 9302

This theorem is referenced by:  8cn  9323  9re  9324  9pos  9341  6lt8  9429  5lt8  9430  4lt8  9431  3lt8  9432  2lt8  9433  1lt8  9434  8lt9  9435  7lt9  9436  8th4div3  9457  8lt10  9840  7lt10  9841  ef01bndlem  12442  cos2bnd  12446  slotstnscsi  13408  slotsdnscsi  13436  2lgsoddprmlem1  15978  2lgsoddprmlem2  15979  2lgsoddprmlem3a  15980  2lgsoddprmlem3b  15981  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983