Theorem 4re 12171

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 12152	. 2 ⊢ 4 = (3 + 1)
2		3re 12167	. . 3 ⊢ 3 ∈ ℝ
3		1re 11089	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11104	. 2 ⊢ (3 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 4 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7350  ℝcr 10984  1c1 10986   + caddc 10988  3c3 12143  4c4 12144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-i2m1 11053  ax-1ne0 11054  ax-rrecex 11057  ax-cnre 11058

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353  df-2 12150  df-3 12151  df-4 12152

This theorem is referenced by:  5re  12174  4ne0  12195  5pos  12196  2lt4  12262  1lt4  12263  4lt5  12264  3lt5  12265  2lt5  12266  1lt5  12267  4lt6  12269  3lt6  12270  4lt7  12275  3lt7  12276  4lt8  12282  3lt8  12283  4lt9  12290  3lt9  12291  div4p1lem1div2  12342  4lt10  12687  3lt10  12688  eluz4eluz2  12739  fz0to4untppr  13473  fzo0to42pr  13588  fldiv4p1lem1div2  13669  fldiv4lem1div2uz2  13670  fldiv4lem1div2  13671  iexpcyc  14037  discr  14069  faclbnd2  14119  4bc2eq6  14157  sqrt2gt1lt2  15094  amgm2  15189  bpoly4  15877  ef01bndlem  16001  sin01bnd  16002  cos01bnd  16003  cos2bnd  16005  flodddiv4  16230  flodddiv4t2lthalf  16233  4sqlem12  16763  tsetndxnstarvndx  17175  slotsdifplendx  17191  slotsdifdsndx  17210  slotsdifunifndx  17217  cnfldfunALTOLD  20733  pcoass  24309  csbren  24685  minveclem2  24712  uniioombllem5  24873  dveflem  25265  pilem2  25733  pilem3  25734  sinhalfpilem  25742  sincosq1lem  25776  tangtx  25784  sincos4thpi  25792  log2cnv  26216  ppiublem1  26472  chtublem  26481  bposlem2  26555  bposlem6  26559  bposlem7  26560  bposlem8  26561  bposlem9  26562  gausslemma2dlem0d  26629  gausslemma2dlem3  26638  gausslemma2dlem4  26639  gausslemma2dlem5  26641  2lgslem1a2  26660  2lgslem1  26664  2lgslem2  26665  2sqlem11  26699  chebbnd1lem2  26740  chebbnd1lem3  26741  chebbnd1  26742  pntibndlem1  26859  pntlemb  26867  pntlemg  26868  pntlemr  26872  pntlemf  26875  usgrexmplef  27993  upgr4cycl4dv4e  28915  ex-id  29164  ex-1st  29174  ex-2nd  29175  dipcj  29442  minvecolem2  29603  minvecolem3  29604  normlem6  29843  lnophmlem2  30745  sqsscirc1  32250  hgt750lemd  33022  hgt750lem  33025  hgt750lem2  33026  hgt750leme  33032  problem2  34017  problem3  34018  iccioo01  35684  lcmineqlem21  40392  lcmineqlem23  40394  3lexlogpow2ineq2  40402  aks4d1p1p7  40417  aks4d1p1p5  40418  limclner  43614  stoweidlem13  43976  stoweidlem26  43989  stoweidlem34  43997  stoweid  44026  stirlinglem12  44048  stirlinglem13  44049  fmtno4prmfac  45482  lighneallem4a  45518  requad01  45531  requad1  45532  requad2  45533  341fppr2  45644  4fppr1  45645  9fppr8  45647  gbowgt5  45672  sbgoldbwt  45687  sbgoldbst  45688  sbgoldbaltlem1  45689  sbgoldbalt  45691  sgoldbeven3prm  45693  nnsum4primes4  45699  nnsum4primesprm  45701  nnsum4primesgbe  45703  nnsum3primesle9  45704  nnsum4primesle9  45705  nnsum4primeseven  45710  nnsum4primesevenALTV  45711  wtgoldbnnsum4prm  45712  bgoldbnnsum3prm  45714  bgoldbtbndlem2  45716  bgoldbtbndlem3  45717  bgoldbtbnd  45719  tgblthelfgott  45725  ackval42  46500  itsclc0yqsollem2  46567  itscnhlinecirc02plem1  46586  2p2ne5  46959