Theorem 4re 12427

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 12407	. 2 ⊢ 4 = (3 + 1)
2		3re 12423	. . 3 ⊢ 3 ∈ ℝ
3		1re 11308	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2857	1 ⊢ 4 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203  3c3 12398  4c4 12399

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407

This theorem is used by:  5re  12430  2lt4  12520  1lt4  12521  4lt5  12522  3lt5  12523  2lt5  12524  1lt5  12525  4lt6  12527  3lt6  12528  4lt7  12533  3lt7  12534  4lt8  12540  3lt8  12541  4lt9  12548  3lt9  12549  div4p1lem1div2  12601  4lt10  12956  uzuzle24  13012  uzuzle34  13013  fz0to4untppr  13764  fzo0to42pr  13888  fldiv4p1lem1div2  13975  fldiv4lem1div2uz2  13976  fldiv4lem1div2  13977  iexpcyc  14351  discr  14384  faclbnd2  14435  4bc2eq6  14473  sqrt2gt1lt2  15441  amgm2  15537  bpoly4  16225  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  cos2bnd  16356  flodddiv4  16585  flodddiv4t2lthalf  16588  4sqlem12  17134  tsetndxnstarvndx  17530  slotsdifplendx  17546  slotsdifdsndx  17565  slotsdifunifndx  17572  pcoass  25345  csbren  25720  minveclem2  25747  uniioombllem5  25908  dveflem  26299  pilem2  26779  pilem3  26780  sinhalfpilem  26792  sincosq1lem  26826  tangtx  26834  sincos4thpi  26842  log2cnv  27272  ppiublem1  27529  chtublem  27538  bposlem2  27612  bposlem6  27616  bposlem7  27617  bposlem8  27618  bposlem9  27619  gausslemma2dlem0d  27686  gausslemma2dlem3  27695  gausslemma2dlem4  27696  gausslemma2dlem5  27698  2lgslem1a2  27717  2lgslem1  27721  2lgslem2  27722  2sqlem11  27756  chebbnd1lem2  27797  chebbnd1lem3  27798  chebbnd1  27799  pntibndlem1  27916  pntlemb  27924  pntlemg  27925  pntlemr  27929  pntlemf  27932  usgrexmplef  29840  upgr4cycl4dv4e  30786  ex-id  31035  ex-1st  31045  ex-2nd  31046  dipcj  31316  minvecolem2  31477  minvecolem3  31478  normlem6  31717  lnophmlem2  32619  cos9thpiminplylem1  34414  sqsscirc1  34540  hgt750lemd  35277  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  problem2  36431  problem3  36432  iccioo01  38250  lcmineqlem21  43099  lcmineqlem23  43101  3lexlogpow2ineq2  43109  aks4d1p1p7  43124  aks4d1p1p5  43125  4rp  43357  limclner  46660  stoweidlem13  47022  stoweidlem26  47035  stoweidlem34  47043  stoweid  47072  stirlinglem12  47094  stirlinglem13  47095  sinnpoly  47940  modm1p1ne  48445  fmtno4prmfac  48656  lighneallem4a  48692  nprmdvdsfacm1lem2  48705  nprmdvdsfacm1lem4  48707  nprmdvdsfacm1  48708  requad01  48718  requad1  48719  requad2  48720  341fppr2  48831  4fppr1  48832  9fppr8  48834  gbowgt5  48859  sbgoldbwt  48874  sbgoldbst  48875  sbgoldbaltlem1  48876  sbgoldbalt  48878  sgoldbeven3prm  48880  nnsum4primes4  48886  nnsum4primesprm  48888  nnsum4primesgbe  48890  nnsum3primesle9  48891  nnsum4primesle9  48892  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  bgoldbtbndlem2  48903  bgoldbtbndlem3  48904  bgoldbtbnd  48906  tgblthelfgott  48912  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  usgrexmpl2trifr  49134  gpg5nbgr3star  49178  pgnbgreunbgrlem2lem3  49213  ackval42  49807  itsclc0yqsollem2  49874  itscnhlinecirc02plem1  49893  2p2ne5  50935  veronesev4lem  50975  veronesev5lem  50976  veronesev6lem  50977  veronesevrowd  50978  veroquadgsumlem  50982