Theorem 5re 12295

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 12274	. 2 ⊢ 5 = (4 + 1)
2		4re 12292	. . 3 ⊢ 4 ∈ ℝ
3		1re 11210	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11225	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7404  ℝcr 11105  1c1 11107   + caddc 11109  4c4 12265  5c5 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7407  df-2 12271  df-3 12272  df-4 12273  df-5 12274

This theorem is referenced by:  6re  12298  6pos  12318  3lt5  12386  2lt5  12387  1lt5  12388  5lt6  12389  4lt6  12390  5lt7  12395  4lt7  12396  5lt8  12402  4lt8  12403  5lt9  12410  4lt9  12411  5lt10  12808  4lt10  12809  5recm6rec  12817  ef01bndlem  16123  prm23ge5  16744  prmlem1  17037  vscandxnscandx  17265  slotsdifipndx  17276  slotstnscsi  17301  plendxnscandx  17314  slotsdnscsi  17333  rmodislmodOLD  20529  sralemOLD  20779  srascaOLD  20787  zlmlemOLD  21051  ppiublem1  26685  ppiub  26687  bposlem3  26769  bposlem4  26770  bposlem5  26771  bposlem6  26772  bposlem8  26774  bposlem9  26775  lgsdir2lem1  26808  gausslemma2dlem4  26852  2lgslem3  26887  cchhllemOLD  28125  ex-id  29667  ex-sqrt  29687  threehalves  32059  cyc3conja  32294  resvvscaOLD  32421  zlmdsOLD  32881  zlmtsetOLD  32883  hgt750lem2  33602  hgt750leme  33608  problem2  34589  12gcd5e1  40806  lcmineqlem23  40854  3lexlogpow2ineq1  40861  3lexlogpow2ineq2  40862  aks4d1p1p4  40874  aks4d1p1p6  40876  aks4d1p1p7  40877  aks4d1p1p5  40878  stoweidlem13  44664  31prm  46200  gbegt5  46364  gbowgt5  46365  sbgoldbo  46390  nnsum3primesle9  46397  nnsum4primesodd  46399  evengpop3  46401