Theorem 5re 12430

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 12408	. 2 ⊢ 5 = (4 + 1)
2		4re 12427	. . 3 ⊢ 4 ∈ ℝ
3		1re 11308	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2857	1 ⊢ 5 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203  4c4 12399  5c5 12400

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 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408

This theorem is used by:  6re  12433  3lt5  12523  2lt5  12524  1lt5  12525  5lt6  12526  4lt6  12527  5lt7  12532  4lt7  12533  5lt8  12539  4lt8  12540  5lt9  12547  4lt9  12548  5lt10  12955  5recm6rec  12964  5eluz3  13010  5rp  13127  fz0to5un2tp  13765  ef01bndlem  16352  prm23ge5  16993  prmlem1  17285  vscandxnscandx  17495  slotsdifipndx  17506  slotstnscsi  17531  plendxnscandx  17544  slotsdnscsi  17563  ppiublem1  27529  ppiub  27531  bposlem3  27613  bposlem4  27614  bposlem5  27615  bposlem6  27616  bposlem8  27618  bposlem9  27619  lgsdir2lem1  27652  gausslemma2dlem4  27696  2lgslem3  27731  ex-id  31035  ex-sqrt  31055  threehalves  33481  cyc3conja  33718  hgt750lem2  35281  hgt750leme  35287  problem2  36431  12gcd5e1  43053  lcmineqlem23  43101  3lexlogpow2ineq1  43108  3lexlogpow2ineq2  43109  aks4d1p1p4  43121  aks4d1p1p6  43123  aks4d1p1p7  43124  aks4d1p1p5  43125  stoweidlem13  47022  goldrarr  47927  goldrasin  47928  goldrapos  47929  goldracos5teq  47931  goldratval  47935  ceil5half3  48415  modm2nep1  48441  modp2nep1  48442  modm1nep2  48443  modm1nem2  48444  modm1p1ne  48445  31prm  48681  gbegt5  48858  gbowgt5  48859  sbgoldbo  48884  nnsum3primesle9  48891  nnsum4primesodd  48893  evengpop3  48895  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  gpg5nbgrvtx13starlem2  49169  gpg5nbgr3star  49178  gpg5edgnedg  49227  veronesev5lem  50976  veronesev6lem  50977  veronesevrowd  50978  veroquadgsumlem  50982