Theorem 5re 11727

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 11706	. 2 ⊢ 5 = (4 + 1)
2		4re 11724	. . 3 ⊢ 4 ∈ ℝ
3		1re 10643	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10658	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2911	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7158  ℝcr 10538  1c1 10540   + caddc 10542  4c4 11697  5c5 11698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-i2m1 10607  ax-1ne0 10608  ax-rrecex 10611  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-2 11703  df-3 11704  df-4 11705  df-5 11706

This theorem is referenced by:  6re  11730  6pos  11750  3lt5  11818  2lt5  11819  1lt5  11820  5lt6  11821  4lt6  11822  5lt7  11827  4lt7  11828  5lt8  11834  4lt8  11835  5lt9  11842  4lt9  11843  5lt10  12236  4lt10  12237  5recm6rec  12245  ef01bndlem  15539  prm23ge5  16154  prmlem1  16443  rmodislmod  19704  sralem  19951  srasca  19955  zlmlem  20666  zlmsca  20670  ppiublem1  25780  ppiub  25782  bposlem3  25864  bposlem4  25865  bposlem5  25866  bposlem6  25867  bposlem8  25869  bposlem9  25870  lgsdir2lem1  25903  gausslemma2dlem4  25947  2lgslem3  25982  cchhllem  26675  ex-id  28215  ex-sqrt  28235  threehalves  30593  cyc3conja  30801  resvvsca  30909  zlmds  31207  zlmtset  31208  hgt750lem2  31925  hgt750leme  31931  problem2  32911  stoweidlem13  42305  31prm  43767  gbegt5  43933  gbowgt5  43934  sbgoldbo  43959  nnsum3primesle9  43966  nnsum4primesodd  43968  evengpop3  43970