Theorem 8re 9123

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 9103	. 2 |- 8 = ( 7 + 1 )
2		7re 9121	. . 3 |- 7 e. RR
3		1re 8073	. . 3 |- 1 e. RR
4	2, 3	readdcli 8087	. 2 |- ( 7 + 1 ) e. RR
5	1, 4	eqeltri 2278	1 |- 8 e. RR

Syntax hints:   e. wcel 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   7c7 9094   8c8 9095

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-2 9097  df-3 9098  df-4 9099  df-5 9100  df-6 9101  df-7 9102  df-8 9103

This theorem is referenced by:  8cn  9124  9re  9125  9pos  9142  6lt8  9230  5lt8  9231  4lt8  9232  3lt8  9233  2lt8  9234  1lt8  9235  8lt9  9236  7lt9  9237  8th4div3  9258  8lt10  9637  7lt10  9638  ef01bndlem  12100  cos2bnd  12104  slotstnscsi  13060  slotsdnscsi  13088  2lgsoddprmlem1  15615  2lgsoddprmlem2  15616  2lgsoddprmlem3a  15617  2lgsoddprmlem3b  15618  2lgsoddprmlem3c  15619  2lgsoddprmlem3d  15620