Theorem 5re 9088

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 9071	. 2 ⊢ 5 = (4 + 1)
2		4re 9086	. . 3 ⊢ 4 ∈ ℝ
3		1re 8044	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8058	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2269	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℝcr 7897  1c1 7899   + caddc 7901  4c4 9062  5c5 9063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9068  df-3 9069  df-4 9070  df-5 9071

This theorem is referenced by:  5cn  9089  6re  9090  6pos  9110  3lt5  9186  2lt5  9187  1lt5  9188  5lt6  9189  4lt6  9190  5lt7  9195  4lt7  9196  5lt8  9202  4lt8  9203  5lt9  9210  4lt9  9211  5lt10  9610  4lt10  9611  5recm6rec  9619  ef01bndlem  11940  vscandxnscandx  12866  slotsdifipndx  12879  slotstnscsi  12899  plendxnscandx  12912  slotsdnscsi  12927  lgsdir2lem1  15377  gausslemma2dlem4  15413  2lgslem3  15450