Theorem 5re 12355

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 12333	. 2 ⊢ 5 = (4 + 1)
2		4re 12352	. . 3 ⊢ 4 ∈ ℝ
3		1re 11235	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11251	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2856	1 ⊢ 5 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126  1c1 11128   + caddc 11130  4c4 12324  5c5 12325

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 2732  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7417  df-2 12330  df-3 12331  df-4 12332  df-5 12333

This theorem is used by:  6re  12358  3lt5  12448  2lt5  12449  1lt5  12450  5lt6  12451  4lt6  12452  5lt7  12457  4lt7  12458  5lt8  12464  4lt8  12465  5lt9  12472  4lt9  12473  5lt10  12880  5recm6rec  12889  5eluz3  12935  5rp  13052  fz0to5un2tp  13689  ef01bndlem  16275  prm23ge5  16910  prmlem1  17202  vscandxnscandx  17412  slotsdifipndx  17423  slotstnscsi  17448  plendxnscandx  17461  slotsdnscsi  17480  ppiublem1  27441  ppiub  27443  bposlem3  27525  bposlem4  27526  bposlem5  27527  bposlem6  27528  bposlem8  27530  bposlem9  27531  lgsdir2lem1  27564  gausslemma2dlem4  27608  2lgslem3  27643  ex-id  30917  ex-sqrt  30937  threehalves  33363  cyc3conja  33600  hgt750lem2  35163  hgt750leme  35169  problem2  36248  12gcd5e1  42872  lcmineqlem23  42920  3lexlogpow2ineq1  42927  3lexlogpow2ineq2  42928  aks4d1p1p4  42940  aks4d1p1p6  42942  aks4d1p1p7  42943  aks4d1p1p5  42944  stoweidlem13  46844  goldrarr  47749  goldrasin  47750  goldrapos  47751  goldracos5teq  47753  goldratval  47757  ceil5half3  48237  modm2nep1  48263  modp2nep1  48264  modm1nep2  48265  modm1nem2  48266  modm1p1ne  48267  31prm  48503  gbegt5  48680  gbowgt5  48681  sbgoldbo  48706  nnsum3primesle9  48713  nnsum4primesodd  48715  evengpop3  48717  usgrexmpl1lem  48940  usgrexmpl2lem  48945  usgrexmpl2nb4  48954  usgrexmpl2nb5  48955  gpg5nbgrvtx13starlem2  48991  gpg5nbgr3star  49000  gpg5edgnedg  49049  veronesev5lem  50813  veronesev6lem  50814  veronesevrowd  50815  veroquadgsumlem  50819