Theorem 5re 12327

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 12306	. 2 ⊢ 5 = (4 + 1)
2		4re 12324	. . 3 ⊢ 4 ∈ ℝ
3		1re 11235	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11250	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7405  ℝcr 11128  1c1 11130   + caddc 11132  4c4 12297  5c5 12298

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-i2m1 11197  ax-1ne0 11198  ax-rrecex 11201  ax-cnre 11202

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-2 12303  df-3 12304  df-4 12305  df-5 12306

This theorem is referenced by:  6re  12330  6pos  12350  3lt5  12418  2lt5  12419  1lt5  12420  5lt6  12421  4lt6  12422  5lt7  12427  4lt7  12428  5lt8  12434  4lt8  12435  5lt9  12442  4lt9  12443  5lt10  12843  4lt10  12844  5recm6rec  12851  5eluz3  12901  5rp  13015  fz0to5un2tp  13648  ef01bndlem  16202  prm23ge5  16835  prmlem1  17127  vscandxnscandx  17338  slotsdifipndx  17349  slotstnscsi  17374  plendxnscandx  17387  slotsdnscsi  17406  ppiublem1  27165  ppiub  27167  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  gausslemma2dlem4  27332  2lgslem3  27367  ex-id  30415  ex-sqrt  30435  threehalves  32889  cyc3conja  33168  hgt750lem2  34684  hgt750leme  34690  problem2  35688  12gcd5e1  42016  lcmineqlem23  42064  3lexlogpow2ineq1  42071  3lexlogpow2ineq2  42072  aks4d1p1p4  42084  aks4d1p1p6  42086  aks4d1p1p7  42087  aks4d1p1p5  42088  stoweidlem13  46042  ceil5half3  47369  31prm  47611  gbegt5  47775  gbowgt5  47776  sbgoldbo  47801  nnsum3primesle9  47808  nnsum4primesodd  47810  evengpop3  47812  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  gpg5nbgrvtx13starlem2  48074  gpg5nbgr3star  48083