Theorem 4re 12348

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 12329	. 2 ⊢ 4 = (3 + 1)
2		3re 12344	. . 3 ⊢ 3 ∈ ℝ
3		1re 11264	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11279	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2822	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2099  (class class class)co 7424  ℝcr 11157  1c1 11159   + caddc 11161  3c3 12320  4c4 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-i2m1 11226  ax-1ne0 11227  ax-rrecex 11230  ax-cnre 11231

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562  df-ov 7427  df-2 12327  df-3 12328  df-4 12329

This theorem is referenced by:  5re  12351  4ne0  12372  5pos  12373  2lt4  12439  1lt4  12440  4lt5  12441  3lt5  12442  2lt5  12443  1lt5  12444  4lt6  12446  3lt6  12447  4lt7  12452  3lt7  12453  4lt8  12459  3lt8  12460  4lt9  12467  3lt9  12468  div4p1lem1div2  12519  4lt10  12865  3lt10  12866  eluz4eluz2  12921  fz0to4untppr  13658  fzo0to42pr  13773  fldiv4p1lem1div2  13855  fldiv4lem1div2uz2  13856  fldiv4lem1div2  13857  iexpcyc  14225  discr  14257  faclbnd2  14308  4bc2eq6  14346  sqrt2gt1lt2  15279  amgm2  15374  bpoly4  16061  ef01bndlem  16186  sin01bnd  16187  cos01bnd  16188  cos2bnd  16190  flodddiv4  16415  flodddiv4t2lthalf  16418  4sqlem12  16958  tsetndxnstarvndx  17373  slotsdifplendx  17389  slotsdifdsndx  17408  slotsdifunifndx  17415  cnfldfunALTOLDOLD  21372  pcoass  25042  csbren  25418  minveclem2  25445  uniioombllem5  25607  dveflem  26002  pilem2  26482  pilem3  26483  sinhalfpilem  26491  sincosq1lem  26525  tangtx  26533  sincos4thpi  26541  log2cnv  26972  ppiublem1  27231  chtublem  27240  bposlem2  27314  bposlem6  27318  bposlem7  27319  bposlem8  27320  bposlem9  27321  gausslemma2dlem0d  27388  gausslemma2dlem3  27397  gausslemma2dlem4  27398  gausslemma2dlem5  27400  2lgslem1a2  27419  2lgslem1  27423  2lgslem2  27424  2sqlem11  27458  chebbnd1lem2  27499  chebbnd1lem3  27500  chebbnd1  27501  pntibndlem1  27618  pntlemb  27626  pntlemg  27627  pntlemr  27631  pntlemf  27634  usgrexmplef  29195  upgr4cycl4dv4e  30118  ex-id  30367  ex-1st  30377  ex-2nd  30378  dipcj  30647  minvecolem2  30808  minvecolem3  30809  normlem6  31048  lnophmlem2  31950  sqsscirc1  33723  hgt750lemd  34494  hgt750lem  34497  hgt750lem2  34498  hgt750leme  34504  problem2  35494  problem3  35495  iccioo01  37034  lcmineqlem21  41748  lcmineqlem23  41750  3lexlogpow2ineq2  41758  aks4d1p1p7  41773  aks4d1p1p5  41774  limclner  45272  stoweidlem13  45634  stoweidlem26  45647  stoweidlem34  45655  stoweid  45684  stirlinglem12  45706  stirlinglem13  45707  fmtno4prmfac  47144  lighneallem4a  47180  requad01  47193  requad1  47194  requad2  47195  341fppr2  47306  4fppr1  47307  9fppr8  47309  gbowgt5  47334  sbgoldbwt  47349  sbgoldbst  47350  sbgoldbaltlem1  47351  sbgoldbalt  47353  sgoldbeven3prm  47355  nnsum4primes4  47361  nnsum4primesprm  47363  nnsum4primesgbe  47365  nnsum3primesle9  47366  nnsum4primesle9  47367  nnsum4primeseven  47372  nnsum4primesevenALTV  47373  wtgoldbnnsum4prm  47374  bgoldbnnsum3prm  47376  bgoldbtbndlem2  47378  bgoldbtbndlem3  47379  bgoldbtbnd  47381  tgblthelfgott  47387  ackval42  48084  itsclc0yqsollem2  48151  itscnhlinecirc02plem1  48170  2p2ne5  48546