Theorem 5re 12345

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 12323	. 2 ⊢ 5 = (4 + 1)
2		4re 12342	. . 3 ⊢ 4 ∈ ℝ
3		1re 11225	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11241	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2861	1 ⊢ 5 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116  1c1 11118   + caddc 11120  4c4 12314  5c5 12315

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rrecex 11189  ax-cnre 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321  df-4 12322  df-5 12323

This theorem is used by:  6re  12348  3lt5  12438  2lt5  12439  1lt5  12440  5lt6  12441  4lt6  12442  5lt7  12447  4lt7  12448  5lt8  12454  4lt8  12455  5lt9  12462  4lt9  12463  5lt10  12870  5recm6rec  12879  5eluz3  12925  5rp  13041  fz0to5un2tp  13678  ef01bndlem  16264  prm23ge5  16899  prmlem1  17191  vscandxnscandx  17401  slotsdifipndx  17412  slotstnscsi  17437  plendxnscandx  17450  slotsdnscsi  17469  ppiublem1  27419  ppiub  27421  bposlem3  27503  bposlem4  27504  bposlem5  27505  bposlem6  27506  bposlem8  27508  bposlem9  27509  lgsdir2lem1  27542  gausslemma2dlem4  27586  2lgslem3  27621  ex-id  30858  ex-sqrt  30878  threehalves  33306  cyc3conja  33543  hgt750lem2  35106  hgt750leme  35112  problem2  36197  12gcd5e1  42830  lcmineqlem23  42878  3lexlogpow2ineq1  42885  3lexlogpow2ineq2  42886  aks4d1p1p4  42898  aks4d1p1p6  42900  aks4d1p1p7  42901  aks4d1p1p5  42902  stoweidlem13  46787  goldrarr  47678  goldrasin  47679  goldrapos  47680  goldracos5teq  47682  ceil5half3  48143  modm2nep1  48169  modp2nep1  48170  modm1nep2  48171  modm1nem2  48172  modm1p1ne  48173  31prm  48409  gbegt5  48586  gbowgt5  48587  sbgoldbo  48612  nnsum3primesle9  48619  nnsum4primesodd  48621  evengpop3  48623  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  gpg5nbgrvtx13starlem2  48897  gpg5nbgr3star  48906  gpg5edgnedg  48955