Theorem 4re 12324

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 12304	. 2 ⊢ 4 = (3 + 1)
2		3re 12320	. . 3 ⊢ 3 ∈ ℝ
3		1re 11207	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11223	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2865	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℝcr 11098  1c1 11100   + caddc 11102  3c3 12295  4c4 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12302  df-3 12303  df-4 12304

This theorem is referenced by:  5re  12327  2lt4  12417  1lt4  12418  4lt5  12419  3lt5  12420  2lt5  12421  1lt5  12422  4lt6  12424  3lt6  12425  4lt7  12430  3lt7  12431  4lt8  12437  3lt8  12438  4lt9  12445  3lt9  12446  div4p1lem1div2  12498  4lt10  12852  uzuzle24  12908  uzuzle34  12909  fz0to4untppr  13657  fzo0to42pr  13781  fldiv4p1lem1div2  13867  fldiv4lem1div2uz2  13868  fldiv4lem1div2  13869  iexpcyc  14242  discr  14275  faclbnd2  14326  4bc2eq6  14364  sqrt2gt1lt2  15324  amgm2  15420  bpoly4  16112  ef01bndlem  16239  sin01bnd  16240  cos01bnd  16241  cos2bnd  16243  flodddiv4  16472  flodddiv4t2lthalf  16475  4sqlem12  17015  tsetndxnstarvndx  17411  slotsdifplendx  17427  slotsdifdsndx  17446  slotsdifunifndx  17453  pcoass  25151  csbren  25526  minveclem2  25553  uniioombllem5  25714  dveflem  26106  pilem2  26580  pilem3  26581  sinhalfpilem  26593  sincosq1lem  26627  tangtx  26635  sincos4thpi  26643  log2cnv  27074  ppiublem1  27331  chtublem  27340  bposlem2  27414  bposlem6  27418  bposlem7  27419  bposlem8  27420  bposlem9  27421  gausslemma2dlem0d  27488  gausslemma2dlem3  27497  gausslemma2dlem4  27498  gausslemma2dlem5  27500  2lgslem1a2  27519  2lgslem1  27523  2lgslem2  27524  2sqlem11  27558  chebbnd1lem2  27599  chebbnd1lem3  27600  chebbnd1  27601  pntibndlem1  27718  pntlemb  27726  pntlemg  27727  pntlemr  27731  pntlemf  27734  usgrexmplef  29549  upgr4cycl4dv4e  30476  ex-id  30725  ex-1st  30735  ex-2nd  30736  dipcj  31006  minvecolem2  31167  minvecolem3  31168  normlem6  31407  lnophmlem2  32309  cos9thpiminplylem1  34116  sqsscirc1  34242  hgt750lemd  34979  hgt750lem  34982  hgt750lem2  34983  hgt750leme  34989  problem2  36056  problem3  36057  iccioo01  37860  lcmineqlem21  42705  lcmineqlem23  42707  3lexlogpow2ineq2  42715  aks4d1p1p7  42730  aks4d1p1p5  42731  4rp  42950  limclner  46256  stoweidlem13  46618  stoweidlem26  46631  stoweidlem34  46639  stoweid  46668  stirlinglem12  46690  stirlinglem13  46691  sinnpoly  47516  modm1p1ne  48001  fmtno4prmfac  48212  lighneallem4a  48248  nprmdvdsfacm1lem2  48261  nprmdvdsfacm1lem4  48263  nprmdvdsfacm1  48264  requad01  48274  requad1  48275  requad2  48276  341fppr2  48387  4fppr1  48388  9fppr8  48390  gbowgt5  48415  sbgoldbwt  48430  sbgoldbst  48431  sbgoldbaltlem1  48432  sbgoldbalt  48434  sgoldbeven3prm  48436  nnsum4primes4  48442  nnsum4primesprm  48444  nnsum4primesgbe  48446  nnsum3primesle9  48447  nnsum4primesle9  48448  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  bgoldbtbndlem2  48459  bgoldbtbndlem3  48460  bgoldbtbnd  48462  tgblthelfgott  48468  usgrexmpl1lem  48674  usgrexmpl2lem  48679  usgrexmpl2nb4  48688  usgrexmpl2nb5  48689  usgrexmpl2trifr  48690  gpg5nbgr3star  48734  pgnbgreunbgrlem2lem3  48769  ackval42  49360  itsclc0yqsollem2  49427  itscnhlinecirc02plem1  49446  2p2ne5  50471