Theorem 5re 9205

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 9188	. 2 ⊢ 5 = (4 + 1)
2		4re 9203	. . 3 ⊢ 4 ∈ ℝ
3		1re 8161	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 8175	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2302	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6010  ℝcr 8014  1c1 8016   + caddc 8018  4c4 9179  5c5 9180

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8109  ax-addrcl 8112

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9185  df-3 9186  df-4 9187  df-5 9188

This theorem is referenced by:  5cn  9206  6re  9207  6pos  9227  3lt5  9303  2lt5  9304  1lt5  9305  5lt6  9306  4lt6  9307  5lt7  9312  4lt7  9313  5lt8  9319  4lt8  9320  5lt9  9327  4lt9  9328  5lt10  9728  4lt10  9729  5recm6rec  9737  ef01bndlem  12288  vscandxnscandx  13216  slotsdifipndx  13229  slotstnscsi  13249  plendxnscandx  13262  slotsdnscsi  13277  lgsdir2lem1  15728  gausslemma2dlem4  15764  2lgslem3  15801