Theorem 4re 12434

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 12414	. 2 ⊢ 4 = (3 + 1)
2		3re 12430	. . 3 ⊢ 3 ∈ ℝ
3		1re 11315	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11331	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2856	1 ⊢ 4 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2144  (class class class)co 7424  ℝcr 11206  1c1 11208   + caddc 11210  3c3 12405  4c4 12406

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 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-i2m1 11275  ax-1ne0 11276  ax-rrecex 11279  ax-cnre 11280

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 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412  df-3 12413  df-4 12414

This theorem is used by:  5re  12437  2lt4  12527  1lt4  12528  4lt5  12529  3lt5  12530  2lt5  12531  1lt5  12532  4lt6  12534  3lt6  12535  4lt7  12540  3lt7  12541  4lt8  12547  3lt8  12548  4lt9  12555  3lt9  12556  div4p1lem1div2  12608  4lt10  12963  uzuzle24  13019  uzuzle34  13020  fz0to4untppr  13771  fzo0to42pr  13895  fldiv4p1lem1div2  13982  fldiv4lem1div2uz2  13983  fldiv4lem1div2  13984  iexpcyc  14358  discr  14391  faclbnd2  14442  4bc2eq6  14480  sqrt2gt1lt2  15450  amgm2  15546  bpoly4  16234  ef01bndlem  16361  sin01bnd  16362  cos01bnd  16363  cos2bnd  16365  flodddiv4  16594  flodddiv4t2lthalf  16597  4sqlem12  17143  tsetndxnstarvndx  17539  slotsdifplendx  17555  slotsdifdsndx  17574  slotsdifunifndx  17581  pcoass  25354  csbren  25729  minveclem2  25756  uniioombllem5  25917  dveflem  26308  pilem2  26788  pilem3  26789  sinhalfpilem  26801  sincosq1lem  26835  tangtx  26843  sincos4thpi  26851  log2cnv  27281  ppiublem1  27538  chtublem  27547  bposlem2  27621  bposlem6  27625  bposlem7  27626  bposlem8  27627  bposlem9  27628  gausslemma2dlem0d  27695  gausslemma2dlem3  27704  gausslemma2dlem4  27705  gausslemma2dlem5  27707  2lgslem1a2  27726  2lgslem1  27730  2lgslem2  27731  2sqlem11  27765  chebbnd1lem2  27806  chebbnd1lem3  27807  chebbnd1  27808  pntibndlem1  27925  pntlemb  27933  pntlemg  27934  pntlemr  27938  pntlemf  27941  usgrexmplef  29849  upgr4cycl4dv4e  30795  ex-id  31044  ex-1st  31054  ex-2nd  31055  dipcj  31325  minvecolem2  31486  minvecolem3  31487  normlem6  31726  lnophmlem2  32628  cos9thpiminplylem1  34464  sqsscirc1  34590  hgt750lemd  35327  hgt750lem  35330  hgt750lem2  35331  hgt750leme  35337  problem2  36549  problem3  36550  iccioo01  38387  lcmineqlem21  43236  lcmineqlem23  43238  3lexlogpow2ineq2  43246  aks4d1p1p7  43261  aks4d1p1p5  43262  4rp  43494  limclner  46797  stoweidlem13  47159  stoweidlem26  47172  stoweidlem34  47180  stoweid  47209  stirlinglem12  47231  stirlinglem13  47232  sinnpoly  48077  modm1p1ne  48582  fmtno4prmfac  48793  lighneallem4a  48829  nprmdvdsfacm1lem2  48842  nprmdvdsfacm1lem4  48844  nprmdvdsfacm1  48845  requad01  48855  requad1  48856  requad2  48857  341fppr2  48968  4fppr1  48969  9fppr8  48971  gbowgt5  48996  sbgoldbwt  49011  sbgoldbst  49012  sbgoldbaltlem1  49013  sbgoldbalt  49015  sgoldbeven3prm  49017  nnsum4primes4  49023  nnsum4primesprm  49025  nnsum4primesgbe  49027  nnsum3primesle9  49028  nnsum4primesle9  49029  nnsum4primeseven  49034  nnsum4primesevenALTV  49035  wtgoldbnnsum4prm  49036  bgoldbnnsum3prm  49038  bgoldbtbndlem2  49040  bgoldbtbndlem3  49041  bgoldbtbnd  49043  tgblthelfgott  49049  usgrexmpl1lem  49255  usgrexmpl2lem  49260  usgrexmpl2nb4  49269  usgrexmpl2nb5  49270  usgrexmpl2trifr  49271  gpg5nbgr3star  49315  pgnbgreunbgrlem2lem3  49350  ackval42  49944  itsclc0yqsollem2  50011  itscnhlinecirc02plem1  50030  2p2ne5  51147  veronesev4lem  51187  veronesev5lem  51188  veronesev6lem  51189  veronesevrowd  51190  veroquadgsumlem  51194