Theorem 5re 8799

Description: The number 5 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
5re	|- 5 e. RR

Proof of Theorem 5re

Step	Hyp	Ref	Expression
1		df-5 8782	. 2 |- 5 = ( 4 + 1 )
2		4re 8797	. . 3 |- 4 e. RR
3		1re 7765	. . 3 |- 1 e. RR
4	2, 3	readdcli 7779	. 2 |- ( 4 + 1 ) e. RR
5	1, 4	eqeltri 2212	1 |- 5 e. RR

Syntax hints:   e. wcel 1480  (class class class)co 5774   RRcr 7619   1c1 7621   + caddc 7623   4c4 8773   5c5 8774

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

This theorem is referenced by:  5cn  8800  6re  8801  6pos  8821  3lt5  8896  2lt5  8897  1lt5  8898  5lt6  8899  4lt6  8900  5lt7  8905  4lt7  8906  5lt8  8912  4lt8  8913  5lt9  8920  4lt9  8921  5lt10  9316  4lt10  9317  5recm6rec  9325  ef01bndlem  11463