Theorem 5re 9069

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 9052	. 2 ⊢ 5 = (4 + 1)
2		4re 9067	. . 3 ⊢ 4 ∈ ℝ
3		1re 8025	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8039	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2269	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2167  (class class class)co 5922  ℝcr 7878  1c1 7880   + caddc 7882  4c4 9043  5c5 9044

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 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9049  df-3 9050  df-4 9051  df-5 9052

This theorem is referenced by:  5cn  9070  6re  9071  6pos  9091  3lt5  9167  2lt5  9168  1lt5  9169  5lt6  9170  4lt6  9171  5lt7  9176  4lt7  9177  5lt8  9183  4lt8  9184  5lt9  9191  4lt9  9192  5lt10  9591  4lt10  9592  5recm6rec  9600  ef01bndlem  11921  vscandxnscandx  12839  slotsdifipndx  12852  slotstnscsi  12872  plendxnscandx  12885  slotsdnscsi  12896  lgsdir2lem1  15269  gausslemma2dlem4  15305  2lgslem3  15342