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 2856	1 ⊢ 4 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2144  (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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  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 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  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  34456  sqsscirc1  34582  hgt750lemd  35319  hgt750lem  35322  hgt750lem2  35323  hgt750leme  35329  problem2  36473  problem3  36474  iccioo01  38293  lcmineqlem21  43142  lcmineqlem23  43144  3lexlogpow2ineq2  43152  aks4d1p1p7  43167  aks4d1p1p5  43168  4rp  43400  limclner  46704  stoweidlem13  47066  stoweidlem26  47079  stoweidlem34  47087  stoweid  47116  stirlinglem12  47138  stirlinglem13  47139  sinnpoly  47984  modm1p1ne  48489  fmtno4prmfac  48700  lighneallem4a  48736  nprmdvdsfacm1lem2  48749  nprmdvdsfacm1lem4  48751  nprmdvdsfacm1  48752  requad01  48762  requad1  48763  requad2  48764  341fppr2  48875  4fppr1  48876  9fppr8  48878  gbowgt5  48903  sbgoldbwt  48918  sbgoldbst  48919  sbgoldbaltlem1  48920  sbgoldbalt  48922  sgoldbeven3prm  48924  nnsum4primes4  48930  nnsum4primesprm  48932  nnsum4primesgbe  48934  nnsum3primesle9  48935  nnsum4primesle9  48936  nnsum4primeseven  48941  nnsum4primesevenALTV  48942  wtgoldbnnsum4prm  48943  bgoldbnnsum3prm  48945  bgoldbtbndlem2  48947  bgoldbtbndlem3  48948  bgoldbtbnd  48950  tgblthelfgott  48956  usgrexmpl1lem  49162  usgrexmpl2lem  49167  usgrexmpl2nb4  49176  usgrexmpl2nb5  49177  usgrexmpl2trifr  49178  gpg5nbgr3star  49222  pgnbgreunbgrlem2lem3  49257  ackval42  49851  itsclc0yqsollem2  49918  itscnhlinecirc02plem1  49937  2p2ne5  50979  veronesev4lem  51019  veronesev5lem  51020  veronesev6lem  51021  veronesevrowd  51022  veroquadgsumlem  51026