Theorem 5re 12212

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 12191	. 2 ⊢ 5 = (4 + 1)
2		4re 12209	. . 3 ⊢ 4 ∈ ℝ
3		1re 11112	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11127	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005  1c1 11007   + caddc 11009  4c4 12182  5c5 12183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-2 12188  df-3 12189  df-4 12190  df-5 12191

This theorem is referenced by:  6re  12215  6pos  12235  3lt5  12298  2lt5  12299  1lt5  12300  5lt6  12301  4lt6  12302  5lt7  12307  4lt7  12308  5lt8  12314  4lt8  12315  5lt9  12322  4lt9  12323  5lt10  12723  4lt10  12724  5recm6rec  12731  5eluz3  12781  5rp  12897  fz0to5un2tp  13531  ef01bndlem  16093  prm23ge5  16727  prmlem1  17019  vscandxnscandx  17228  slotsdifipndx  17239  slotstnscsi  17264  plendxnscandx  17277  slotsdnscsi  17296  ppiublem1  27140  ppiub  27142  bposlem3  27224  bposlem4  27225  bposlem5  27226  bposlem6  27227  bposlem8  27229  bposlem9  27230  lgsdir2lem1  27263  gausslemma2dlem4  27307  2lgslem3  27342  ex-id  30414  ex-sqrt  30434  threehalves  32895  cyc3conja  33126  hgt750lem2  34665  hgt750leme  34671  problem2  35710  12gcd5e1  42106  lcmineqlem23  42154  3lexlogpow2ineq1  42161  3lexlogpow2ineq2  42162  aks4d1p1p4  42174  aks4d1p1p6  42176  aks4d1p1p7  42177  aks4d1p1p5  42178  stoweidlem13  46121  ceil5half3  47450  modm2nep1  47476  modp2nep1  47477  modm1nep2  47478  modm1nem2  47479  modm1p1ne  47480  31prm  47707  gbegt5  47871  gbowgt5  47872  sbgoldbo  47897  nnsum3primesle9  47904  nnsum4primesodd  47906  evengpop3  47908  usgrexmpl1lem  48131  usgrexmpl2lem  48136  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146  gpg5nbgrvtx13starlem2  48182  gpg5nbgr3star  48191  gpg5edgnedg  48240