Theorem 5re 9316

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 9299	. 2 |- 5 = ( 4 + 1 )
2		4re 9314	. . 3 |- 4 e. RR
3		1re 8273	. . 3 |- 1 e. RR
4	2, 3	readdcli 8287	. 2 |- ( 4 + 1 ) e. RR
5	1, 4	eqeltri 2305	1 |- 5 e. RR

Syntax hints:   e. wcel 2203  (class class class)co 6050   RRcr 8126   1c1 8128   + caddc 8130   4c4 9290   5c5 9291

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228  df-2 9296  df-3 9297  df-4 9298  df-5 9299

This theorem is referenced by:  5cn  9317  6re  9318  6pos  9338  3lt5  9414  2lt5  9415  1lt5  9416  5lt6  9417  4lt6  9418  5lt7  9423  4lt7  9424  5lt8  9430  4lt8  9431  5lt9  9438  4lt9  9439  5lt10  9843  4lt10  9844  5recm6rec  9852  5eluz3  9893  ef01bndlem  12442  vscandxnscandx  13375  slotsdifipndx  13388  slotstnscsi  13408  plendxnscandx  13421  slotsdnscsi  13436  lgsdir2lem1  15901  gausslemma2dlem4  15937  2lgslem3  15974