Theorem 8re 9006

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 8986	. 2 |- 8 = ( 7 + 1 )
2		7re 9004	. . 3 |- 7 e. RR
3		1re 7958	. . 3 |- 1 e. RR
4	2, 3	readdcli 7972	. 2 |- ( 7 + 1 ) e. RR
5	1, 4	eqeltri 2250	1 |- 8 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5877   RRcr 7812   1c1 7814   + caddc 7816   7c7 8977   8c8 8978

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8980  df-3 8981  df-4 8982  df-5 8983  df-6 8984  df-7 8985  df-8 8986

This theorem is referenced by:  8cn  9007  9re  9008  9pos  9025  6lt8  9112  5lt8  9113  4lt8  9114  3lt8  9115  2lt8  9116  1lt8  9117  8lt9  9118  7lt9  9119  8th4div3  9140  8lt10  9517  7lt10  9518  ef01bndlem  11766  cos2bnd  11770  slotstnscsi  12655  slotsdnscsi  12679  2lgsoddprmlem1  14538  2lgsoddprmlem2  14539  2lgsoddprmlem3a  14540  2lgsoddprmlem3b  14541  2lgsoddprmlem3c  14542  2lgsoddprmlem3d  14543