Theorem 5re 12268

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 12247	. 2 ⊢ 5 = (4 + 1)
2		4re 12265	. . 3 ⊢ 4 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  4c4 12238  5c5 12239

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 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247

This theorem is referenced by:  6re  12271  6pos  12291  3lt5  12354  2lt5  12355  1lt5  12356  5lt6  12357  4lt6  12358  5lt7  12363  4lt7  12364  5lt8  12370  4lt8  12371  5lt9  12378  4lt9  12379  5lt10  12779  4lt10  12780  5recm6rec  12787  5eluz3  12833  5rp  12949  fz0to5un2tp  13585  ef01bndlem  16151  prm23ge5  16786  prmlem1  17078  vscandxnscandx  17287  slotsdifipndx  17298  slotstnscsi  17323  plendxnscandx  17336  slotsdnscsi  17355  ppiublem1  27165  ppiub  27167  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  gausslemma2dlem4  27332  2lgslem3  27367  ex-id  30504  ex-sqrt  30524  threehalves  32974  cyc3conja  33218  hgt750lem2  34796  hgt750leme  34802  problem2  35848  12gcd5e1  42442  lcmineqlem23  42490  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  stoweidlem13  46441  goldrarr  47329  goldrasin  47330  goldrapos  47331  goldracos5teq  47333  ceil5half3  47794  modm2nep1  47820  modp2nep1  47821  modm1nep2  47822  modm1nem2  47823  modm1p1ne  47824  31prm  48060  gbegt5  48237  gbowgt5  48238  sbgoldbo  48263  nnsum3primesle9  48270  nnsum4primesodd  48272  evengpop3  48274  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  gpg5nbgrvtx13starlem2  48548  gpg5nbgr3star  48557  gpg5edgnedg  48606