Theorem 4re 12302

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 12283	. 2 ⊢ 4 = (3 + 1)
2		3re 12298	. . 3 ⊢ 3 ∈ ℝ
3		1re 11220	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11235	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2104  (class class class)co 7413  ℝcr 11113  1c1 11115   + caddc 11117  3c3 12274  4c4 12275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-i2m1 11182  ax-1ne0 11183  ax-rrecex 11186  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7416  df-2 12281  df-3 12282  df-4 12283

This theorem is referenced by:  5re  12305  4ne0  12326  5pos  12327  2lt4  12393  1lt4  12394  4lt5  12395  3lt5  12396  2lt5  12397  1lt5  12398  4lt6  12400  3lt6  12401  4lt7  12406  3lt7  12407  4lt8  12413  3lt8  12414  4lt9  12421  3lt9  12422  div4p1lem1div2  12473  4lt10  12819  3lt10  12820  eluz4eluz2  12875  fz0to4untppr  13610  fzo0to42pr  13725  fldiv4p1lem1div2  13806  fldiv4lem1div2uz2  13807  fldiv4lem1div2  13808  iexpcyc  14177  discr  14209  faclbnd2  14257  4bc2eq6  14295  sqrt2gt1lt2  15227  amgm2  15322  bpoly4  16009  ef01bndlem  16133  sin01bnd  16134  cos01bnd  16135  cos2bnd  16137  flodddiv4  16362  flodddiv4t2lthalf  16365  4sqlem12  16895  tsetndxnstarvndx  17310  slotsdifplendx  17326  slotsdifdsndx  17345  slotsdifunifndx  17352  cnfldfunALTOLD  21160  pcoass  24773  csbren  25149  minveclem2  25176  uniioombllem5  25338  dveflem  25730  pilem2  26198  pilem3  26199  sinhalfpilem  26207  sincosq1lem  26241  tangtx  26249  sincos4thpi  26257  log2cnv  26683  ppiublem1  26939  chtublem  26948  bposlem2  27022  bposlem6  27026  bposlem7  27027  bposlem8  27028  bposlem9  27029  gausslemma2dlem0d  27096  gausslemma2dlem3  27105  gausslemma2dlem4  27106  gausslemma2dlem5  27108  2lgslem1a2  27127  2lgslem1  27131  2lgslem2  27132  2sqlem11  27166  chebbnd1lem2  27207  chebbnd1lem3  27208  chebbnd1  27209  pntibndlem1  27326  pntlemb  27334  pntlemg  27335  pntlemr  27339  pntlemf  27342  usgrexmplef  28781  upgr4cycl4dv4e  29703  ex-id  29952  ex-1st  29962  ex-2nd  29963  dipcj  30232  minvecolem2  30393  minvecolem3  30394  normlem6  30633  lnophmlem2  31535  sqsscirc1  33184  hgt750lemd  33956  hgt750lem  33959  hgt750lem2  33960  hgt750leme  33966  problem2  34947  problem3  34948  iccioo01  36513  lcmineqlem21  41222  lcmineqlem23  41224  3lexlogpow2ineq2  41232  aks4d1p1p7  41247  aks4d1p1p5  41248  limclner  44667  stoweidlem13  45029  stoweidlem26  45042  stoweidlem34  45050  stoweid  45079  stirlinglem12  45101  stirlinglem13  45102  fmtno4prmfac  46540  lighneallem4a  46576  requad01  46589  requad1  46590  requad2  46591  341fppr2  46702  4fppr1  46703  9fppr8  46705  gbowgt5  46730  sbgoldbwt  46745  sbgoldbst  46746  sbgoldbaltlem1  46747  sbgoldbalt  46749  sgoldbeven3prm  46751  nnsum4primes4  46757  nnsum4primesprm  46759  nnsum4primesgbe  46761  nnsum3primesle9  46762  nnsum4primesle9  46763  nnsum4primeseven  46768  nnsum4primesevenALTV  46769  wtgoldbnnsum4prm  46770  bgoldbnnsum3prm  46772  bgoldbtbndlem2  46774  bgoldbtbndlem3  46775  bgoldbtbnd  46777  tgblthelfgott  46783  ackval42  47471  itsclc0yqsollem2  47538  itscnhlinecirc02plem1  47557  2p2ne5  47934