Theorem 5re 9281

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 9264	. 2 |- 5 = ( 4 + 1 )
2		4re 9279	. . 3 |- 4 e. RR
3		1re 8238	. . 3 |- 1 e. RR
4	2, 3	readdcli 8252	. 2 |- ( 4 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 5 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6028   RRcr 8091   1c1 8093   + caddc 8095   4c4 9255   5c5 9256

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 2213  ax-1re 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9261  df-3 9262  df-4 9263  df-5 9264

This theorem is referenced by:  5cn  9282  6re  9283  6pos  9303  3lt5  9379  2lt5  9380  1lt5  9381  5lt6  9382  4lt6  9383  5lt7  9388  4lt7  9389  5lt8  9395  4lt8  9396  5lt9  9403  4lt9  9404  5lt10  9806  4lt10  9807  5recm6rec  9815  5eluz3  9856  ef01bndlem  12397  vscandxnscandx  13325  slotsdifipndx  13338  slotstnscsi  13358  plendxnscandx  13371  slotsdnscsi  13386  lgsdir2lem1  15847  gausslemma2dlem4  15883  2lgslem3  15920