Theorem 5re 8564

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 8547	. 2 ⊢ 5 = (4 + 1)
2		4re 8562	. . 3 ⊢ 4 ∈ ℝ
3		1re 7550	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7564	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2161	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 1439  (class class class)co 5668  ℝcr 7412  1c1 7414   + caddc 7416  4c4 8538  5c5 8539

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071  ax-1re 7502  ax-addrcl 7505

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085  df-2 8544  df-3 8545  df-4 8546  df-5 8547

This theorem is referenced by:  5cn  8565  6re  8566  6pos  8586  3lt5  8655  2lt5  8656  1lt5  8657  5lt6  8658  4lt6  8659  5lt7  8664  4lt7  8665  5lt8  8671  4lt8  8672  5lt9  8679  4lt9  8680  5lt10  9074  4lt10  9075  ef01bndlem  11110