Theorem 4re 10608

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 10592	. 2 |- 4 = ( 3 + 1 )
2		3re 10605	. . 3 |- 3 e. RR
3		1re 9584	. . 3 |- 1 e. RR
4	2, 3	readdcli 9598	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2538	1 |- 4 e. RR

Syntax hints:   e. wcel 1823  (class class class)co 6270   RRcr 9480   1c1 9482   + caddc 9484   3c3 10582   4c4 10583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-2 10590  df-3 10591  df-4 10592

This theorem is referenced by:  4cn  10609  5re  10610  4ne0  10628  5pos  10629  2lt4  10702  1lt4  10703  4lt5  10704  3lt5  10705  2lt5  10706  1lt5  10707  4lt6  10709  3lt6  10710  4lt7  10715  3lt7  10716  4lt8  10722  3lt8  10723  4lt9  10730  3lt9  10731  4lt10  10739  3lt10  10740  fzo0to42pr  11882  iexpcyc  12254  discr  12285  faclbnd2  12351  sqrt2gt1lt2  13190  amgm2  13284  ef01bndlem  14001  sin01bnd  14002  cos01bnd  14003  cos2bnd  14005  4sqlem12  14558  pcoass  21690  csbren  21992  minveclem2  22007  uniioombllem5  22162  dveflem  22546  pilem2  23013  pilem3  23014  sinhalfpilem  23022  sincosq1lem  23056  tangtx  23064  sincos4thpi  23072  log2cnv  23472  ppiublem1  23675  chtublem  23684  bposlem2  23758  bposlem6  23762  bposlem7  23763  bposlem8  23764  bposlem9  23765  2sqlem11  23848  chebbnd1lem2  23853  chebbnd1lem3  23854  chebbnd1  23855  pntibndlem1  23972  pntlemb  23980  pntlemg  23981  pntlemr  23985  pntlemf  23988  usgraexvlem  24597  usgraex0elv  24598  usgraex1elv  24599  usgraex2elv  24600  usgraex3elv  24601  4cycl4v4e  24868  4cycl4dv4e  24870  ex-id  25357  ex-1st  25367  ex-2nd  25368  dipcj  25825  minvecolem2  25989  minvecolem3  25990  normlem6  26230  lnophmlem2  27134  sqsscirc1  28125  problem2  29284  problem3  29285  4bc2eq6  29353  bpoly4  30049  limclner  31896  stoweidlem13  32034  stoweidlem26  32047  stoweidlem34  32055  stoweid  32084  stirlinglem12  32106  stirlinglem13  32107  2p2ne5  33601