Theorem 5re 9001

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 8984	. 2 |- 5 = ( 4 + 1 )
2		4re 8999	. . 3 |- 4 e. RR
3		1re 7959	. . 3 |- 1 e. RR
4	2, 3	readdcli 7973	. 2 |- ( 4 + 1 ) e. RR
5	1, 4	eqeltri 2250	1 |- 5 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5878   RRcr 7813   1c1 7815   + caddc 7817   4c4 8975   5c5 8976

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7908  ax-addrcl 7911

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8981  df-3 8982  df-4 8983  df-5 8984

This theorem is referenced by:  5cn  9002  6re  9003  6pos  9023  3lt5  9098  2lt5  9099  1lt5  9100  5lt6  9101  4lt6  9102  5lt7  9107  4lt7  9108  5lt8  9114  4lt8  9115  5lt9  9122  4lt9  9123  5lt10  9521  4lt10  9522  5recm6rec  9530  ef01bndlem  11767  vscandxnscandx  12623  slotsdifipndx  12636  slotstnscsi  12656  plendxnscandx  12669  slotsdnscsi  12680  lgsdir2lem1  14617