Theorem 8re 9287

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 9267	. 2 |- 8 = ( 7 + 1 )
2		7re 9285	. . 3 |- 7 e. RR
3		1re 8238	. . 3 |- 1 e. RR
4	2, 3	readdcli 8252	. 2 |- ( 7 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 8 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6028   RRcr 8091   1c1 8093   + caddc 8095   7c7 9258   8c8 9259

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 2213  ax-1re 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9261  df-3 9262  df-4 9263  df-5 9264  df-6 9265  df-7 9266  df-8 9267

This theorem is referenced by:  8cn  9288  9re  9289  9pos  9306  6lt8  9394  5lt8  9395  4lt8  9396  3lt8  9397  2lt8  9398  1lt8  9399  8lt9  9400  7lt9  9401  8th4div3  9422  8lt10  9803  7lt10  9804  ef01bndlem  12397  cos2bnd  12401  slotstnscsi  13358  slotsdnscsi  13386  2lgsoddprmlem1  15924  2lgsoddprmlem2  15925  2lgsoddprmlem3a  15926  2lgsoddprmlem3b  15927  2lgsoddprmlem3c  15928  2lgsoddprmlem3d  15929