Theorem 5re 12280

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 12259	. 2 ⊢ 5 = (4 + 1)
2		4re 12277	. . 3 ⊢ 4 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11196	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2825	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074  1c1 11076   + caddc 11078  4c4 12250  5c5 12251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257  df-4 12258  df-5 12259

This theorem is referenced by:  6re  12283  6pos  12303  3lt5  12366  2lt5  12367  1lt5  12368  5lt6  12369  4lt6  12370  5lt7  12375  4lt7  12376  5lt8  12382  4lt8  12383  5lt9  12390  4lt9  12391  5lt10  12791  4lt10  12792  5recm6rec  12799  5eluz3  12849  5rp  12965  fz0to5un2tp  13599  ef01bndlem  16159  prm23ge5  16793  prmlem1  17085  vscandxnscandx  17294  slotsdifipndx  17305  slotstnscsi  17330  plendxnscandx  17343  slotsdnscsi  17362  ppiublem1  27120  ppiub  27122  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem8  27209  bposlem9  27210  lgsdir2lem1  27243  gausslemma2dlem4  27287  2lgslem3  27322  ex-id  30370  ex-sqrt  30390  threehalves  32842  cyc3conja  33121  hgt750lem2  34650  hgt750leme  34656  problem2  35660  12gcd5e1  41998  lcmineqlem23  42046  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  stoweidlem13  46018  ceil5half3  47345  modm2nep1  47371  modp2nep1  47372  modm1nep2  47373  modm1nem2  47374  modm1p1ne  47375  31prm  47602  gbegt5  47766  gbowgt5  47767  sbgoldbo  47792  nnsum3primesle9  47799  nnsum4primesodd  47801  evengpop3  47803  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  gpg5nbgrvtx13starlem2  48067  gpg5nbgr3star  48076