Theorem 5re 8913

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 8896	. 2 ⊢ 5 = (4 + 1)
2		4re 8911	. . 3 ⊢ 4 ∈ ℝ
3		1re 7878	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7892	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2230	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2128  (class class class)co 5825  ℝcr 7732  1c1 7734   + caddc 7736  4c4 8887  5c5 8888

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139  ax-1re 7827  ax-addrcl 7830

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153  df-2 8893  df-3 8894  df-4 8895  df-5 8896

This theorem is referenced by:  5cn  8914  6re  8915  6pos  8935  3lt5  9010  2lt5  9011  1lt5  9012  5lt6  9013  4lt6  9014  5lt7  9019  4lt7  9020  5lt8  9026  4lt8  9027  5lt9  9034  4lt9  9035  5lt10  9430  4lt10  9431  5recm6rec  9439  ef01bndlem  11657