Theorem 4re 12302

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 12282	. 2 ⊢ 4 = (3 + 1)
2		3re 12298	. . 3 ⊢ 3 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11197	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2858	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072  1c1 11074   + caddc 11076  3c3 12273  4c4 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281  df-4 12282

This theorem is referenced by:  5re  12305  2lt4  12395  1lt4  12396  4lt5  12397  3lt5  12398  2lt5  12399  1lt5  12400  4lt6  12402  3lt6  12403  4lt7  12408  3lt7  12409  4lt8  12415  3lt8  12416  4lt9  12423  3lt9  12424  div4p1lem1div2  12476  4lt10  12830  uzuzle24  12886  uzuzle34  12887  fz0to4untppr  13635  fzo0to42pr  13759  fldiv4p1lem1div2  13845  fldiv4lem1div2uz2  13846  fldiv4lem1div2  13847  iexpcyc  14220  discr  14253  faclbnd2  14304  4bc2eq6  14342  sqrt2gt1lt2  15301  amgm2  15397  bpoly4  16089  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos2bnd  16220  flodddiv4  16449  flodddiv4t2lthalf  16452  4sqlem12  16992  tsetndxnstarvndx  17388  slotsdifplendx  17404  slotsdifdsndx  17423  slotsdifunifndx  17430  pcoass  25086  csbren  25461  minveclem2  25488  uniioombllem5  25649  dveflem  26041  pilem2  26515  pilem3  26516  sinhalfpilem  26528  sincosq1lem  26562  tangtx  26570  sincos4thpi  26578  log2cnv  27009  ppiublem1  27266  chtublem  27275  bposlem2  27349  bposlem6  27353  bposlem7  27354  bposlem8  27355  bposlem9  27356  gausslemma2dlem0d  27423  gausslemma2dlem3  27432  gausslemma2dlem4  27433  gausslemma2dlem5  27435  2lgslem1a2  27454  2lgslem1  27458  2lgslem2  27459  2sqlem11  27493  chebbnd1lem2  27534  chebbnd1lem3  27535  chebbnd1  27536  pntibndlem1  27653  pntlemb  27661  pntlemg  27662  pntlemr  27666  pntlemf  27669  usgrexmplef  29460  upgr4cycl4dv4e  30387  ex-id  30636  ex-1st  30646  ex-2nd  30647  dipcj  30917  minvecolem2  31078  minvecolem3  31079  normlem6  31318  lnophmlem2  32220  cos9thpiminplylem1  34079  sqsscirc1  34205  hgt750lemd  34942  hgt750lem  34945  hgt750lem2  34946  hgt750leme  34952  problem2  36016  problem3  36017  iccioo01  37821  lcmineqlem21  42666  lcmineqlem23  42668  3lexlogpow2ineq2  42676  aks4d1p1p7  42691  aks4d1p1p5  42692  4rp  42909  limclner  46225  stoweidlem13  46587  stoweidlem26  46600  stoweidlem34  46608  stoweid  46637  stirlinglem12  46659  stirlinglem13  46660  sinnpoly  47485  modm1p1ne  47970  fmtno4prmfac  48181  lighneallem4a  48217  nprmdvdsfacm1lem2  48230  nprmdvdsfacm1lem4  48232  nprmdvdsfacm1  48233  requad01  48243  requad1  48244  requad2  48245  341fppr2  48356  4fppr1  48357  9fppr8  48359  gbowgt5  48384  sbgoldbwt  48399  sbgoldbst  48400  sbgoldbaltlem1  48401  sbgoldbalt  48403  sgoldbeven3prm  48405  nnsum4primes4  48411  nnsum4primesprm  48413  nnsum4primesgbe  48415  nnsum3primesle9  48416  nnsum4primesle9  48417  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  bgoldbtbndlem2  48428  bgoldbtbndlem3  48429  bgoldbtbnd  48431  tgblthelfgott  48437  usgrexmpl1lem  48643  usgrexmpl2lem  48648  usgrexmpl2nb4  48657  usgrexmpl2nb5  48658  usgrexmpl2trifr  48659  gpg5nbgr3star  48703  pgnbgreunbgrlem2lem3  48738  ackval42  49318  itsclc0yqsollem2  49385  itscnhlinecirc02plem1  49404  2p2ne5  50419