Theorem 5re 11137

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 11120	. 2 ⊢ 5 = (4 + 1)
2		4re 11135	. . 3 ⊢ 4 ∈ ℝ
3		1re 10077	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10091	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2726	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2030  (class class class)co 6690  ℝcr 9973  1c1 9975   + caddc 9977  4c4 11110  5c5 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117  df-3 11118  df-4 11119  df-5 11120

This theorem is referenced by:  5cn  11138  6re  11139  6pos  11157  3lt5  11239  2lt5  11240  1lt5  11241  5lt6  11242  4lt6  11243  5lt7  11248  4lt7  11249  5lt8  11255  4lt8  11256  5lt9  11263  4lt9  11264  5lt10OLD  11272  4lt10OLD  11273  5lt10  11715  4lt10  11716  5recm6rec  11724  ef01bndlem  14958  prm23ge5  15567  prmlem1  15861  rmodislmod  18979  sralem  19225  srasca  19229  zlmlem  19913  zlmsca  19917  ppiublem1  24972  ppiub  24974  bposlem3  25056  bposlem4  25057  bposlem5  25058  bposlem6  25059  bposlem8  25061  bposlem9  25062  lgsdir2lem1  25095  gausslemma2dlem4  25139  2lgslem3  25174  cchhllem  25812  ex-id  27421  ex-sqrt  27441  threehalves  29751  resvvsca  29962  zlmds  30136  zlmtset  30137  hgt750lem2  30858  hgt750leme  30864  problem2  31685  problem2OLD  31686  stoweidlem13  40548  31prm  41837  gbegt5  41974  gbowgt5  41975  sbgoldbo  42000  nnsum3primesle9  42007  nnsum4primesodd  42009  evengpop3  42011