Theorem 5re 11572

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 11551	. 2 ⊢ 5 = (4 + 1)
2		4re 11569	. . 3 ⊢ 4 ∈ ℝ
3		1re 10487	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10502	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2879	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2081  (class class class)co 7016  ℝcr 10382  1c1 10384   + caddc 10386  4c4 11542  5c5 11543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-i2m1 10451  ax-1ne0 10452  ax-rrecex 10455  ax-cnre 10456

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-iota 6189  df-fv 6233  df-ov 7019  df-2 11548  df-3 11549  df-4 11550  df-5 11551

This theorem is referenced by:  6re  11575  6pos  11595  3lt5  11663  2lt5  11664  1lt5  11665  5lt6  11666  4lt6  11667  5lt7  11672  4lt7  11673  5lt8  11679  4lt8  11680  5lt9  11687  4lt9  11688  5lt10  12083  4lt10  12084  5recm6rec  12092  ef01bndlem  15370  prm23ge5  15981  prmlem1  16270  rmodislmod  19392  sralem  19639  srasca  19643  zlmlem  20346  zlmsca  20350  ppiublem1  25460  ppiub  25462  bposlem3  25544  bposlem4  25545  bposlem5  25546  bposlem6  25547  bposlem8  25549  bposlem9  25550  lgsdir2lem1  25583  gausslemma2dlem4  25627  2lgslem3  25662  cchhllem  26356  ex-id  27905  ex-sqrt  27925  threehalves  30275  cyc3conja  30437  resvvsca  30561  zlmds  30822  zlmtset  30823  hgt750lem2  31540  hgt750leme  31546  problem2  32517  stoweidlem13  41840  31prm  43242  gbegt5  43408  gbowgt5  43409  sbgoldbo  43434  nnsum3primesle9  43441  nnsum4primesodd  43443  evengpop3  43445