Theorem 5re 7994

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 7976	. 2 ⊢ 5 = (4 + 1)
2		4re 7992	. . 3 ⊢ 4 ∈ ℝ
3		1re 7026	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7040	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2110	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 1393  (class class class)co 5512  ℝcr 6888  1c1 6890   + caddc 6892  4c4 7966  5c5 7967

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-1re 6978  ax-addrcl 6981

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-2 7973  df-3 7974  df-4 7975  df-5 7976

This theorem is referenced by:  5cn  7995  6re  7996  6pos  8017  3lt5  8093  2lt5  8094  1lt5  8095  5lt6  8096  4lt6  8097  5lt7  8102  4lt7  8103  5lt8  8109  4lt8  8110  5lt9  8117  4lt9  8118  5lt10  8126  4lt10  8127