Theorem 5re 8932

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 8915	. 2 ⊢ 5 = (4 + 1)
2		4re 8930	. . 3 ⊢ 4 ∈ ℝ
3		1re 7894	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7908	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2238	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2136  (class class class)co 5841  ℝcr 7748  1c1 7750   + caddc 7752  4c4 8906  5c5 8907

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161  df-2 8912  df-3 8913  df-4 8914  df-5 8915

This theorem is referenced by:  5cn  8933  6re  8934  6pos  8954  3lt5  9029  2lt5  9030  1lt5  9031  5lt6  9032  4lt6  9033  5lt7  9038  4lt7  9039  5lt8  9045  4lt8  9046  5lt9  9053  4lt9  9054  5lt10  9452  4lt10  9453  5recm6rec  9461  ef01bndlem  11693  lgsdir2lem1  13529