Theorem 4re 12212

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 12193	. 2 ⊢ 4 = (3 + 1)
2		3re 12208	. . 3 ⊢ 3 ∈ ℝ
3		1re 11115	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11130	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012  3c3 12184  4c4 12185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193

This theorem is referenced by:  5re  12215  5pos  12237  2lt4  12298  1lt4  12299  4lt5  12300  3lt5  12301  2lt5  12302  1lt5  12303  4lt6  12305  3lt6  12306  4lt7  12311  3lt7  12312  4lt8  12318  3lt8  12319  4lt9  12326  3lt9  12327  div4p1lem1div2  12379  4lt10  12727  3lt10  12728  uzuzle24  12786  uzuzle34  12787  fz0to4untppr  13533  fzo0to42pr  13656  fldiv4p1lem1div2  13739  fldiv4lem1div2uz2  13740  fldiv4lem1div2  13741  iexpcyc  14114  discr  14147  faclbnd2  14198  4bc2eq6  14236  sqrt2gt1lt2  15181  amgm2  15277  bpoly4  15966  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos2bnd  16097  flodddiv4  16326  flodddiv4t2lthalf  16329  4sqlem12  16868  tsetndxnstarvndx  17263  slotsdifplendx  17279  slotsdifdsndx  17298  slotsdifunifndx  17305  pcoass  24922  csbren  25297  minveclem2  25324  uniioombllem5  25486  dveflem  25881  pilem2  26360  pilem3  26361  sinhalfpilem  26370  sincosq1lem  26404  tangtx  26412  sincos4thpi  26420  log2cnv  26852  ppiublem1  27111  chtublem  27120  bposlem2  27194  bposlem6  27198  bposlem7  27199  bposlem8  27200  bposlem9  27201  gausslemma2dlem0d  27268  gausslemma2dlem3  27277  gausslemma2dlem4  27278  gausslemma2dlem5  27280  2lgslem1a2  27299  2lgslem1  27303  2lgslem2  27304  2sqlem11  27338  chebbnd1lem2  27379  chebbnd1lem3  27380  chebbnd1  27381  pntibndlem1  27498  pntlemb  27506  pntlemg  27507  pntlemr  27511  pntlemf  27514  usgrexmplef  29204  upgr4cycl4dv4e  30129  ex-id  30378  ex-1st  30388  ex-2nd  30389  dipcj  30658  minvecolem2  30819  minvecolem3  30820  normlem6  31059  lnophmlem2  31961  cos9thpiminplylem1  33749  sqsscirc1  33875  hgt750lemd  34616  hgt750lem  34619  hgt750lem2  34620  hgt750leme  34626  problem2  35643  problem3  35644  iccioo01  37305  lcmineqlem21  42026  lcmineqlem23  42028  3lexlogpow2ineq2  42036  aks4d1p1p7  42051  aks4d1p1p5  42052  4rp  42277  limclner  45636  stoweidlem13  45998  stoweidlem26  46011  stoweidlem34  46019  stoweid  46048  stirlinglem12  46070  stirlinglem13  46071  sinnpoly  46879  modm1p1ne  47358  fmtno4prmfac  47560  lighneallem4a  47596  requad01  47609  requad1  47610  requad2  47611  341fppr2  47722  4fppr1  47723  9fppr8  47725  gbowgt5  47750  sbgoldbwt  47765  sbgoldbst  47766  sbgoldbaltlem1  47767  sbgoldbalt  47769  sgoldbeven3prm  47771  nnsum4primes4  47777  nnsum4primesprm  47779  nnsum4primesgbe  47781  nnsum3primesle9  47782  nnsum4primesle9  47783  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  wtgoldbnnsum4prm  47790  bgoldbnnsum3prm  47792  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbnd  47797  tgblthelfgott  47803  usgrexmpl1lem  48009  usgrexmpl2lem  48014  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  usgrexmpl2trifr  48025  gpg5nbgr3star  48069  pgnbgreunbgrlem2lem3  48104  ackval42  48685  itsclc0yqsollem2  48752  itscnhlinecirc02plem1  48771  2p2ne5  49787