Theorem 5re 9012

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 8995	. 2 |- 5 = ( 4 + 1 )
2		4re 9010	. . 3 |- 4 e. RR
3		1re 7970	. . 3 |- 1 e. RR
4	2, 3	readdcli 7984	. 2 |- ( 4 + 1 ) e. RR
5	1, 4	eqeltri 2260	1 |- 5 e. RR

Syntax hints:   e. wcel 2158  (class class class)co 5888   RRcr 7824   1c1 7826   + caddc 7828   4c4 8986   5c5 8987

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-1re 7919  ax-addrcl 7922

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183  df-2 8992  df-3 8993  df-4 8994  df-5 8995

This theorem is referenced by:  5cn  9013  6re  9014  6pos  9034  3lt5  9109  2lt5  9110  1lt5  9111  5lt6  9112  4lt6  9113  5lt7  9118  4lt7  9119  5lt8  9125  4lt8  9126  5lt9  9133  4lt9  9134  5lt10  9532  4lt10  9533  5recm6rec  9541  ef01bndlem  11778  vscandxnscandx  12635  slotsdifipndx  12648  slotstnscsi  12668  plendxnscandx  12681  slotsdnscsi  12692  lgsdir2lem1  14725