Theorem 4re 12229

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 12210	. 2 ⊢ 4 = (3 + 1)
2		3re 12225	. . 3 ⊢ 3 ∈ ℝ
3		1re 11132	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11147	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029  3c3 12201  4c4 12202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208  df-3 12209  df-4 12210

This theorem is referenced by:  5re  12232  5pos  12254  2lt4  12315  1lt4  12316  4lt5  12317  3lt5  12318  2lt5  12319  1lt5  12320  4lt6  12322  3lt6  12323  4lt7  12328  3lt7  12329  4lt8  12335  3lt8  12336  4lt9  12343  3lt9  12344  div4p1lem1div2  12396  4lt10  12743  3lt10  12744  uzuzle24  12798  uzuzle34  12799  fz0to4untppr  13546  fzo0to42pr  13669  fldiv4p1lem1div2  13755  fldiv4lem1div2uz2  13756  fldiv4lem1div2  13757  iexpcyc  14130  discr  14163  faclbnd2  14214  4bc2eq6  14252  sqrt2gt1lt2  15197  amgm2  15293  bpoly4  15982  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  cos2bnd  16113  flodddiv4  16342  flodddiv4t2lthalf  16345  4sqlem12  16884  tsetndxnstarvndx  17279  slotsdifplendx  17295  slotsdifdsndx  17314  slotsdifunifndx  17321  pcoass  24980  csbren  25355  minveclem2  25382  uniioombllem5  25544  dveflem  25939  pilem2  26418  pilem3  26419  sinhalfpilem  26428  sincosq1lem  26462  tangtx  26470  sincos4thpi  26478  log2cnv  26910  ppiublem1  27169  chtublem  27178  bposlem2  27252  bposlem6  27256  bposlem7  27257  bposlem8  27258  bposlem9  27259  gausslemma2dlem0d  27326  gausslemma2dlem3  27335  gausslemma2dlem4  27336  gausslemma2dlem5  27338  2lgslem1a2  27357  2lgslem1  27361  2lgslem2  27362  2sqlem11  27396  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  pntibndlem1  27556  pntlemb  27564  pntlemg  27565  pntlemr  27569  pntlemf  27572  usgrexmplef  29332  upgr4cycl4dv4e  30260  ex-id  30509  ex-1st  30519  ex-2nd  30520  dipcj  30789  minvecolem2  30950  minvecolem3  30951  normlem6  31190  lnophmlem2  32092  cos9thpiminplylem1  33939  sqsscirc1  34065  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  problem2  35860  problem3  35861  iccioo01  37532  lcmineqlem21  42303  lcmineqlem23  42305  3lexlogpow2ineq2  42313  aks4d1p1p7  42328  aks4d1p1p5  42329  4rp  42555  limclner  45895  stoweidlem13  46257  stoweidlem26  46270  stoweidlem34  46278  stoweid  46307  stirlinglem12  46329  stirlinglem13  46330  sinnpoly  47137  modm1p1ne  47616  fmtno4prmfac  47818  lighneallem4a  47854  requad01  47867  requad1  47868  requad2  47869  341fppr2  47980  4fppr1  47981  9fppr8  47983  gbowgt5  48008  sbgoldbwt  48023  sbgoldbst  48024  sbgoldbaltlem1  48025  sbgoldbalt  48027  sgoldbeven3prm  48029  nnsum4primes4  48035  nnsum4primesprm  48037  nnsum4primesgbe  48039  nnsum3primesle9  48040  nnsum4primesle9  48041  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbnd  48055  tgblthelfgott  48061  usgrexmpl1lem  48267  usgrexmpl2lem  48272  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  usgrexmpl2trifr  48283  gpg5nbgr3star  48327  pgnbgreunbgrlem2lem3  48362  ackval42  48942  itsclc0yqsollem2  49009  itscnhlinecirc02plem1  49028  2p2ne5  50043