Theorem 5re 9114

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 9097	. 2 ⊢ 5 = (4 + 1)
2		4re 9112	. . 3 ⊢ 4 ∈ ℝ
3		1re 8070	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8084	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2277	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2175  (class class class)co 5943  ℝcr 7923  1c1 7925   + caddc 7927  4c4 9088  5c5 9089

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200  df-2 9094  df-3 9095  df-4 9096  df-5 9097

This theorem is referenced by:  5cn  9115  6re  9116  6pos  9136  3lt5  9212  2lt5  9213  1lt5  9214  5lt6  9215  4lt6  9216  5lt7  9221  4lt7  9222  5lt8  9228  4lt8  9229  5lt9  9236  4lt9  9237  5lt10  9637  4lt10  9638  5recm6rec  9646  ef01bndlem  12038  vscandxnscandx  12965  slotsdifipndx  12978  slotstnscsi  12998  plendxnscandx  13011  slotsdnscsi  13026  lgsdir2lem1  15476  gausslemma2dlem4  15512  2lgslem3  15549