Theorem 4re 12329

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 12310	. 2 ⊢ 4 = (3 + 1)
2		3re 12325	. . 3 ⊢ 3 ∈ ℝ
3		1re 11240	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11255	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2831	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133  1c1 11135   + caddc 11137  3c3 12301  4c4 12302

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-i2m1 11202  ax-1ne0 11203  ax-rrecex 11206  ax-cnre 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308  df-3 12309  df-4 12310

This theorem is referenced by:  5re  12332  5pos  12354  2lt4  12420  1lt4  12421  4lt5  12422  3lt5  12423  2lt5  12424  1lt5  12425  4lt6  12427  3lt6  12428  4lt7  12433  3lt7  12434  4lt8  12440  3lt8  12441  4lt9  12448  3lt9  12449  div4p1lem1div2  12501  4lt10  12849  3lt10  12850  eluz4eluz2  12904  eluz4eluz3  12905  fz0to4untppr  13652  fzo0to42pr  13774  fldiv4p1lem1div2  13857  fldiv4lem1div2uz2  13858  fldiv4lem1div2  13859  iexpcyc  14230  discr  14263  faclbnd2  14314  4bc2eq6  14352  sqrt2gt1lt2  15298  amgm2  15393  bpoly4  16080  ef01bndlem  16207  sin01bnd  16208  cos01bnd  16209  cos2bnd  16211  flodddiv4  16439  flodddiv4t2lthalf  16442  4sqlem12  16981  tsetndxnstarvndx  17378  slotsdifplendx  17394  slotsdifdsndx  17413  slotsdifunifndx  17420  pcoass  24980  csbren  25356  minveclem2  25383  uniioombllem5  25545  dveflem  25940  pilem2  26419  pilem3  26420  sinhalfpilem  26429  sincosq1lem  26463  tangtx  26471  sincos4thpi  26479  log2cnv  26911  ppiublem1  27170  chtublem  27179  bposlem2  27253  bposlem6  27257  bposlem7  27258  bposlem8  27259  bposlem9  27260  gausslemma2dlem0d  27327  gausslemma2dlem3  27336  gausslemma2dlem4  27337  gausslemma2dlem5  27339  2lgslem1a2  27358  2lgslem1  27362  2lgslem2  27363  2sqlem11  27397  chebbnd1lem2  27438  chebbnd1lem3  27439  chebbnd1  27440  pntibndlem1  27557  pntlemb  27565  pntlemg  27566  pntlemr  27570  pntlemf  27573  usgrexmplef  29243  upgr4cycl4dv4e  30171  ex-id  30420  ex-1st  30430  ex-2nd  30431  dipcj  30700  minvecolem2  30861  minvecolem3  30862  normlem6  31101  lnophmlem2  32003  cos9thpiminplylem1  33821  sqsscirc1  33944  hgt750lemd  34685  hgt750lem  34688  hgt750lem2  34689  hgt750leme  34695  problem2  35693  problem3  35694  iccioo01  37350  lcmineqlem21  42067  lcmineqlem23  42069  3lexlogpow2ineq2  42077  aks4d1p1p7  42092  aks4d1p1p5  42093  4rp  42318  limclner  45660  stoweidlem13  46022  stoweidlem26  46035  stoweidlem34  46043  stoweid  46072  stirlinglem12  46094  stirlinglem13  46095  fmtno4prmfac  47566  lighneallem4a  47602  requad01  47615  requad1  47616  requad2  47617  341fppr2  47728  4fppr1  47729  9fppr8  47731  gbowgt5  47756  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbaltlem1  47773  sbgoldbalt  47775  sgoldbeven3prm  47777  nnsum4primes4  47783  nnsum4primesprm  47785  nnsum4primesgbe  47787  nnsum3primesle9  47788  nnsum4primesle9  47789  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbnd  47803  tgblthelfgott  47809  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpg5nbgr3star  48063  ackval42  48656  itsclc0yqsollem2  48723  itscnhlinecirc02plem1  48742  2p2ne5  49642