Theorem 5re 8936

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 8919	. 2 |- 5 = ( 4 + 1 )
2		4re 8934	. . 3 |- 4 e. RR
3		1re 7898	. . 3 |- 1 e. RR
4	2, 3	readdcli 7912	. 2 |- ( 4 + 1 ) e. RR
5	1, 4	eqeltri 2239	1 |- 5 e. RR

Syntax hints:   e. wcel 2136  (class class class)co 5842   RRcr 7752   1c1 7754   + caddc 7756   4c4 8910   5c5 8911

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8916  df-3 8917  df-4 8918  df-5 8919

This theorem is referenced by:  5cn  8937  6re  8938  6pos  8958  3lt5  9033  2lt5  9034  1lt5  9035  5lt6  9036  4lt6  9037  5lt7  9042  4lt7  9043  5lt8  9049  4lt8  9050  5lt9  9057  4lt9  9058  5lt10  9456  4lt10  9457  5recm6rec  9465  ef01bndlem  11697  lgsdir2lem1  13569