Theorem 5re 12330

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 12308	. 2 ⊢ 5 = (4 + 1)
2		4re 12327	. . 3 ⊢ 4 ∈ ℝ
3		1re 11210	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11226	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2865	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2149  (class class class)co 7413  ℝcr 11101  1c1 11103   + caddc 11105  4c4 12299  5c5 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11160  ax-icn 11161  ax-addcl 11162  ax-addrcl 11163  ax-mulcl 11164  ax-mulrcl 11165  ax-i2m1 11170  ax-1ne0 11171  ax-rrecex 11174  ax-cnre 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6495  df-fv 6547  df-ov 7416  df-2 12305  df-3 12306  df-4 12307  df-5 12308

This theorem is referenced by:  6re  12333  3lt5  12423  2lt5  12424  1lt5  12425  5lt6  12426  4lt6  12427  5lt7  12432  4lt7  12433  5lt8  12439  4lt8  12440  5lt9  12447  4lt9  12448  5lt10  12854  5recm6rec  12863  5eluz3  12909  5rp  13025  fz0to5un2tp  13661  ef01bndlem  16242  prm23ge5  16877  prmlem1  17169  vscandxnscandx  17379  slotsdifipndx  17390  slotstnscsi  17415  plendxnscandx  17428  slotsdnscsi  17447  ppiublem1  27334  ppiub  27336  bposlem3  27418  bposlem4  27419  bposlem5  27420  bposlem6  27421  bposlem8  27423  bposlem9  27424  lgsdir2lem1  27457  gausslemma2dlem4  27501  2lgslem3  27536  ex-id  30728  ex-sqrt  30748  threehalves  33177  cyc3conja  33420  hgt750lem2  34986  hgt750leme  34992  problem2  36093  12gcd5e1  42697  lcmineqlem23  42745  3lexlogpow2ineq1  42752  3lexlogpow2ineq2  42753  aks4d1p1p4  42765  aks4d1p1p6  42767  aks4d1p1p7  42768  aks4d1p1p5  42769  stoweidlem13  46656  goldrarr  47544  goldrasin  47545  goldrapos  47546  goldracos5teq  47548  ceil5half3  48009  modm2nep1  48035  modp2nep1  48036  modm1nep2  48037  modm1nem2  48038  modm1p1ne  48039  31prm  48275  gbegt5  48452  gbowgt5  48453  sbgoldbo  48478  nnsum3primesle9  48485  nnsum4primesodd  48487  evengpop3  48489  usgrexmpl1lem  48712  usgrexmpl2lem  48717  usgrexmpl2nb4  48726  usgrexmpl2nb5  48727  gpg5nbgrvtx13starlem2  48763  gpg5nbgr3star  48772  gpg5edgnedg  48821