Theorem 8re 9092

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 9072	. 2 |- 8 = ( 7 + 1 )
2		7re 9090	. . 3 |- 7 e. RR
3		1re 8042	. . 3 |- 1 e. RR
4	2, 3	readdcli 8056	. 2 |- ( 7 + 1 ) e. RR
5	1, 4	eqeltri 2269	1 |- 8 e. RR

Syntax hints:   e. wcel 2167  (class class class)co 5925   RRcr 7895   1c1 7897   + caddc 7899   7c7 9063   8c8 9064

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1re 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9066  df-3 9067  df-4 9068  df-5 9069  df-6 9070  df-7 9071  df-8 9072

This theorem is referenced by:  8cn  9093  9re  9094  9pos  9111  6lt8  9199  5lt8  9200  4lt8  9201  3lt8  9202  2lt8  9203  1lt8  9204  8lt9  9205  7lt9  9206  8th4div3  9227  8lt10  9605  7lt10  9606  ef01bndlem  11938  cos2bnd  11942  slotstnscsi  12897  slotsdnscsi  12925  2lgsoddprmlem1  15430  2lgsoddprmlem2  15431  2lgsoddprmlem3a  15432  2lgsoddprmlem3b  15433  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435