Theorem 4re 10029

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

Assertion

Ref	Expression
4re	|- 4 e. RR

Proof of Theorem 4re

Step	Hyp	Ref	Expression
1		df-4 10016	. 2 |- 4 = ( 3 + 1 )
2		3re 10027	. . 3 |- 3 e. RR
3		1re 9046	. . 3 |- 1 e. RR
4	2, 3	readdcli 9059	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2474	1 |- 4 e. RR

Syntax hints:   e. wcel 1721  (class class class)co 6040   RRcr 8945   1c1 8947   + caddc 8949   3c3 10006   4c4 10007

This theorem is referenced by:  4cn  10030  5re  10031  5pos  10043  2lt4  10102  1lt4  10103  4lt5  10104  3lt5  10105  2lt5  10106  1lt5  10107  4lt6  10109  3lt6  10110  4lt7  10115  3lt7  10116  4lt8  10122  3lt8  10123  4lt9  10130  3lt9  10131  4lt10  10139  3lt10  10140  8th4div3  10147  fzo0to42pr  11141  iexpcyc  11440  discr  11471  faclbnd2  11537  sqr2gt1lt2  12035  amgm2  12128  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  cos2bnd  12744  4sqlem12  13279  pcoass  19002  minveclem2  19280  uniioombllem5  19432  dveflem  19816  pilem2  20321  pilem3  20322  sinhalfpilem  20327  sincosq1lem  20358  tangtx  20366  sincos4thpi  20374  sincos6thpi  20376  log2cnv  20737  ppiublem1  20939  chtublem  20948  bposlem2  21022  bposlem6  21026  bposlem7  21027  bposlem8  21028  bposlem9  21029  2sqlem11  21112  chebbnd1lem2  21117  chebbnd1lem3  21118  chebbnd1  21119  pntibndlem1  21236  pntlemb  21244  pntlemg  21245  pntlemr  21249  pntlemf  21252  usgraexvlem  21367  usgraex0elv  21368  usgraex1elv  21369  usgraex2elv  21370  usgraex3elv  21371  4cycl4v4e  21606  4cycl4dv4e  21608  ex-id  21695  ex-1st  21705  ex-2nd  21706  4ipval2  22157  4ipval3  22161  ipidsq  22162  dipcl  22164  dipcj  22166  dip0r  22169  ip1ilem  22280  ipasslem10  22293  minvecolem2  22330  minvecolem3  22331  normlem6  22570  polid2i  22612  lnopeq0i  23463  lnophmlem2  23473  sqsscirc1  24259  4bc2eq6  25157  bpoly3  26008  bpoly4  26009  csbrn  26346  stoweidlem13  27629  stoweidlem26  27642  stoweidlem34  27650  stoweid  27679  stirlinglem12  27701  stirlinglem13  27702  2p2ne5  28250

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rrecex 9018  ax-cnre 9019

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-2 10014  df-3 10015  df-4 10016