Theorem 5re 8994

Description: The number 5 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
5re	⊢ 5 ∈ ℝ

Proof of Theorem 5re

Step	Hyp	Ref	Expression
1		df-5 8977	. 2 ⊢ 5 = (4 + 1)
2		4re 8992	. . 3 ⊢ 4 ∈ ℝ
3		1re 7953	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7967	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2250	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5872  ℝcr 7807  1c1 7809   + caddc 7811  4c4 8968  5c5 8969

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 7902  ax-addrcl 7905

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8974  df-3 8975  df-4 8976  df-5 8977

This theorem is referenced by:  5cn  8995  6re  8996  6pos  9016  3lt5  9091  2lt5  9092  1lt5  9093  5lt6  9094  4lt6  9095  5lt7  9100  4lt7  9101  5lt8  9107  4lt8  9108  5lt9  9115  4lt9  9116  5lt10  9514  4lt10  9515  5recm6rec  9523  ef01bndlem  11757  vscandxnscandx  12612  slotsdifipndx  12625  slotstnscsi  12642  plendxnscandx  12655  slotsdnscsi  12666  lgsdir2lem1  14300