Theorem 5re 12470

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 12448	. 2 ⊢ 5 = (4 + 1)
2		4re 12467	. . 3 ⊢ 4 ∈ ℝ
3		1re 11347	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11363	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2860	1 ⊢ 5 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238  1c1 11240   + caddc 11242  4c4 12439  5c5 12440

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447  df-5 12448

This theorem is used by:  6re  12473  3lt5  12563  2lt5  12564  1lt5  12565  5lt6  12566  4lt6  12567  5lt7  12572  4lt7  12573  5lt8  12579  4lt8  12580  5lt9  12587  4lt9  12588  5lt10  12995  5recm6rec  13004  5eluz3  13050  5rp  13167  fz0to5un2tp  13805  ef01bndlem  16396  prm23ge5  17037  prmlem1  17329  vscandxnscandx  17541  slotsdifipndx  17552  slotstnscsi  17577  plendxnscandx  17590  slotsdnscsi  17609  ppiublem1  27586  ppiub  27588  bposlem3  27670  bposlem4  27671  bposlem5  27672  bposlem6  27673  bposlem8  27675  bposlem9  27676  lgsdir2lem1  27709  gausslemma2dlem4  27753  2lgslem3  27788  ex-id  31092  ex-sqrt  31112  threehalves  33577  cyc3conja  33817  hgt750lem2  35392  hgt750leme  35398  problem2  36639  12gcd5e1  43319  lcmineqlem23  43367  3lexlogpow2ineq1  43374  3lexlogpow2ineq2  43375  aks4d1p1p4  43387  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  stoweidlem13  47296  goldrarr  48201  goldrasin  48202  goldrapos  48203  goldracos5teq  48205  goldratval  48209  ceil5half3  48689  modm2nep1  48715  modp2nep1  48716  modm1nep2  48717  modm1nem2  48718  modm1p1ne  48719  31prm  48955  gbegt5  49132  gbowgt5  49133  sbgoldbo  49158  nnsum3primesle9  49165  nnsum4primesodd  49167  evengpop3  49169  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  gpg5nbgrvtx13starlem2  49443  gpg5nbgr3star  49452  gpg5edgnedg  49501  veronesev5lem  51405  veronesev6lem  51406  veronesevrowd  51407  veroquadgsumlem  51411