Theorem 4re 12265

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 12246	. 2 ⊢ 4 = (3 + 1)
2		3re 12261	. . 3 ⊢ 3 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  3c3 12237  4c4 12238

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246

This theorem is referenced by:  5re  12268  5pos  12290  2lt4  12351  1lt4  12352  4lt5  12353  3lt5  12354  2lt5  12355  1lt5  12356  4lt6  12358  3lt6  12359  4lt7  12364  3lt7  12365  4lt8  12371  3lt8  12372  4lt9  12379  3lt9  12380  div4p1lem1div2  12432  4lt10  12780  3lt10  12781  uzuzle24  12835  uzuzle34  12836  fz0to4untppr  13584  fzo0to42pr  13708  fldiv4p1lem1div2  13794  fldiv4lem1div2uz2  13795  fldiv4lem1div2  13796  iexpcyc  14169  discr  14202  faclbnd2  14253  4bc2eq6  14291  sqrt2gt1lt2  15236  amgm2  15332  bpoly4  16024  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  cos2bnd  16155  flodddiv4  16384  flodddiv4t2lthalf  16387  4sqlem12  16927  tsetndxnstarvndx  17322  slotsdifplendx  17338  slotsdifdsndx  17357  slotsdifunifndx  17364  pcoass  24991  csbren  25366  minveclem2  25393  uniioombllem5  25554  dveflem  25946  pilem2  26417  pilem3  26418  sinhalfpilem  26427  sincosq1lem  26461  tangtx  26469  sincos4thpi  26477  log2cnv  26908  ppiublem1  27165  chtublem  27174  bposlem2  27248  bposlem6  27252  bposlem7  27253  bposlem8  27254  bposlem9  27255  gausslemma2dlem0d  27322  gausslemma2dlem3  27331  gausslemma2dlem4  27332  gausslemma2dlem5  27334  2lgslem1a2  27353  2lgslem1  27357  2lgslem2  27358  2sqlem11  27392  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  pntibndlem1  27552  pntlemb  27560  pntlemg  27561  pntlemr  27565  pntlemf  27568  usgrexmplef  29328  upgr4cycl4dv4e  30255  ex-id  30504  ex-1st  30514  ex-2nd  30515  dipcj  30785  minvecolem2  30946  minvecolem3  30947  normlem6  31186  lnophmlem2  32088  cos9thpiminplylem1  33926  sqsscirc1  34052  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  problem2  35848  problem3  35849  iccioo01  37643  lcmineqlem21  42488  lcmineqlem23  42490  3lexlogpow2ineq2  42498  aks4d1p1p7  42513  aks4d1p1p5  42514  4rp  42732  limclner  46079  stoweidlem13  46441  stoweidlem26  46454  stoweidlem34  46462  stoweid  46491  stirlinglem12  46513  stirlinglem13  46514  sinnpoly  47339  modm1p1ne  47824  fmtno4prmfac  48035  lighneallem4a  48071  nprmdvdsfacm1lem2  48084  nprmdvdsfacm1lem4  48086  nprmdvdsfacm1  48087  requad01  48097  requad1  48098  requad2  48099  341fppr2  48210  4fppr1  48211  9fppr8  48213  gbowgt5  48238  sbgoldbwt  48253  sbgoldbst  48254  sbgoldbaltlem1  48255  sbgoldbalt  48257  sgoldbeven3prm  48259  nnsum4primes4  48265  nnsum4primesprm  48267  nnsum4primesgbe  48269  nnsum3primesle9  48270  nnsum4primesle9  48271  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  tgblthelfgott  48291  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpg5nbgr3star  48557  pgnbgreunbgrlem2lem3  48592  ackval42  49172  itsclc0yqsollem2  49239  itscnhlinecirc02plem1  49258  2p2ne5  50273