Theorem 5re 9063

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 9046	. 2 ⊢ 5 = (4 + 1)
2		4re 9061	. . 3 ⊢ 4 ∈ ℝ
3		1re 8020	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8034	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2266	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873  1c1 7875   + caddc 7877  4c4 9037  5c5 9038

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189  df-2 9043  df-3 9044  df-4 9045  df-5 9046

This theorem is referenced by:  5cn  9064  6re  9065  6pos  9085  3lt5  9161  2lt5  9162  1lt5  9163  5lt6  9164  4lt6  9165  5lt7  9170  4lt7  9171  5lt8  9177  4lt8  9178  5lt9  9185  4lt9  9186  5lt10  9585  4lt10  9586  5recm6rec  9594  ef01bndlem  11902  vscandxnscandx  12782  slotsdifipndx  12795  slotstnscsi  12815  plendxnscandx  12828  slotsdnscsi  12839  lgsdir2lem1  15185  gausslemma2dlem4  15221  2lgslem3  15258