Theorem 5re 12296

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 12275	. 2 ⊢ 5 = (4 + 1)
2		4re 12293	. . 3 ⊢ 4 ∈ ℝ
3		1re 11211	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11226	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2821	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2098  (class class class)co 7401  ℝcr 11105  1c1 11107   + caddc 11109  4c4 12266  5c5 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  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 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404  df-2 12272  df-3 12273  df-4 12274  df-5 12275

This theorem is referenced by:  6re  12299  6pos  12319  3lt5  12387  2lt5  12388  1lt5  12389  5lt6  12390  4lt6  12391  5lt7  12396  4lt7  12397  5lt8  12403  4lt8  12404  5lt9  12411  4lt9  12412  5lt10  12809  4lt10  12810  5recm6rec  12818  ef01bndlem  16124  prm23ge5  16747  prmlem1  17040  vscandxnscandx  17268  slotsdifipndx  17279  slotstnscsi  17304  plendxnscandx  17317  slotsdnscsi  17336  rmodislmodOLD  20767  sralemOLD  21015  srascaOLD  21023  zlmlemOLD  21372  ppiublem1  27051  ppiub  27053  bposlem3  27135  bposlem4  27136  bposlem5  27137  bposlem6  27138  bposlem8  27140  bposlem9  27141  lgsdir2lem1  27174  gausslemma2dlem4  27218  2lgslem3  27253  cchhllemOLD  28614  ex-id  30156  ex-sqrt  30176  threehalves  32548  cyc3conja  32784  resvvscaOLD  32918  zlmdsOLD  33432  zlmtsetOLD  33434  hgt750lem2  34153  hgt750leme  34159  problem2  35140  12gcd5e1  41361  lcmineqlem23  41409  3lexlogpow2ineq1  41416  3lexlogpow2ineq2  41417  aks4d1p1p4  41429  aks4d1p1p6  41431  aks4d1p1p7  41432  aks4d1p1p5  41433  stoweidlem13  45214  31prm  46750  gbegt5  46914  gbowgt5  46915  sbgoldbo  46940  nnsum3primesle9  46947  nnsum4primesodd  46949  evengpop3  46951