Theorem 4re 10401

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 10385	. 2 |- 4 = ( 3 + 1 )
2		3re 10398	. . 3 |- 3 e. RR
3		1re 9388	. . 3 |- 1 e. RR
4	2, 3	readdcli 9402	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2513	1 |- 4 e. RR

Syntax hints:   e. wcel 1756  (class class class)co 6094   RRcr 9284   1c1 9286   + caddc 9288   3c3 10375   4c4 10376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-i2m1 9353  ax-1ne0 9354  ax-rrecex 9357  ax-cnre 9358

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-iota 5384  df-fv 5429  df-ov 6097  df-2 10383  df-3 10384  df-4 10385

This theorem is referenced by:  4cn  10402  5re  10403  4ne0  10421  5pos  10422  2lt4  10495  1lt4  10496  4lt5  10497  3lt5  10498  2lt5  10499  1lt5  10500  4lt6  10502  3lt6  10503  4lt7  10508  3lt7  10509  4lt8  10515  3lt8  10516  4lt9  10523  3lt9  10524  4lt10  10532  3lt10  10533  fzo0to42pr  11619  iexpcyc  11973  discr  12004  faclbnd2  12070  sqr2gt1lt2  12767  amgm2  12860  ef01bndlem  13471  sin01bnd  13472  cos01bnd  13473  cos2bnd  13475  4sqlem12  14020  pcoass  20599  csbren  20901  minveclem2  20916  uniioombllem5  21070  dveflem  21454  pilem2  21920  pilem3  21921  sinhalfpilem  21928  sincosq1lem  21962  tangtx  21970  sincos4thpi  21978  log2cnv  22342  ppiublem1  22544  chtublem  22553  bposlem2  22627  bposlem6  22631  bposlem7  22632  bposlem8  22633  bposlem9  22634  2sqlem11  22717  chebbnd1lem2  22722  chebbnd1lem3  22723  chebbnd1  22724  pntibndlem1  22841  pntlemb  22849  pntlemg  22850  pntlemr  22854  pntlemf  22857  usgraexvlem  23316  usgraex0elv  23317  usgraex1elv  23318  usgraex2elv  23319  usgraex3elv  23320  4cycl4v4e  23555  4cycl4dv4e  23557  ex-id  23644  ex-1st  23654  ex-2nd  23655  dipcj  24115  ipasslem10  24242  minvecolem2  24279  minvecolem3  24280  normlem6  24520  lnophmlem2  25424  sqsscirc1  26341  problem2  27302  problem3  27303  4bc2eq6  27394  bpoly4  28205  stoweidlem13  29811  stoweidlem26  29824  stoweidlem34  29832  stoweid  29861  stirlinglem12  29883  stirlinglem13  29884  2p2ne5  31153