Theorem 4re 11465

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 11445	. 2 ⊢ 4 = (3 + 1)
2		3re 11460	. . 3 ⊢ 3 ∈ ℝ
3		1re 10378	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10394	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2855	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 6924  ℝcr 10273  1c1 10275   + caddc 10277  3c3 11436  4c4 11437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-i2m1 10342  ax-1ne0 10343  ax-rrecex 10346  ax-cnre 10347

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-iota 6101  df-fv 6145  df-ov 6927  df-2 11443  df-3 11444  df-4 11445

This theorem is referenced by:  4cnOLD  11467  5re  11469  4ne0  11495  5pos  11496  2lt4  11562  1lt4  11563  4lt5  11564  3lt5  11565  2lt5  11566  1lt5  11567  4lt6  11569  3lt6  11570  4lt7  11575  3lt7  11576  4lt8  11582  3lt8  11583  4lt9  11590  3lt9  11591  div4p1lem1div2  11642  4lt10  11988  3lt10  11989  fz0to4untppr  12766  fzo0to42pr  12879  fldiv4p1lem1div2  12960  fldiv4lem1div2uz2  12961  fldiv4lem1div2  12962  iexpcyc  13293  discr  13325  faclbnd2  13402  4bc2eq6  13440  sqrt2gt1lt2  14428  amgm2  14523  bpoly4  15201  ef01bndlem  15325  sin01bnd  15326  cos01bnd  15327  cos2bnd  15329  flodddiv4  15553  flodddiv4t2lthalf  15556  4sqlem12  16075  cnfldfun  20165  pcoass  23242  csbren  23616  minveclem2  23643  uniioombllem5  23802  dveflem  24190  pilem2  24654  pilem3  24655  pilem3OLD  24656  sinhalfpilem  24664  sincosq1lem  24698  tangtx  24706  sincos4thpi  24714  log2cnv  25134  ppiublem1  25390  chtublem  25399  bposlem2  25473  bposlem6  25477  bposlem7  25478  bposlem8  25479  bposlem9  25480  gausslemma2dlem0d  25547  gausslemma2dlem3  25556  gausslemma2dlem4  25557  gausslemma2dlem5  25559  2lgslem1a2  25578  2lgslem1  25582  2lgslem2  25583  2sqlem11  25617  chebbnd1lem2  25628  chebbnd1lem3  25629  chebbnd1  25630  pntibndlem1  25747  pntlemb  25755  pntlemg  25756  pntlemr  25760  pntlemf  25763  usgrexmplef  26623  upgr4cycl4dv4e  27605  ex-id  27883  ex-1st  27893  ex-2nd  27894  dipcj  28158  minvecolem2  28320  minvecolem3  28321  normlem6  28561  lnophmlem2  29465  sqsscirc1  30560  hgt750lemd  31336  hgt750lem  31339  hgt750lem2  31340  hgt750leme  31346  problem2  32165  problem3  32166  limclner  40805  stoweidlem13  41171  stoweidlem26  41184  stoweidlem34  41192  stoweid  41221  stirlinglem12  41243  stirlinglem13  41244  fmtno4prmfac  42519  lighneallem4a  42560  requad01  42573  requad1  42574  requad2  42575  gbowgt5  42689  sbgoldbwt  42704  sbgoldbst  42705  sbgoldbaltlem1  42706  sbgoldbalt  42708  sgoldbeven3prm  42710  nnsum4primes4  42716  nnsum4primesprm  42718  nnsum4primesgbe  42720  nnsum3primesle9  42721  nnsum4primesle9  42722  nnsum4primeseven  42727  nnsum4primesevenALTV  42728  wtgoldbnnsum4prm  42729  bgoldbnnsum3prm  42731  bgoldbtbndlem2  42733  bgoldbtbndlem3  42734  bgoldbtbnd  42736  tgblthelfgott  42742  itsclc0yqsollem2  43513  itscnhlinecirc02plem1  43532  2p2ne5  43664