Theorem 4re 12270

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 12251	. 2 ⊢ 4 = (3 + 1)
2		3re 12266	. . 3 ⊢ 3 ∈ ℝ
3		1re 11174	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  3c3 12242  4c4 12243

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 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251

This theorem is referenced by:  5re  12273  5pos  12295  2lt4  12356  1lt4  12357  4lt5  12358  3lt5  12359  2lt5  12360  1lt5  12361  4lt6  12363  3lt6  12364  4lt7  12369  3lt7  12370  4lt8  12376  3lt8  12377  4lt9  12384  3lt9  12385  div4p1lem1div2  12437  4lt10  12785  3lt10  12786  uzuzle24  12844  uzuzle34  12845  fz0to4untppr  13591  fzo0to42pr  13714  fldiv4p1lem1div2  13797  fldiv4lem1div2uz2  13798  fldiv4lem1div2  13799  iexpcyc  14172  discr  14205  faclbnd2  14256  4bc2eq6  14294  sqrt2gt1lt2  15240  amgm2  15336  bpoly4  16025  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  cos2bnd  16156  flodddiv4  16385  flodddiv4t2lthalf  16388  4sqlem12  16927  tsetndxnstarvndx  17322  slotsdifplendx  17338  slotsdifdsndx  17357  slotsdifunifndx  17364  pcoass  24924  csbren  25299  minveclem2  25326  uniioombllem5  25488  dveflem  25883  pilem2  26362  pilem3  26363  sinhalfpilem  26372  sincosq1lem  26406  tangtx  26414  sincos4thpi  26422  log2cnv  26854  ppiublem1  27113  chtublem  27122  bposlem2  27196  bposlem6  27200  bposlem7  27201  bposlem8  27202  bposlem9  27203  gausslemma2dlem0d  27270  gausslemma2dlem3  27279  gausslemma2dlem4  27280  gausslemma2dlem5  27282  2lgslem1a2  27301  2lgslem1  27305  2lgslem2  27306  2sqlem11  27340  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  pntibndlem1  27500  pntlemb  27508  pntlemg  27509  pntlemr  27513  pntlemf  27516  usgrexmplef  29186  upgr4cycl4dv4e  30114  ex-id  30363  ex-1st  30373  ex-2nd  30374  dipcj  30643  minvecolem2  30804  minvecolem3  30805  normlem6  31044  lnophmlem2  31946  cos9thpiminplylem1  33772  sqsscirc1  33898  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  problem2  35653  problem3  35654  iccioo01  37315  lcmineqlem21  42037  lcmineqlem23  42039  3lexlogpow2ineq2  42047  aks4d1p1p7  42062  aks4d1p1p5  42063  4rp  42288  limclner  45649  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  stoweid  46061  stirlinglem12  46083  stirlinglem13  46084  sinnpoly  46892  modm1p1ne  47371  fmtno4prmfac  47573  lighneallem4a  47609  requad01  47622  requad1  47623  requad2  47624  341fppr2  47735  4fppr1  47736  9fppr8  47738  gbowgt5  47763  sbgoldbwt  47778  sbgoldbst  47779  sbgoldbaltlem1  47780  sbgoldbalt  47782  sgoldbeven3prm  47784  nnsum4primes4  47790  nnsum4primesprm  47792  nnsum4primesgbe  47794  nnsum3primesle9  47795  nnsum4primesle9  47796  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  tgblthelfgott  47816  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpg5nbgr3star  48072  pgnbgreunbgrlem2lem3  48106  ackval42  48685  itsclc0yqsollem2  48752  itscnhlinecirc02plem1  48771  2p2ne5  49787