Theorem 4re 12342

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 12322	. 2 ⊢ 4 = (3 + 1)
2		3re 12338	. . 3 ⊢ 3 ∈ ℝ
3		1re 11225	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11241	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2861	1 ⊢ 4 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116  1c1 11118   + caddc 11120  3c3 12313  4c4 12314

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rrecex 11189  ax-cnre 11190

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321  df-4 12322

This theorem is used by:  5re  12345  2lt4  12435  1lt4  12436  4lt5  12437  3lt5  12438  2lt5  12439  1lt5  12440  4lt6  12442  3lt6  12443  4lt7  12448  3lt7  12449  4lt8  12455  3lt8  12456  4lt9  12463  3lt9  12464  div4p1lem1div2  12516  4lt10  12871  uzuzle24  12927  uzuzle34  12928  fz0to4untppr  13677  fzo0to42pr  13801  fldiv4p1lem1div2  13888  fldiv4lem1div2uz2  13889  fldiv4lem1div2  13890  iexpcyc  14263  discr  14296  faclbnd2  14347  4bc2eq6  14385  sqrt2gt1lt2  15351  amgm2  15447  bpoly4  16137  ef01bndlem  16264  sin01bnd  16265  cos01bnd  16266  cos2bnd  16268  flodddiv4  16497  flodddiv4t2lthalf  16500  4sqlem12  17040  tsetndxnstarvndx  17436  slotsdifplendx  17452  slotsdifdsndx  17471  slotsdifunifndx  17478  pcoass  25236  csbren  25611  minveclem2  25638  uniioombllem5  25799  dveflem  26191  pilem2  26668  pilem3  26669  sinhalfpilem  26681  sincosq1lem  26715  tangtx  26723  sincos4thpi  26731  log2cnv  27162  ppiublem1  27419  chtublem  27428  bposlem2  27502  bposlem6  27506  bposlem7  27507  bposlem8  27508  bposlem9  27509  gausslemma2dlem0d  27576  gausslemma2dlem3  27585  gausslemma2dlem4  27586  gausslemma2dlem5  27588  2lgslem1a2  27607  2lgslem1  27611  2lgslem2  27612  2sqlem11  27646  chebbnd1lem2  27687  chebbnd1lem3  27688  chebbnd1  27689  pntibndlem1  27806  pntlemb  27814  pntlemg  27815  pntlemr  27819  pntlemf  27822  usgrexmplef  29669  upgr4cycl4dv4e  30609  ex-id  30858  ex-1st  30868  ex-2nd  30869  dipcj  31139  minvecolem2  31300  minvecolem3  31301  normlem6  31540  lnophmlem2  32442  cos9thpiminplylem1  34238  sqsscirc1  34364  hgt750lemd  35102  hgt750lem  35105  hgt750lem2  35106  hgt750leme  35112  problem2  36197  problem3  36198  iccioo01  38032  lcmineqlem21  42876  lcmineqlem23  42878  3lexlogpow2ineq2  42886  aks4d1p1p7  42901  aks4d1p1p5  42902  4rp  43121  limclner  46425  stoweidlem13  46787  stoweidlem26  46800  stoweidlem34  46808  stoweid  46837  stirlinglem12  46859  stirlinglem13  46860  sinnpoly  47688  modm1p1ne  48173  fmtno4prmfac  48384  lighneallem4a  48420  nprmdvdsfacm1lem2  48433  nprmdvdsfacm1lem4  48435  nprmdvdsfacm1  48436  requad01  48446  requad1  48447  requad2  48448  341fppr2  48559  4fppr1  48560  9fppr8  48562  gbowgt5  48587  sbgoldbwt  48602  sbgoldbst  48603  sbgoldbaltlem1  48604  sbgoldbalt  48606  sgoldbeven3prm  48608  nnsum4primes4  48614  nnsum4primesprm  48616  nnsum4primesgbe  48618  nnsum3primesle9  48619  nnsum4primesle9  48620  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  wtgoldbnnsum4prm  48627  bgoldbnnsum3prm  48629  bgoldbtbndlem2  48631  bgoldbtbndlem3  48632  bgoldbtbnd  48634  tgblthelfgott  48640  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  usgrexmpl2trifr  48862  gpg5nbgr3star  48906  pgnbgreunbgrlem2lem3  48941  ackval42  49535  itsclc0yqsollem2  49602  itscnhlinecirc02plem1  49621  2p2ne5  50677