Theorem 5re 9117

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

Syntax hints:   e. wcel 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   4c4 9091   5c5 9092

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

This theorem is referenced by:  5cn  9118  6re  9119  6pos  9139  3lt5  9215  2lt5  9216  1lt5  9217  5lt6  9218  4lt6  9219  5lt7  9224  4lt7  9225  5lt8  9231  4lt8  9232  5lt9  9239  4lt9  9240  5lt10  9640  4lt10  9641  5recm6rec  9649  ef01bndlem  12100  vscandxnscandx  13027  slotsdifipndx  13040  slotstnscsi  13060  plendxnscandx  13073  slotsdnscsi  13088  lgsdir2lem1  15538  gausslemma2dlem4  15574  2lgslem3  15611