Theorem 5re 12440

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 12418	. 2 ⊢ 5 = (4 + 1)
2		4re 12437	. . 3 ⊢ 4 ∈ ℝ
3		1re 11318	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11334	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 5 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209  1c1 11211   + caddc 11213  4c4 12409  5c5 12410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-i2m1 11278  ax-1ne0 11279  ax-rrecex 11282  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415  df-3 12416  df-4 12417  df-5 12418

This theorem is used by:  6re  12443  3lt5  12533  2lt5  12534  1lt5  12535  5lt6  12536  4lt6  12537  5lt7  12542  4lt7  12543  5lt8  12549  4lt8  12550  5lt9  12557  4lt9  12558  5lt10  12965  5recm6rec  12974  5eluz3  13020  5rp  13137  fz0to5un2tp  13775  ef01bndlem  16364  prm23ge5  17005  prmlem1  17297  vscandxnscandx  17507  slotsdifipndx  17518  slotstnscsi  17543  plendxnscandx  17556  slotsdnscsi  17575  ppiublem1  27541  ppiub  27543  bposlem3  27625  bposlem4  27626  bposlem5  27627  bposlem6  27628  bposlem8  27630  bposlem9  27631  lgsdir2lem1  27664  gausslemma2dlem4  27708  2lgslem3  27743  ex-id  31047  ex-sqrt  31067  threehalves  33534  cyc3conja  33771  hgt750lem2  35334  hgt750leme  35340  problem2  36552  12gcd5e1  43193  lcmineqlem23  43241  3lexlogpow2ineq1  43248  3lexlogpow2ineq2  43249  aks4d1p1p4  43261  aks4d1p1p6  43263  aks4d1p1p7  43264  aks4d1p1p5  43265  stoweidlem13  47162  goldrarr  48067  goldrasin  48068  goldrapos  48069  goldracos5teq  48071  goldratval  48075  ceil5half3  48555  modm2nep1  48581  modp2nep1  48582  modm1nep2  48583  modm1nem2  48584  modm1p1ne  48585  31prm  48821  gbegt5  48998  gbowgt5  48999  sbgoldbo  49024  nnsum3primesle9  49031  nnsum4primesodd  49033  evengpop3  49035  usgrexmpl1lem  49258  usgrexmpl2lem  49263  usgrexmpl2nb4  49272  usgrexmpl2nb5  49273  gpg5nbgrvtx13starlem2  49309  gpg5nbgr3star  49318  gpg5edgnedg  49367  veronesev5lem  51191  veronesev6lem  51192  veronesevrowd  51193  veroquadgsumlem  51197