Theorem 4re 12351

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 12332	. 2 ⊢ 4 = (3 + 1)
2		3re 12347	. . 3 ⊢ 3 ∈ ℝ
3		1re 11262	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11277	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2836	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℝcr 11155  1c1 11157   + caddc 11159  3c3 12323  4c4 12324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-i2m1 11224  ax-1ne0 11225  ax-rrecex 11228  ax-cnre 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-2 12330  df-3 12331  df-4 12332

This theorem is referenced by:  5re  12354  5pos  12376  2lt4  12442  1lt4  12443  4lt5  12444  3lt5  12445  2lt5  12446  1lt5  12447  4lt6  12449  3lt6  12450  4lt7  12455  3lt7  12456  4lt8  12462  3lt8  12463  4lt9  12470  3lt9  12471  div4p1lem1div2  12523  4lt10  12871  3lt10  12872  eluz4eluz2  12926  eluz4eluz3  12927  fz0to4untppr  13671  fzo0to42pr  13793  fldiv4p1lem1div2  13876  fldiv4lem1div2uz2  13877  fldiv4lem1div2  13878  iexpcyc  14247  discr  14280  faclbnd2  14331  4bc2eq6  14369  sqrt2gt1lt2  15314  amgm2  15409  bpoly4  16096  ef01bndlem  16221  sin01bnd  16222  cos01bnd  16223  cos2bnd  16225  flodddiv4  16453  flodddiv4t2lthalf  16456  4sqlem12  16995  tsetndxnstarvndx  17404  slotsdifplendx  17420  slotsdifdsndx  17439  slotsdifunifndx  17446  cnfldfunALTOLDOLD  21394  pcoass  25058  csbren  25434  minveclem2  25461  uniioombllem5  25623  dveflem  26018  pilem2  26497  pilem3  26498  sinhalfpilem  26506  sincosq1lem  26540  tangtx  26548  sincos4thpi  26556  log2cnv  26988  ppiublem1  27247  chtublem  27256  bposlem2  27330  bposlem6  27334  bposlem7  27335  bposlem8  27336  bposlem9  27337  gausslemma2dlem0d  27404  gausslemma2dlem3  27413  gausslemma2dlem4  27414  gausslemma2dlem5  27416  2lgslem1a2  27435  2lgslem1  27439  2lgslem2  27440  2sqlem11  27474  chebbnd1lem2  27515  chebbnd1lem3  27516  chebbnd1  27517  pntibndlem1  27634  pntlemb  27642  pntlemg  27643  pntlemr  27647  pntlemf  27650  usgrexmplef  29277  upgr4cycl4dv4e  30205  ex-id  30454  ex-1st  30464  ex-2nd  30465  dipcj  30734  minvecolem2  30895  minvecolem3  30896  normlem6  31135  lnophmlem2  32037  sqsscirc1  33908  hgt750lemd  34664  hgt750lem  34667  hgt750lem2  34668  hgt750leme  34674  problem2  35672  problem3  35673  iccioo01  37329  lcmineqlem21  42051  lcmineqlem23  42053  3lexlogpow2ineq2  42061  aks4d1p1p7  42076  aks4d1p1p5  42077  4rp  42339  limclner  45671  stoweidlem13  46033  stoweidlem26  46046  stoweidlem34  46054  stoweid  46083  stirlinglem12  46105  stirlinglem13  46106  fmtno4prmfac  47564  lighneallem4a  47600  requad01  47613  requad1  47614  requad2  47615  341fppr2  47726  4fppr1  47727  9fppr8  47729  gbowgt5  47754  sbgoldbwt  47769  sbgoldbst  47770  sbgoldbaltlem1  47771  sbgoldbalt  47773  sgoldbeven3prm  47775  nnsum4primes4  47781  nnsum4primesprm  47783  nnsum4primesgbe  47785  nnsum3primesle9  47786  nnsum4primesle9  47787  nnsum4primeseven  47792  nnsum4primesevenALTV  47793  wtgoldbnnsum4prm  47794  bgoldbnnsum3prm  47796  bgoldbtbndlem2  47798  bgoldbtbndlem3  47799  bgoldbtbnd  47801  tgblthelfgott  47807  usgrexmpl1lem  47985  usgrexmpl2lem  47990  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  usgrexmpl2trifr  48001  gpg5nbgr3star  48042  ackval42  48622  itsclc0yqsollem2  48689  itscnhlinecirc02plem1  48708  2p2ne5  49372