Theorem 4re 10394

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 10378	. 2 |- 4 = ( 3 + 1 )
2		3re 10391	. . 3 |- 3 e. RR
3		1re 9381	. . 3 |- 1 e. RR
4	2, 3	readdcli 9395	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2511	1 |- 4 e. RR

Syntax hints:   e. wcel 1761  (class class class)co 6090   RRcr 9277   1c1 9279   + caddc 9281   3c3 10368   4c4 10369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-i2m1 9346  ax-1ne0 9347  ax-rrecex 9350  ax-cnre 9351

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093  df-2 10376  df-3 10377  df-4 10378

This theorem is referenced by:  4cn  10395  5re  10396  4ne0  10414  5pos  10415  2lt4  10488  1lt4  10489  4lt5  10490  3lt5  10491  2lt5  10492  1lt5  10493  4lt6  10495  3lt6  10496  4lt7  10501  3lt7  10502  4lt8  10508  3lt8  10509  4lt9  10516  3lt9  10517  4lt10  10525  3lt10  10526  fzo0to42pr  11612  iexpcyc  11966  discr  11997  faclbnd2  12063  sqr2gt1lt2  12760  amgm2  12853  ef01bndlem  13464  sin01bnd  13465  cos01bnd  13466  cos2bnd  13468  4sqlem12  14013  pcoass  20555  csbren  20857  minveclem2  20872  uniioombllem5  21026  dveflem  21410  pilem2  21876  pilem3  21877  sinhalfpilem  21884  sincosq1lem  21918  tangtx  21926  sincos4thpi  21934  log2cnv  22298  ppiublem1  22500  chtublem  22509  bposlem2  22583  bposlem6  22587  bposlem7  22588  bposlem8  22589  bposlem9  22590  2sqlem11  22673  chebbnd1lem2  22678  chebbnd1lem3  22679  chebbnd1  22680  pntibndlem1  22797  pntlemb  22805  pntlemg  22806  pntlemr  22810  pntlemf  22813  usgraexvlem  23248  usgraex0elv  23249  usgraex1elv  23250  usgraex2elv  23251  usgraex3elv  23252  4cycl4v4e  23487  4cycl4dv4e  23489  ex-id  23576  ex-1st  23586  ex-2nd  23587  dipcj  24047  ipasslem10  24174  minvecolem2  24211  minvecolem3  24212  normlem6  24452  lnophmlem2  25356  sqsscirc1  26274  problem2  27229  problem3  27230  4bc2eq6  27320  bpoly4  28131  stoweidlem13  29733  stoweidlem26  29746  stoweidlem34  29754  stoweid  29783  stirlinglem12  29805  stirlinglem13  29806  2p2ne5  30989