Theorem 4re 10675

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 10659	. 2 |- 4 = ( 3 + 1 )
2		3re 10672	. . 3 |- 3 e. RR
3		1re 9629	. . 3 |- 1 e. RR
4	2, 3	readdcli 9643	. 2 |- ( 3 + 1 ) e. RR
5	1, 4	eqeltri 2526	1 |- 4 e. RR

Syntax hints:   e. wcel 1891  (class class class)co 6276   RRcr 9525   1c1 9527   + caddc 9529   3c3 10649   4c4 10650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-i2m1 9594  ax-1ne0 9595  ax-rrecex 9598  ax-cnre 9599

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-iota 5525  df-fv 5569  df-ov 6279  df-2 10657  df-3 10658  df-4 10659

This theorem is referenced by:  4cn  10676  5re  10677  4ne0  10695  5pos  10696  2lt4  10770  1lt4  10771  4lt5  10772  3lt5  10773  2lt5  10774  1lt5  10775  4lt6  10777  3lt6  10778  4lt7  10783  3lt7  10784  4lt8  10790  3lt8  10791  4lt9  10798  3lt9  10799  4lt10  10807  3lt10  10808  fzo0to42pr  11993  iexpcyc  12373  discr  12403  faclbnd2  12470  4bc2eq6  12508  sqrt2gt1lt2  13349  amgm2  13443  bpoly4  14123  ef01bndlem  14249  sin01bnd  14250  cos01bnd  14251  cos2bnd  14253  4sqlem12  14911  pcoass  22066  csbren  22364  minveclem2  22379  minveclem2OLD  22391  uniioombllem5  22557  dveflem  22943  pilem2  23419  pilem2OLD  23420  pilem3  23421  pilem3OLD  23422  sinhalfpilem  23430  sincosq1lem  23464  tangtx  23472  sincos4thpi  23480  log2cnv  23882  ppiublem1  24142  chtublem  24151  bposlem2  24225  bposlem6  24229  bposlem7  24230  bposlem8  24231  bposlem9  24232  2sqlem11  24315  chebbnd1lem2  24320  chebbnd1lem3  24321  chebbnd1  24322  pntibndlem1  24439  pntlemb  24447  pntlemg  24448  pntlemr  24452  pntlemf  24455  usgraexmplvtxlem  25134  usgraex0elv  25135  usgraex1elv  25136  usgraex2elv  25137  usgraex3elv  25138  4cycl4v4e  25406  4cycl4dv4e  25408  ex-id  25896  ex-1st  25906  ex-2nd  25907  dipcj  26365  minvecolem2  26529  minvecolem3  26530  minvecolem2OLD  26539  minvecolem3OLD  26540  normlem6  26780  lnophmlem2  27682  sqsscirc1  28721  problem2  30304  problem3  30305  limclner  37774  stoweidlem13  37930  stoweidlem26  37943  stoweidlem34  37952  stoweid  37982  stirlinglem12  38004  stirlinglem13  38005  gbogt5  38954  bgoldbwt  38969  bgoldbst  38970  sgoldbaltlem1  38971  sgoldbalt  38973  nnsum4primes4  38975  nnsum4primesprm  38977  nnsum4primesgbe  38979  nnsum3primesle9  38980  nnsum4primesle9  38981  nnsum4primeseven  38986  nnsum4primesevenALTV  38987  wtgoldbnnsum4prm  38988  bgoldbnnsum3prm  38990  bgoldbtbndlem2  38992  bgoldbtbndlem3  38993  bgoldbtbnd  38995  tgblthelfgott  38999  upgr4cycl4dv4e  39978  2p2ne5  40862