Theorem 4re 12259

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 12240	. 2 ⊢ 4 = (3 + 1)
2		3re 12255	. . 3 ⊢ 3 ∈ ℝ
3		1re 11138	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11154	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  3c3 12231  4c4 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240

This theorem is referenced by:  5re  12262  5pos  12284  2lt4  12345  1lt4  12346  4lt5  12347  3lt5  12348  2lt5  12349  1lt5  12350  4lt6  12352  3lt6  12353  4lt7  12358  3lt7  12359  4lt8  12365  3lt8  12366  4lt9  12373  3lt9  12374  div4p1lem1div2  12426  4lt10  12774  3lt10  12775  uzuzle24  12829  uzuzle34  12830  fz0to4untppr  13578  fzo0to42pr  13702  fldiv4p1lem1div2  13788  fldiv4lem1div2uz2  13789  fldiv4lem1div2  13790  iexpcyc  14163  discr  14196  faclbnd2  14247  4bc2eq6  14285  sqrt2gt1lt2  15230  amgm2  15326  bpoly4  16018  ef01bndlem  16145  sin01bnd  16146  cos01bnd  16147  cos2bnd  16149  flodddiv4  16378  flodddiv4t2lthalf  16381  4sqlem12  16921  tsetndxnstarvndx  17316  slotsdifplendx  17332  slotsdifdsndx  17351  slotsdifunifndx  17358  pcoass  25004  csbren  25379  minveclem2  25406  uniioombllem5  25567  dveflem  25959  pilem2  26433  pilem3  26434  sinhalfpilem  26443  sincosq1lem  26477  tangtx  26485  sincos4thpi  26493  log2cnv  26924  ppiublem1  27182  chtublem  27191  bposlem2  27265  bposlem6  27269  bposlem7  27270  bposlem8  27271  bposlem9  27272  gausslemma2dlem0d  27339  gausslemma2dlem3  27348  gausslemma2dlem4  27349  gausslemma2dlem5  27351  2lgslem1a2  27370  2lgslem1  27374  2lgslem2  27375  2sqlem11  27409  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  pntibndlem1  27569  pntlemb  27577  pntlemg  27578  pntlemr  27582  pntlemf  27585  usgrexmplef  29345  upgr4cycl4dv4e  30273  ex-id  30522  ex-1st  30532  ex-2nd  30533  dipcj  30803  minvecolem2  30964  minvecolem3  30965  normlem6  31204  lnophmlem2  32106  cos9thpiminplylem1  33945  sqsscirc1  34071  hgt750lemd  34811  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  problem2  35867  problem3  35868  iccioo01  37660  lcmineqlem21  42505  lcmineqlem23  42507  3lexlogpow2ineq2  42515  aks4d1p1p7  42530  aks4d1p1p5  42531  4rp  42749  limclner  46100  stoweidlem13  46462  stoweidlem26  46475  stoweidlem34  46483  stoweid  46512  stirlinglem12  46534  stirlinglem13  46535  sinnpoly  47354  modm1p1ne  47839  fmtno4prmfac  48050  lighneallem4a  48086  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  requad01  48112  requad1  48113  requad2  48114  341fppr2  48225  4fppr1  48226  9fppr8  48228  gbowgt5  48253  sbgoldbwt  48268  sbgoldbst  48269  sbgoldbaltlem1  48270  sbgoldbalt  48272  sgoldbeven3prm  48274  nnsum4primes4  48280  nnsum4primesprm  48282  nnsum4primesgbe  48284  nnsum3primesle9  48285  nnsum4primesle9  48286  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbnd  48300  tgblthelfgott  48306  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  gpg5nbgr3star  48572  pgnbgreunbgrlem2lem3  48607  ackval42  49187  itsclc0yqsollem2  49254  itscnhlinecirc02plem1  49273  2p2ne5  50288