Theorem 5re 8792

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 8775	. 2 ⊢ 5 = (4 + 1)
2		4re 8790	. . 3 ⊢ 4 ∈ ℝ
3		1re 7758	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7772	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2210	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612  1c1 7614   + caddc 7616  4c4 8766  5c5 8767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1re 7707  ax-addrcl 7710

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-2 8772  df-3 8773  df-4 8774  df-5 8775

This theorem is referenced by:  5cn  8793  6re  8794  6pos  8814  3lt5  8889  2lt5  8890  1lt5  8891  5lt6  8892  4lt6  8893  5lt7  8898  4lt7  8899  5lt8  8905  4lt8  8906  5lt9  8913  4lt9  8914  5lt10  9309  4lt10  9310  5recm6rec  9318  ef01bndlem  11452