Theorem 4re 11724

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 11705	. 2 ⊢ 4 = (3 + 1)
2		3re 11720	. . 3 ⊢ 3 ∈ ℝ
3		1re 10643	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10658	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2911	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7158  ℝcr 10538  1c1 10540   + caddc 10542  3c3 11696  4c4 11697

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-i2m1 10607  ax-1ne0 10608  ax-rrecex 10611  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-2 11703  df-3 11704  df-4 11705

This theorem is referenced by:  5re  11727  4ne0  11748  5pos  11749  2lt4  11815  1lt4  11816  4lt5  11817  3lt5  11818  2lt5  11819  1lt5  11820  4lt6  11822  3lt6  11823  4lt7  11828  3lt7  11829  4lt8  11835  3lt8  11836  4lt9  11843  3lt9  11844  div4p1lem1div2  11895  4lt10  12237  3lt10  12238  eluz4eluz2  12288  fz0to4untppr  13013  fzo0to42pr  13127  fldiv4p1lem1div2  13208  fldiv4lem1div2uz2  13209  fldiv4lem1div2  13210  iexpcyc  13572  discr  13604  faclbnd2  13654  4bc2eq6  13692  sqrt2gt1lt2  14636  amgm2  14731  bpoly4  15415  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  cos2bnd  15543  flodddiv4  15766  flodddiv4t2lthalf  15769  4sqlem12  16294  cnfldfun  20559  pcoass  23630  csbren  24004  minveclem2  24031  uniioombllem5  24190  dveflem  24578  pilem2  25042  pilem3  25043  sinhalfpilem  25051  sincosq1lem  25085  tangtx  25093  sincos4thpi  25101  log2cnv  25524  ppiublem1  25780  chtublem  25789  bposlem2  25863  bposlem6  25867  bposlem7  25868  bposlem8  25869  bposlem9  25870  gausslemma2dlem0d  25937  gausslemma2dlem3  25946  gausslemma2dlem4  25947  gausslemma2dlem5  25949  2lgslem1a2  25968  2lgslem1  25972  2lgslem2  25973  2sqlem11  26007  chebbnd1lem2  26048  chebbnd1lem3  26049  chebbnd1  26050  pntibndlem1  26167  pntlemb  26175  pntlemg  26176  pntlemr  26180  pntlemf  26183  usgrexmplef  27043  upgr4cycl4dv4e  27966  ex-id  28215  ex-1st  28225  ex-2nd  28226  dipcj  28493  minvecolem2  28654  minvecolem3  28655  normlem6  28894  lnophmlem2  29796  sqsscirc1  31153  hgt750lemd  31921  hgt750lem  31924  hgt750lem2  31925  hgt750leme  31931  problem2  32911  problem3  32912  limclner  41939  stoweidlem13  42305  stoweidlem26  42318  stoweidlem34  42326  stoweid  42355  stirlinglem12  42377  stirlinglem13  42378  fmtno4prmfac  43741  lighneallem4a  43780  requad01  43793  requad1  43794  requad2  43795  341fppr2  43906  4fppr1  43907  9fppr8  43909  gbowgt5  43934  sbgoldbwt  43949  sbgoldbst  43950  sbgoldbaltlem1  43951  sbgoldbalt  43953  sgoldbeven3prm  43955  nnsum4primes4  43961  nnsum4primesprm  43963  nnsum4primesgbe  43965  nnsum3primesle9  43966  nnsum4primesle9  43967  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  wtgoldbnnsum4prm  43974  bgoldbnnsum3prm  43976  bgoldbtbndlem2  43978  bgoldbtbndlem3  43979  bgoldbtbnd  43981  tgblthelfgott  43987  itsclc0yqsollem2  44757  itscnhlinecirc02plem1  44776  2p2ne5  44906