Theorem 8re 8805

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 8785	. 2 |- 8 = ( 7 + 1 )
2		7re 8803	. . 3 |- 7 e. RR
3		1re 7765	. . 3 |- 1 e. RR
4	2, 3	readdcli 7779	. 2 |- ( 7 + 1 ) e. RR
5	1, 4	eqeltri 2212	1 |- 8 e. RR

Syntax hints:   e. wcel 1480  (class class class)co 5774   RRcr 7619   1c1 7621   + caddc 7623   7c7 8776   8c8 8777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1re 7714  ax-addrcl 7717

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-2 8779  df-3 8780  df-4 8781  df-5 8782  df-6 8783  df-7 8784  df-8 8785

This theorem is referenced by:  8cn  8806  9re  8807  9pos  8824  6lt8  8911  5lt8  8912  4lt8  8913  3lt8  8914  2lt8  8915  1lt8  8916  8lt9  8917  7lt9  8918  8th4div3  8939  8lt10  9313  7lt10  9314  ef01bndlem  11463  cos2bnd  11467