Theorem 4re 12348

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 12329	. 2 ⊢ 4 = (3 + 1)
2		3re 12344	. . 3 ⊢ 3 ∈ ℝ
3		1re 11259	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11274	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℝcr 11152  1c1 11154   + caddc 11156  3c3 12320  4c4 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-i2m1 11221  ax-1ne0 11222  ax-rrecex 11225  ax-cnre 11226

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327  df-3 12328  df-4 12329

This theorem is referenced by:  5re  12351  4ne0  12372  5pos  12373  2lt4  12439  1lt4  12440  4lt5  12441  3lt5  12442  2lt5  12443  1lt5  12444  4lt6  12446  3lt6  12447  4lt7  12452  3lt7  12453  4lt8  12459  3lt8  12460  4lt9  12467  3lt9  12468  div4p1lem1div2  12519  4lt10  12867  3lt10  12868  eluz4eluz2  12923  eluz4eluz3  12924  fz0to4untppr  13667  fzo0to42pr  13789  fldiv4p1lem1div2  13872  fldiv4lem1div2uz2  13873  fldiv4lem1div2  13874  iexpcyc  14243  discr  14276  faclbnd2  14327  4bc2eq6  14365  sqrt2gt1lt2  15310  amgm2  15405  bpoly4  16092  ef01bndlem  16217  sin01bnd  16218  cos01bnd  16219  cos2bnd  16221  flodddiv4  16449  flodddiv4t2lthalf  16452  4sqlem12  16990  tsetndxnstarvndx  17405  slotsdifplendx  17421  slotsdifdsndx  17440  slotsdifunifndx  17447  cnfldfunALTOLDOLD  21411  pcoass  25071  csbren  25447  minveclem2  25474  uniioombllem5  25636  dveflem  26032  pilem2  26511  pilem3  26512  sinhalfpilem  26520  sincosq1lem  26554  tangtx  26562  sincos4thpi  26570  log2cnv  27002  ppiublem1  27261  chtublem  27270  bposlem2  27344  bposlem6  27348  bposlem7  27349  bposlem8  27350  bposlem9  27351  gausslemma2dlem0d  27418  gausslemma2dlem3  27427  gausslemma2dlem4  27428  gausslemma2dlem5  27430  2lgslem1a2  27449  2lgslem1  27453  2lgslem2  27454  2sqlem11  27488  chebbnd1lem2  27529  chebbnd1lem3  27530  chebbnd1  27531  pntibndlem1  27648  pntlemb  27656  pntlemg  27657  pntlemr  27661  pntlemf  27664  usgrexmplef  29291  upgr4cycl4dv4e  30214  ex-id  30463  ex-1st  30473  ex-2nd  30474  dipcj  30743  minvecolem2  30904  minvecolem3  30905  normlem6  31144  lnophmlem2  32046  sqsscirc1  33869  hgt750lemd  34642  hgt750lem  34645  hgt750lem2  34646  hgt750leme  34652  problem2  35651  problem3  35652  iccioo01  37310  lcmineqlem21  42031  lcmineqlem23  42033  3lexlogpow2ineq2  42041  aks4d1p1p7  42056  aks4d1p1p5  42057  4rp  42313  limclner  45607  stoweidlem13  45969  stoweidlem26  45982  stoweidlem34  45990  stoweid  46019  stirlinglem12  46041  stirlinglem13  46042  fmtno4prmfac  47497  lighneallem4a  47533  requad01  47546  requad1  47547  requad2  47548  341fppr2  47659  4fppr1  47660  9fppr8  47662  gbowgt5  47687  sbgoldbwt  47702  sbgoldbst  47703  sbgoldbaltlem1  47704  sbgoldbalt  47706  sgoldbeven3prm  47708  nnsum4primes4  47714  nnsum4primesprm  47716  nnsum4primesgbe  47718  nnsum3primesle9  47719  nnsum4primesle9  47720  nnsum4primeseven  47725  nnsum4primesevenALTV  47726  wtgoldbnnsum4prm  47727  bgoldbnnsum3prm  47729  bgoldbtbndlem2  47731  bgoldbtbndlem3  47732  bgoldbtbnd  47734  tgblthelfgott  47740  usgrexmpl1lem  47916  usgrexmpl2lem  47921  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  usgrexmpl2trifr  47932  gpg5nbgr3star  47972  ackval42  48546  itsclc0yqsollem2  48613  itscnhlinecirc02plem1  48632  2p2ne5  49029