Theorem 5re 12350

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 12329	. 2 ⊢ 5 = (4 + 1)
2		4re 12347	. . 3 ⊢ 4 ∈ ℝ
3		1re 11258	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11273	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2834	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151  1c1 11153   + caddc 11155  4c4 12320  5c5 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326  df-3 12327  df-4 12328  df-5 12329

This theorem is referenced by:  6re  12353  6pos  12373  3lt5  12441  2lt5  12442  1lt5  12443  5lt6  12444  4lt6  12445  5lt7  12450  4lt7  12451  5lt8  12457  4lt8  12458  5lt9  12465  4lt9  12466  5lt10  12865  4lt10  12866  5recm6rec  12874  5eluz3  12924  5rp  13038  fz0to5un2tp  13667  ef01bndlem  16216  prm23ge5  16848  prmlem1  17141  vscandxnscandx  17369  slotsdifipndx  17380  slotstnscsi  17405  plendxnscandx  17418  slotsdnscsi  17437  rmodislmodOLD  20945  sralemOLD  21193  srascaOLD  21201  zlmlemOLD  21545  ppiublem1  27260  ppiub  27262  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem8  27349  bposlem9  27350  lgsdir2lem1  27383  gausslemma2dlem4  27427  2lgslem3  27462  cchhllemOLD  28916  ex-id  30462  ex-sqrt  30482  threehalves  32881  cyc3conja  33159  resvvscaOLD  33343  zlmdsOLD  33923  zlmtsetOLD  33925  hgt750lem2  34645  hgt750leme  34651  problem2  35650  12gcd5e1  41984  lcmineqlem23  42032  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  stoweidlem13  45968  ceil5half3  47279  31prm  47521  gbegt5  47685  gbowgt5  47686  sbgoldbo  47711  nnsum3primesle9  47718  nnsum4primesodd  47720  evengpop3  47722  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  gpg5nbgrvtx13starlem2  47962  gpg5nbgr3star  47971