Theorem 4re 12201

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 12182	. 2 ⊢ 4 = (3 + 1)
2		3re 12197	. . 3 ⊢ 3 ∈ ℝ
3		1re 11104	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11119	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2825	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2110  (class class class)co 7341  ℝcr 10997  1c1 10999   + caddc 11001  3c3 12173  4c4 12174

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 2112  ax-9 2120  ax-ext 2702  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-i2m1 11066  ax-1ne0 11067  ax-rrecex 11070  ax-cnre 11071

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344  df-2 12180  df-3 12181  df-4 12182

This theorem is referenced by:  5re  12204  5pos  12226  2lt4  12287  1lt4  12288  4lt5  12289  3lt5  12290  2lt5  12291  1lt5  12292  4lt6  12294  3lt6  12295  4lt7  12300  3lt7  12301  4lt8  12307  3lt8  12308  4lt9  12315  3lt9  12316  div4p1lem1div2  12368  4lt10  12716  3lt10  12717  uzuzle24  12775  uzuzle34  12776  fz0to4untppr  13522  fzo0to42pr  13645  fldiv4p1lem1div2  13731  fldiv4lem1div2uz2  13732  fldiv4lem1div2  13733  iexpcyc  14106  discr  14139  faclbnd2  14190  4bc2eq6  14228  sqrt2gt1lt2  15173  amgm2  15269  bpoly4  15958  ef01bndlem  16085  sin01bnd  16086  cos01bnd  16087  cos2bnd  16089  flodddiv4  16318  flodddiv4t2lthalf  16321  4sqlem12  16860  tsetndxnstarvndx  17255  slotsdifplendx  17271  slotsdifdsndx  17290  slotsdifunifndx  17297  pcoass  24944  csbren  25319  minveclem2  25346  uniioombllem5  25508  dveflem  25903  pilem2  26382  pilem3  26383  sinhalfpilem  26392  sincosq1lem  26426  tangtx  26434  sincos4thpi  26442  log2cnv  26874  ppiublem1  27133  chtublem  27142  bposlem2  27216  bposlem6  27220  bposlem7  27221  bposlem8  27222  bposlem9  27223  gausslemma2dlem0d  27290  gausslemma2dlem3  27299  gausslemma2dlem4  27300  gausslemma2dlem5  27302  2lgslem1a2  27321  2lgslem1  27325  2lgslem2  27326  2sqlem11  27360  chebbnd1lem2  27401  chebbnd1lem3  27402  chebbnd1  27403  pntibndlem1  27520  pntlemb  27528  pntlemg  27529  pntlemr  27533  pntlemf  27536  usgrexmplef  29230  upgr4cycl4dv4e  30155  ex-id  30404  ex-1st  30414  ex-2nd  30415  dipcj  30684  minvecolem2  30845  minvecolem3  30846  normlem6  31085  lnophmlem2  31987  cos9thpiminplylem1  33785  sqsscirc1  33911  hgt750lemd  34651  hgt750lem  34654  hgt750lem2  34655  hgt750leme  34661  problem2  35678  problem3  35679  iccioo01  37340  lcmineqlem21  42061  lcmineqlem23  42063  3lexlogpow2ineq2  42071  aks4d1p1p7  42086  aks4d1p1p5  42087  4rp  42312  limclner  45668  stoweidlem13  46030  stoweidlem26  46043  stoweidlem34  46051  stoweid  46080  stirlinglem12  46102  stirlinglem13  46103  sinnpoly  46901  modm1p1ne  47380  fmtno4prmfac  47582  lighneallem4a  47618  requad01  47631  requad1  47632  requad2  47633  341fppr2  47744  4fppr1  47745  9fppr8  47747  gbowgt5  47772  sbgoldbwt  47787  sbgoldbst  47788  sbgoldbaltlem1  47789  sbgoldbalt  47791  sgoldbeven3prm  47793  nnsum4primes4  47799  nnsum4primesprm  47801  nnsum4primesgbe  47803  nnsum3primesle9  47804  nnsum4primesle9  47805  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  wtgoldbnnsum4prm  47812  bgoldbnnsum3prm  47814  bgoldbtbndlem2  47816  bgoldbtbndlem3  47817  bgoldbtbnd  47819  tgblthelfgott  47825  usgrexmpl1lem  48031  usgrexmpl2lem  48036  usgrexmpl2nb4  48045  usgrexmpl2nb5  48046  usgrexmpl2trifr  48047  gpg5nbgr3star  48091  pgnbgreunbgrlem2lem3  48126  ackval42  48707  itsclc0yqsollem2  48774  itscnhlinecirc02plem1  48793  2p2ne5  49809