Theorem 4re 12467

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 12447	. 2 ⊢ 4 = (3 + 1)
2		3re 12463	. . 3 ⊢ 3 ∈ ℝ
3		1re 11347	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11363	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2860	1 ⊢ 4 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238  1c1 11240   + caddc 11242  3c3 12438  4c4 12439

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447

This theorem is used by:  5re  12470  2lt4  12560  1lt4  12561  4lt5  12562  3lt5  12563  2lt5  12564  1lt5  12565  4lt6  12567  3lt6  12568  4lt7  12573  3lt7  12574  4lt8  12580  3lt8  12581  4lt9  12588  3lt9  12589  div4p1lem1div2  12641  4lt10  12996  uzuzle24  13052  uzuzle34  13053  fz0to4untppr  13804  fzo0to42pr  13928  fldiv4p1lem1div2  14015  fldiv4lem1div2uz2  14016  fldiv4lem1div2  14017  iexpcyc  14391  discr  14425  faclbnd2  14476  4bc2eq6  14514  sqrt2gt1lt2  15484  amgm2  15581  bpoly4  16269  ef01bndlem  16396  sin01bnd  16397  cos01bnd  16398  cos2bnd  16400  flodddiv4  16629  flodddiv4t2lthalf  16632  4sqlem12  17178  tsetndxnstarvndx  17576  slotsdifplendx  17592  slotsdifdsndx  17611  slotsdifunifndx  17618  pcoass  25400  csbren  25775  minveclem2  25802  uniioombllem5  25963  dveflem  26354  pilem2  26836  pilem3  26837  sinhalfpilem  26849  sincosq1lem  26883  tangtx  26891  sincos4thpi  26899  log2cnv  27329  ppiublem1  27586  chtublem  27595  bposlem2  27669  bposlem6  27673  bposlem7  27674  bposlem8  27675  bposlem9  27676  gausslemma2dlem0d  27743  gausslemma2dlem3  27752  gausslemma2dlem4  27753  gausslemma2dlem5  27755  2lgslem1a2  27774  2lgslem1  27778  2lgslem2  27779  2sqlem11  27813  chebbnd1lem2  27854  chebbnd1lem3  27855  chebbnd1  27856  pntibndlem1  27973  pntlemb  27981  pntlemg  27982  pntlemr  27986  pntlemf  27989  usgrexmplef  29897  upgr4cycl4dv4e  30843  ex-id  31092  ex-1st  31102  ex-2nd  31103  dipcj  31373  minvecolem2  31534  minvecolem3  31535  normlem6  31774  lnophmlem2  32676  cos9thpiminplylem1  34525  sqsscirc1  34651  hgt750lemd  35388  hgt750lem  35391  hgt750lem2  35392  hgt750leme  35398  problem2  36639  problem3  36640  iccioo01  38518  lcmineqlem21  43365  lcmineqlem23  43367  3lexlogpow2ineq2  43375  aks4d1p1p7  43390  aks4d1p1p5  43391  4rp  43623  limclner  46934  stoweidlem13  47296  stoweidlem26  47309  stoweidlem34  47317  stoweid  47346  stirlinglem12  47368  stirlinglem13  47369  sinnpoly  48214  modm1p1ne  48719  fmtno4prmfac  48930  lighneallem4a  48966  nprmdvdsfacm1lem2  48979  nprmdvdsfacm1lem4  48981  nprmdvdsfacm1  48982  requad01  48992  requad1  48993  requad2  48994  341fppr2  49105  4fppr1  49106  9fppr8  49108  gbowgt5  49133  sbgoldbwt  49148  sbgoldbst  49149  sbgoldbaltlem1  49150  sbgoldbalt  49152  sgoldbeven3prm  49154  nnsum4primes4  49160  nnsum4primesprm  49162  nnsum4primesgbe  49164  nnsum3primesle9  49165  nnsum4primesle9  49166  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbnd  49180  tgblthelfgott  49186  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  usgrexmpl2trifr  49408  gpg5nbgr3star  49452  pgnbgreunbgrlem2lem3  49487  ackval42  50139  itsclc0yqsollem2  50206  itscnhlinecirc02plem1  50225  2p2ne5  51364  veronesev4lem  51404  veronesev5lem  51405  veronesev6lem  51406  veronesevrowd  51407  veroquadgsumlem  51411