Theorem 5re 11716

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 11695	. 2 ⊢ 5 = (4 + 1)
2		4re 11713	. . 3 ⊢ 4 ∈ ℝ
3		1re 10633	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10648	. 2 ⊢ (4 + 1) ∈ ℝ
5	1, 4	eqeltri 2907	1 ⊢ 5 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7148  ℝcr 10528  1c1 10530   + caddc 10532  4c4 11686  5c5 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-i2m1 10597  ax-1ne0 10598  ax-rrecex 10601  ax-cnre 10602

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-2 11692  df-3 11693  df-4 11694  df-5 11695

This theorem is referenced by:  6re  11719  6pos  11739  3lt5  11807  2lt5  11808  1lt5  11809  5lt6  11810  4lt6  11811  5lt7  11816  4lt7  11817  5lt8  11823  4lt8  11824  5lt9  11831  4lt9  11832  5lt10  12225  4lt10  12226  5recm6rec  12234  ef01bndlem  15529  prm23ge5  16144  prmlem1  16433  rmodislmod  19694  sralem  19941  srasca  19945  zlmlem  20656  zlmsca  20660  ppiublem1  25770  ppiub  25772  bposlem3  25854  bposlem4  25855  bposlem5  25856  bposlem6  25857  bposlem8  25859  bposlem9  25860  lgsdir2lem1  25893  gausslemma2dlem4  25937  2lgslem3  25972  cchhllem  26665  ex-id  28205  ex-sqrt  28225  threehalves  30584  cyc3conja  30792  resvvsca  30900  zlmds  31198  zlmtset  31199  hgt750lem2  31916  hgt750leme  31922  problem2  32902  stoweidlem13  42289  31prm  43751  gbegt5  43917  gbowgt5  43918  sbgoldbo  43943  nnsum3primesle9  43950  nnsum4primesodd  43952  evengpop3  43954