Theorem 5re 9000

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 8983	. 2 ⊢ 5 = (4 + 1)
2		4re 8998	. . 3 ⊢ 4 ∈ ℝ
3		1re 7958	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7972	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2250	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812  1c1 7814   + caddc 7816  4c4 8974  5c5 8975

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 7907  ax-addrcl 7910

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

This theorem is referenced by:  5cn  9001  6re  9002  6pos  9022  3lt5  9097  2lt5  9098  1lt5  9099  5lt6  9100  4lt6  9101  5lt7  9106  4lt7  9107  5lt8  9113  4lt8  9114  5lt9  9121  4lt9  9122  5lt10  9520  4lt10  9521  5recm6rec  9529  ef01bndlem  11766  vscandxnscandx  12622  slotsdifipndx  12635  slotstnscsi  12655  plendxnscandx  12668  slotsdnscsi  12679  lgsdir2lem1  14514