Theorem 5re 9150

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 9133	. 2 ⊢ 5 = (4 + 1)
2		4re 9148	. . 3 ⊢ 4 ∈ ℝ
3		1re 8106	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8120	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2280	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2178  (class class class)co 5967  ℝcr 7959  1c1 7961   + caddc 7963  4c4 9124  5c5 9125

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203  df-2 9130  df-3 9131  df-4 9132  df-5 9133

This theorem is referenced by:  5cn  9151  6re  9152  6pos  9172  3lt5  9248  2lt5  9249  1lt5  9250  5lt6  9251  4lt6  9252  5lt7  9257  4lt7  9258  5lt8  9264  4lt8  9265  5lt9  9272  4lt9  9273  5lt10  9673  4lt10  9674  5recm6rec  9682  ef01bndlem  12182  vscandxnscandx  13109  slotsdifipndx  13122  slotstnscsi  13142  plendxnscandx  13155  slotsdnscsi  13170  lgsdir2lem1  15620  gausslemma2dlem4  15656  2lgslem3  15693