Theorem 4re 12298

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 12279	. 2 ⊢ 4 = (3 + 1)
2		3re 12294	. . 3 ⊢ 3 ∈ ℝ
3		1re 11216	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11231	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2829	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7411  ℝcr 11111  1c1 11113   + caddc 11115  3c3 12270  4c4 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-i2m1 11180  ax-1ne0 11181  ax-rrecex 11184  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-2 12277  df-3 12278  df-4 12279

This theorem is referenced by:  5re  12301  4ne0  12322  5pos  12323  2lt4  12389  1lt4  12390  4lt5  12391  3lt5  12392  2lt5  12393  1lt5  12394  4lt6  12396  3lt6  12397  4lt7  12402  3lt7  12403  4lt8  12409  3lt8  12410  4lt9  12417  3lt9  12418  div4p1lem1div2  12469  4lt10  12815  3lt10  12816  eluz4eluz2  12871  fz0to4untppr  13606  fzo0to42pr  13721  fldiv4p1lem1div2  13802  fldiv4lem1div2uz2  13803  fldiv4lem1div2  13804  iexpcyc  14173  discr  14205  faclbnd2  14253  4bc2eq6  14291  sqrt2gt1lt2  15223  amgm2  15318  bpoly4  16005  ef01bndlem  16129  sin01bnd  16130  cos01bnd  16131  cos2bnd  16133  flodddiv4  16358  flodddiv4t2lthalf  16361  4sqlem12  16891  tsetndxnstarvndx  17306  slotsdifplendx  17322  slotsdifdsndx  17341  slotsdifunifndx  17348  cnfldfunALTOLD  20964  pcoass  24547  csbren  24923  minveclem2  24950  uniioombllem5  25111  dveflem  25503  pilem2  25971  pilem3  25972  sinhalfpilem  25980  sincosq1lem  26014  tangtx  26022  sincos4thpi  26030  log2cnv  26456  ppiublem1  26712  chtublem  26721  bposlem2  26795  bposlem6  26799  bposlem7  26800  bposlem8  26801  bposlem9  26802  gausslemma2dlem0d  26869  gausslemma2dlem3  26878  gausslemma2dlem4  26879  gausslemma2dlem5  26881  2lgslem1a2  26900  2lgslem1  26904  2lgslem2  26905  2sqlem11  26939  chebbnd1lem2  26980  chebbnd1lem3  26981  chebbnd1  26982  pntibndlem1  27099  pntlemb  27107  pntlemg  27108  pntlemr  27112  pntlemf  27115  usgrexmplef  28554  upgr4cycl4dv4e  29476  ex-id  29725  ex-1st  29735  ex-2nd  29736  dipcj  30005  minvecolem2  30166  minvecolem3  30167  normlem6  30406  lnophmlem2  31308  sqsscirc1  32957  hgt750lemd  33729  hgt750lem  33732  hgt750lem2  33733  hgt750leme  33739  problem2  34720  problem3  34721  iccioo01  36300  lcmineqlem21  41006  lcmineqlem23  41008  3lexlogpow2ineq2  41016  aks4d1p1p7  41031  aks4d1p1p5  41032  limclner  44452  stoweidlem13  44814  stoweidlem26  44827  stoweidlem34  44835  stoweid  44864  stirlinglem12  44886  stirlinglem13  44887  fmtno4prmfac  46325  lighneallem4a  46361  requad01  46374  requad1  46375  requad2  46376  341fppr2  46487  4fppr1  46488  9fppr8  46490  gbowgt5  46515  sbgoldbwt  46530  sbgoldbst  46531  sbgoldbaltlem1  46532  sbgoldbalt  46534  sgoldbeven3prm  46536  nnsum4primes4  46542  nnsum4primesprm  46544  nnsum4primesgbe  46546  nnsum3primesle9  46547  nnsum4primesle9  46548  nnsum4primeseven  46553  nnsum4primesevenALTV  46554  wtgoldbnnsum4prm  46555  bgoldbnnsum3prm  46557  bgoldbtbndlem2  46559  bgoldbtbndlem3  46560  bgoldbtbnd  46562  tgblthelfgott  46568  ackval42  47466  itsclc0yqsollem2  47533  itscnhlinecirc02plem1  47552  2p2ne5  47929