Theorem 4re 12246

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 12227	. 2 ⊢ 4 = (3 + 1)
2		3re 12242	. . 3 ⊢ 3 ∈ ℝ
3		1re 11150	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11165	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  1c1 11045   + caddc 11047  3c3 12218  4c4 12219

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 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226  df-4 12227

This theorem is referenced by:  5re  12249  5pos  12271  2lt4  12332  1lt4  12333  4lt5  12334  3lt5  12335  2lt5  12336  1lt5  12337  4lt6  12339  3lt6  12340  4lt7  12345  3lt7  12346  4lt8  12352  3lt8  12353  4lt9  12360  3lt9  12361  div4p1lem1div2  12413  4lt10  12761  3lt10  12762  uzuzle24  12820  uzuzle34  12821  fz0to4untppr  13567  fzo0to42pr  13690  fldiv4p1lem1div2  13773  fldiv4lem1div2uz2  13774  fldiv4lem1div2  13775  iexpcyc  14148  discr  14181  faclbnd2  14232  4bc2eq6  14270  sqrt2gt1lt2  15216  amgm2  15312  bpoly4  16001  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  cos2bnd  16132  flodddiv4  16361  flodddiv4t2lthalf  16364  4sqlem12  16903  tsetndxnstarvndx  17298  slotsdifplendx  17314  slotsdifdsndx  17333  slotsdifunifndx  17340  pcoass  24957  csbren  25332  minveclem2  25359  uniioombllem5  25521  dveflem  25916  pilem2  26395  pilem3  26396  sinhalfpilem  26405  sincosq1lem  26439  tangtx  26447  sincos4thpi  26455  log2cnv  26887  ppiublem1  27146  chtublem  27155  bposlem2  27229  bposlem6  27233  bposlem7  27234  bposlem8  27235  bposlem9  27236  gausslemma2dlem0d  27303  gausslemma2dlem3  27312  gausslemma2dlem4  27313  gausslemma2dlem5  27315  2lgslem1a2  27334  2lgslem1  27338  2lgslem2  27339  2sqlem11  27373  chebbnd1lem2  27414  chebbnd1lem3  27415  chebbnd1  27416  pntibndlem1  27533  pntlemb  27541  pntlemg  27542  pntlemr  27546  pntlemf  27549  usgrexmplef  29239  upgr4cycl4dv4e  30164  ex-id  30413  ex-1st  30423  ex-2nd  30424  dipcj  30693  minvecolem2  30854  minvecolem3  30855  normlem6  31094  lnophmlem2  31996  cos9thpiminplylem1  33765  sqsscirc1  33891  hgt750lemd  34632  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  problem2  35646  problem3  35647  iccioo01  37308  lcmineqlem21  42030  lcmineqlem23  42032  3lexlogpow2ineq2  42040  aks4d1p1p7  42055  aks4d1p1p5  42056  4rp  42281  limclner  45642  stoweidlem13  46004  stoweidlem26  46017  stoweidlem34  46025  stoweid  46054  stirlinglem12  46076  stirlinglem13  46077  sinnpoly  46885  modm1p1ne  47364  fmtno4prmfac  47566  lighneallem4a  47602  requad01  47615  requad1  47616  requad2  47617  341fppr2  47728  4fppr1  47729  9fppr8  47731  gbowgt5  47756  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbaltlem1  47773  sbgoldbalt  47775  sgoldbeven3prm  47777  nnsum4primes4  47783  nnsum4primesprm  47785  nnsum4primesgbe  47787  nnsum3primesle9  47788  nnsum4primesle9  47789  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbnd  47803  tgblthelfgott  47809  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpg5nbgr3star  48065  pgnbgreunbgrlem2lem3  48099  ackval42  48678  itsclc0yqsollem2  48745  itscnhlinecirc02plem1  48764  2p2ne5  49780