Theorem 5re 12230

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 12209	. 2 ⊢ 5 = (4 + 1)
2		4re 12227	. . 3 ⊢ 4 ∈ ℝ
3		1re 11130	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11145	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023  1c1 11025   + caddc 11027  4c4 12200  5c5 12201

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 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rrecex 11096  ax-cnre 11097

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 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206  df-3 12207  df-4 12208  df-5 12209

This theorem is referenced by:  6re  12233  6pos  12253  3lt5  12316  2lt5  12317  1lt5  12318  5lt6  12319  4lt6  12320  5lt7  12325  4lt7  12326  5lt8  12332  4lt8  12333  5lt9  12340  4lt9  12341  5lt10  12740  4lt10  12741  5recm6rec  12748  5eluz3  12794  5rp  12910  fz0to5un2tp  13545  ef01bndlem  16107  prm23ge5  16741  prmlem1  17033  vscandxnscandx  17242  slotsdifipndx  17253  slotstnscsi  17278  plendxnscandx  17291  slotsdnscsi  17310  ppiublem1  27167  ppiub  27169  bposlem3  27251  bposlem4  27252  bposlem5  27253  bposlem6  27254  bposlem8  27256  bposlem9  27257  lgsdir2lem1  27290  gausslemma2dlem4  27334  2lgslem3  27369  ex-id  30458  ex-sqrt  30478  threehalves  32945  cyc3conja  33188  hgt750lem2  34758  hgt750leme  34764  problem2  35809  12gcd5e1  42196  lcmineqlem23  42244  3lexlogpow2ineq1  42251  3lexlogpow2ineq2  42252  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  stoweidlem13  46199  ceil5half3  47528  modm2nep1  47554  modp2nep1  47555  modm1nep2  47556  modm1nem2  47557  modm1p1ne  47558  31prm  47785  gbegt5  47949  gbowgt5  47950  sbgoldbo  47975  nnsum3primesle9  47982  nnsum4primesodd  47984  evengpop3  47986  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  gpg5nbgrvtx13starlem2  48260  gpg5nbgr3star  48269  gpg5edgnedg  48318