Theorem 5re 8957

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 8940	. 2 ⊢ 5 = (4 + 1)
2		4re 8955	. . 3 ⊢ 4 ∈ ℝ
3		1re 7919	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 7933	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2243	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2141  (class class class)co 5853  ℝcr 7773  1c1 7775   + caddc 7777  4c4 8931  5c5 8932

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-2 8937  df-3 8938  df-4 8939  df-5 8940

This theorem is referenced by:  5cn  8958  6re  8959  6pos  8979  3lt5  9054  2lt5  9055  1lt5  9056  5lt6  9057  4lt6  9058  5lt7  9063  4lt7  9064  5lt8  9070  4lt8  9071  5lt9  9078  4lt9  9079  5lt10  9477  4lt10  9478  5recm6rec  9486  ef01bndlem  11719  lgsdir2lem1  13723