Theorem 5re 12215

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 12194	. 2 ⊢ 5 = (4 + 1)
2		4re 12212	. . 3 ⊢ 4 ∈ ℝ
3		1re 11115	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11130	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012  4c4 12185  5c5 12186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193  df-5 12194

This theorem is referenced by:  6re  12218  6pos  12238  3lt5  12301  2lt5  12302  1lt5  12303  5lt6  12304  4lt6  12305  5lt7  12310  4lt7  12311  5lt8  12317  4lt8  12318  5lt9  12325  4lt9  12326  5lt10  12726  4lt10  12727  5recm6rec  12734  5eluz3  12784  5rp  12900  fz0to5un2tp  13534  ef01bndlem  16093  prm23ge5  16727  prmlem1  17019  vscandxnscandx  17228  slotsdifipndx  17239  slotstnscsi  17264  plendxnscandx  17277  slotsdnscsi  17296  ppiublem1  27111  ppiub  27113  bposlem3  27195  bposlem4  27196  bposlem5  27197  bposlem6  27198  bposlem8  27200  bposlem9  27201  lgsdir2lem1  27234  gausslemma2dlem4  27278  2lgslem3  27313  ex-id  30378  ex-sqrt  30398  threehalves  32855  cyc3conja  33099  hgt750lem2  34620  hgt750leme  34626  problem2  35643  12gcd5e1  41980  lcmineqlem23  42028  3lexlogpow2ineq1  42035  3lexlogpow2ineq2  42036  aks4d1p1p4  42048  aks4d1p1p6  42050  aks4d1p1p7  42051  aks4d1p1p5  42052  stoweidlem13  45998  ceil5half3  47328  modm2nep1  47354  modp2nep1  47355  modm1nep2  47356  modm1nem2  47357  modm1p1ne  47358  31prm  47585  gbegt5  47749  gbowgt5  47750  sbgoldbo  47775  nnsum3primesle9  47782  nnsum4primesodd  47784  evengpop3  47786  usgrexmpl1lem  48009  usgrexmpl2lem  48014  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  gpg5nbgrvtx13starlem2  48060  gpg5nbgr3star  48069  gpg5edgnedg  48118