Theorem 5re 12262

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 12241	. 2 ⊢ 5 = (4 + 1)
2		4re 12259	. . 3 ⊢ 4 ∈ ℝ
3		1re 11138	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11154	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  4c4 12232  5c5 12233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240  df-5 12241

This theorem is referenced by:  6re  12265  6pos  12285  3lt5  12348  2lt5  12349  1lt5  12350  5lt6  12351  4lt6  12352  5lt7  12357  4lt7  12358  5lt8  12364  4lt8  12365  5lt9  12372  4lt9  12373  5lt10  12773  4lt10  12774  5recm6rec  12781  5eluz3  12827  5rp  12943  fz0to5un2tp  13579  ef01bndlem  16145  prm23ge5  16780  prmlem1  17072  vscandxnscandx  17281  slotsdifipndx  17292  slotstnscsi  17317  plendxnscandx  17330  slotsdnscsi  17349  ppiublem1  27182  ppiub  27184  bposlem3  27266  bposlem4  27267  bposlem5  27268  bposlem6  27269  bposlem8  27271  bposlem9  27272  lgsdir2lem1  27305  gausslemma2dlem4  27349  2lgslem3  27384  ex-id  30522  ex-sqrt  30542  threehalves  32992  cyc3conja  33236  hgt750lem2  34815  hgt750leme  34821  problem2  35867  12gcd5e1  42459  lcmineqlem23  42507  3lexlogpow2ineq1  42514  3lexlogpow2ineq2  42515  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  stoweidlem13  46462  goldrarr  47346  goldrasin  47347  goldrapos  47348  ceil5half3  47809  modm2nep1  47835  modp2nep1  47836  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  31prm  48075  gbegt5  48252  gbowgt5  48253  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primesodd  48287  evengpop3  48289  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  gpg5nbgrvtx13starlem2  48563  gpg5nbgr3star  48572  gpg5edgnedg  48621