Theorem 5re 9086

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 9069	. 2 ⊢ 5 = (4 + 1)
2		4re 9084	. . 3 ⊢ 4 ∈ ℝ
3		1re 8042	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8056	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2269	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  ℝcr 7895  1c1 7897   + caddc 7899  4c4 9060  5c5 9061

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 7990  ax-addrcl 7993

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

This theorem is referenced by:  5cn  9087  6re  9088  6pos  9108  3lt5  9184  2lt5  9185  1lt5  9186  5lt6  9187  4lt6  9188  5lt7  9193  4lt7  9194  5lt8  9200  4lt8  9201  5lt9  9208  4lt9  9209  5lt10  9608  4lt10  9609  5recm6rec  9617  ef01bndlem  11938  vscandxnscandx  12864  slotsdifipndx  12877  slotstnscsi  12897  plendxnscandx  12910  slotsdnscsi  12925  lgsdir2lem1  15353  gausslemma2dlem4  15389  2lgslem3  15426