Theorem 4re 11879

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

Assertion

Ref	Expression
4re	⊢ 4 ∈ ℝ

Proof of Theorem 4re

Step	Hyp	Ref	Expression
1		df-4 11860	. 2 ⊢ 4 = (3 + 1)
2		3re 11875	. . 3 ⊢ 3 ∈ ℝ
3		1re 10798	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10813	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℝcr 10693  1c1 10695   + caddc 10697  3c3 11851  4c4 11852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-2 11858  df-3 11859  df-4 11860

This theorem is referenced by:  5re  11882  4ne0  11903  5pos  11904  2lt4  11970  1lt4  11971  4lt5  11972  3lt5  11973  2lt5  11974  1lt5  11975  4lt6  11977  3lt6  11978  4lt7  11983  3lt7  11984  4lt8  11990  3lt8  11991  4lt9  11998  3lt9  11999  div4p1lem1div2  12050  4lt10  12394  3lt10  12395  eluz4eluz2  12446  fz0to4untppr  13180  fzo0to42pr  13294  fldiv4p1lem1div2  13375  fldiv4lem1div2uz2  13376  fldiv4lem1div2  13377  iexpcyc  13740  discr  13772  faclbnd2  13822  4bc2eq6  13860  sqrt2gt1lt2  14803  amgm2  14898  bpoly4  15584  ef01bndlem  15708  sin01bnd  15709  cos01bnd  15710  cos2bnd  15712  flodddiv4  15937  flodddiv4t2lthalf  15940  4sqlem12  16472  cnfldfun  20329  pcoass  23875  csbren  24250  minveclem2  24277  uniioombllem5  24438  dveflem  24830  pilem2  25298  pilem3  25299  sinhalfpilem  25307  sincosq1lem  25341  tangtx  25349  sincos4thpi  25357  log2cnv  25781  ppiublem1  26037  chtublem  26046  bposlem2  26120  bposlem6  26124  bposlem7  26125  bposlem8  26126  bposlem9  26127  gausslemma2dlem0d  26194  gausslemma2dlem3  26203  gausslemma2dlem4  26204  gausslemma2dlem5  26206  2lgslem1a2  26225  2lgslem1  26229  2lgslem2  26230  2sqlem11  26264  chebbnd1lem2  26305  chebbnd1lem3  26306  chebbnd1  26307  pntibndlem1  26424  pntlemb  26432  pntlemg  26433  pntlemr  26437  pntlemf  26440  usgrexmplef  27301  upgr4cycl4dv4e  28222  ex-id  28471  ex-1st  28481  ex-2nd  28482  dipcj  28749  minvecolem2  28910  minvecolem3  28911  normlem6  29150  lnophmlem2  30052  sqsscirc1  31526  hgt750lemd  32294  hgt750lem  32297  hgt750lem2  32298  hgt750leme  32304  problem2  33291  problem3  33292  iccioo01  35181  lcmineqlem21  39740  lcmineqlem23  39742  3lexlogpow2ineq2  39750  aks4d1p1p7  39764  aks4d1p1p5  39765  limclner  42810  stoweidlem13  43172  stoweidlem26  43185  stoweidlem34  43193  stoweid  43222  stirlinglem12  43244  stirlinglem13  43245  fmtno4prmfac  44640  lighneallem4a  44676  requad01  44689  requad1  44690  requad2  44691  341fppr2  44802  4fppr1  44803  9fppr8  44805  gbowgt5  44830  sbgoldbwt  44845  sbgoldbst  44846  sbgoldbaltlem1  44847  sbgoldbalt  44849  sgoldbeven3prm  44851  nnsum4primes4  44857  nnsum4primesprm  44859  nnsum4primesgbe  44861  nnsum3primesle9  44862  nnsum4primesle9  44863  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  bgoldbtbnd  44877  tgblthelfgott  44883  ackval42  45658  itsclc0yqsollem2  45725  itscnhlinecirc02plem1  45744  2p2ne5  46116