Theorem 5re 12232

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 12211	. 2 ⊢ 5 = (4 + 1)
2		4re 12229	. . 3 ⊢ 4 ∈ ℝ
3		1re 11132	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11147	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029  4c4 12202  5c5 12203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208  df-3 12209  df-4 12210  df-5 12211

This theorem is referenced by:  6re  12235  6pos  12255  3lt5  12318  2lt5  12319  1lt5  12320  5lt6  12321  4lt6  12322  5lt7  12327  4lt7  12328  5lt8  12334  4lt8  12335  5lt9  12342  4lt9  12343  5lt10  12742  4lt10  12743  5recm6rec  12750  5eluz3  12796  5rp  12912  fz0to5un2tp  13547  ef01bndlem  16109  prm23ge5  16743  prmlem1  17035  vscandxnscandx  17244  slotsdifipndx  17255  slotstnscsi  17280  plendxnscandx  17293  slotsdnscsi  17312  ppiublem1  27169  ppiub  27171  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  gausslemma2dlem4  27336  2lgslem3  27371  ex-id  30509  ex-sqrt  30529  threehalves  32996  cyc3conja  33239  hgt750lem2  34809  hgt750leme  34815  problem2  35860  12gcd5e1  42267  lcmineqlem23  42315  3lexlogpow2ineq1  42322  3lexlogpow2ineq2  42323  aks4d1p1p4  42335  aks4d1p1p6  42337  aks4d1p1p7  42338  aks4d1p1p5  42339  stoweidlem13  46267  ceil5half3  47596  modm2nep1  47622  modp2nep1  47623  modm1nep2  47624  modm1nem2  47625  modm1p1ne  47626  31prm  47853  gbegt5  48017  gbowgt5  48018  sbgoldbo  48043  nnsum3primesle9  48050  nnsum4primesodd  48052  evengpop3  48054  usgrexmpl1lem  48277  usgrexmpl2lem  48282  usgrexmpl2nb4  48291  usgrexmpl2nb5  48292  gpg5nbgrvtx13starlem2  48328  gpg5nbgr3star  48337  gpg5edgnedg  48386