Theorem 5re 12273

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 12252	. 2 ⊢ 5 = (4 + 1)
2		4re 12270	. . 3 ⊢ 4 ∈ ℝ
3		1re 11174	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  4c4 12243  5c5 12244

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 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252

This theorem is referenced by:  6re  12276  6pos  12296  3lt5  12359  2lt5  12360  1lt5  12361  5lt6  12362  4lt6  12363  5lt7  12368  4lt7  12369  5lt8  12375  4lt8  12376  5lt9  12383  4lt9  12384  5lt10  12784  4lt10  12785  5recm6rec  12792  5eluz3  12842  5rp  12958  fz0to5un2tp  13592  ef01bndlem  16152  prm23ge5  16786  prmlem1  17078  vscandxnscandx  17287  slotsdifipndx  17298  slotstnscsi  17323  plendxnscandx  17336  slotsdnscsi  17355  ppiublem1  27113  ppiub  27115  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  gausslemma2dlem4  27280  2lgslem3  27315  ex-id  30363  ex-sqrt  30383  threehalves  32835  cyc3conja  33114  hgt750lem2  34643  hgt750leme  34649  problem2  35653  12gcd5e1  41991  lcmineqlem23  42039  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  stoweidlem13  46011  ceil5half3  47341  modm2nep1  47367  modp2nep1  47368  modm1nep2  47369  modm1nem2  47370  modm1p1ne  47371  31prm  47598  gbegt5  47762  gbowgt5  47763  sbgoldbo  47788  nnsum3primesle9  47795  nnsum4primesodd  47797  evengpop3  47799  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpg5nbgrvtx13starlem2  48063  gpg5nbgr3star  48072