Theorem 4re 12241

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 12222	. 2 ⊢ 4 = (3 + 1)
2		3re 12237	. . 3 ⊢ 3 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11159	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037  1c1 11039   + caddc 11041  3c3 12213  4c4 12214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221  df-4 12222

This theorem is referenced by:  5re  12244  5pos  12266  2lt4  12327  1lt4  12328  4lt5  12329  3lt5  12330  2lt5  12331  1lt5  12332  4lt6  12334  3lt6  12335  4lt7  12340  3lt7  12341  4lt8  12347  3lt8  12348  4lt9  12355  3lt9  12356  div4p1lem1div2  12408  4lt10  12755  3lt10  12756  uzuzle24  12810  uzuzle34  12811  fz0to4untppr  13558  fzo0to42pr  13681  fldiv4p1lem1div2  13767  fldiv4lem1div2uz2  13768  fldiv4lem1div2  13769  iexpcyc  14142  discr  14175  faclbnd2  14226  4bc2eq6  14264  sqrt2gt1lt2  15209  amgm2  15305  bpoly4  15994  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  cos2bnd  16125  flodddiv4  16354  flodddiv4t2lthalf  16357  4sqlem12  16896  tsetndxnstarvndx  17291  slotsdifplendx  17307  slotsdifdsndx  17326  slotsdifunifndx  17333  pcoass  24992  csbren  25367  minveclem2  25394  uniioombllem5  25556  dveflem  25951  pilem2  26430  pilem3  26431  sinhalfpilem  26440  sincosq1lem  26474  tangtx  26482  sincos4thpi  26490  log2cnv  26922  ppiublem1  27181  chtublem  27190  bposlem2  27264  bposlem6  27268  bposlem7  27269  bposlem8  27270  bposlem9  27271  gausslemma2dlem0d  27338  gausslemma2dlem3  27347  gausslemma2dlem4  27348  gausslemma2dlem5  27350  2lgslem1a2  27369  2lgslem1  27373  2lgslem2  27374  2sqlem11  27408  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  pntibndlem1  27568  pntlemb  27576  pntlemg  27577  pntlemr  27581  pntlemf  27584  usgrexmplef  29344  upgr4cycl4dv4e  30272  ex-id  30521  ex-1st  30531  ex-2nd  30532  dipcj  30802  minvecolem2  30963  minvecolem3  30964  normlem6  31203  lnophmlem2  32105  cos9thpiminplylem1  33960  sqsscirc1  34086  hgt750lemd  34826  hgt750lem  34829  hgt750lem2  34830  hgt750leme  34836  problem2  35882  problem3  35883  iccioo01  37582  lcmineqlem21  42419  lcmineqlem23  42421  3lexlogpow2ineq2  42429  aks4d1p1p7  42444  aks4d1p1p5  42445  4rp  42670  limclner  46009  stoweidlem13  46371  stoweidlem26  46384  stoweidlem34  46392  stoweid  46421  stirlinglem12  46443  stirlinglem13  46444  sinnpoly  47251  modm1p1ne  47730  fmtno4prmfac  47932  lighneallem4a  47968  requad01  47981  requad1  47982  requad2  47983  341fppr2  48094  4fppr1  48095  9fppr8  48097  gbowgt5  48122  sbgoldbwt  48137  sbgoldbst  48138  sbgoldbaltlem1  48139  sbgoldbalt  48141  sgoldbeven3prm  48143  nnsum4primes4  48149  nnsum4primesprm  48151  nnsum4primesgbe  48153  nnsum3primesle9  48154  nnsum4primesle9  48155  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbnd  48169  tgblthelfgott  48175  usgrexmpl1lem  48381  usgrexmpl2lem  48386  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  usgrexmpl2trifr  48397  gpg5nbgr3star  48441  pgnbgreunbgrlem2lem3  48476  ackval42  49056  itsclc0yqsollem2  49123  itscnhlinecirc02plem1  49142  2p2ne5  50157