Theorem 5re 11099

Description: The number 5 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
5re	|- 5 e. RR

Proof of Theorem 5re

Step	Hyp	Ref	Expression
1		df-5 11082	. 2 |- 5 = ( 4 + 1 )
2		4re 11097	. . 3 |- 4 e. RR
3		1re 10039	. . 3 |- 1 e. RR
4	2, 3	readdcli 10053	. 2 |- ( 4 + 1 ) e. RR
5	1, 4	eqeltri 2697	1 |- 5 e. RR

Syntax hints:   e. wcel 1990  (class class class)co 6650   RRcr 9935   1c1 9937   + caddc 9939   4c4 11072   5c5 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-2 11079  df-3 11080  df-4 11081  df-5 11082

This theorem is referenced by:  5cn  11100  6re  11101  6pos  11119  3lt5  11201  2lt5  11202  1lt5  11203  5lt6  11204  4lt6  11205  5lt7  11210  4lt7  11211  5lt8  11217  4lt8  11218  5lt9  11225  4lt9  11226  5lt10OLD  11234  4lt10OLD  11235  5lt10  11677  4lt10  11678  5recm6rec  11686  ef01bndlem  14914  prm23ge5  15520  prmlem1  15814  rmodislmod  18931  sralem  19177  srasca  19181  zlmlem  19865  zlmsca  19869  ppiublem1  24927  ppiub  24929  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem8  25016  bposlem9  25017  lgsdir2lem1  25050  gausslemma2dlem4  25094  2lgslem3  25129  cchhllem  25767  ex-id  27291  ex-sqrt  27311  threehalves  29623  resvvsca  29834  zlmds  30008  zlmtset  30009  hgt750lem2  30730  hgt750leme  30736  problem2  31559  problem2OLD  31560  stoweidlem13  40230  31prm  41512  gbegt5  41649  gbowgt5  41650  sbgoldbo  41675  nnsum3primesle9  41682  nnsum4primesodd  41684  evengpop3  41686