Theorem 3re 10971

Description: The number 3 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
3re	⊢ 3 ∈ ℝ

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 10957	. 2 ⊢ 3 = (2 + 1)
2		2re 10967	. . 3 ⊢ 2 ∈ ℝ
3		1re 9918	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 9932	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2684	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814  1c1 9816   + caddc 9818  2c2 10947  3c3 10948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-2 10956  df-3 10957

This theorem is referenced by:  3cn  10972  4re  10974  3ne0  10992  4pos  10993  1lt3  11073  3lt4  11074  2lt4  11075  3lt5  11078  3lt6  11083  2lt6  11084  3lt7  11089  2lt7  11090  3lt8  11096  2lt8  11097  3lt9  11104  2lt9  11105  3lt10OLD  11113  2lt10OLD  11114  1le3  11121  3halfnz  11332  3lt10  11555  2lt10  11556  uzuzle23  11605  uz3m2nn  11607  nn01to3  11657  3rp  11714  fz0to4untppr  12311  expnass  12832  hashtpg  13121  sqrlem7  13837  sqrt9  13862  caucvgrlem  14251  caurcvgr  14252  bpoly4  14629  ef01bndlem  14753  sin01bnd  14754  cos2bnd  14757  sin01gt0  14759  cos01gt0  14760  egt2lt3  14773  rpnnen2lem3  14784  rpnnen2lem4  14785  rpnnen2lem9  14790  flodddiv4  14975  matsca  20040  matvsca  20041  vitalilem4  23186  dveflem  23546  sincosq3sgn  24056  sincosq4sgn  24057  tangtx  24061  sincos6thpi  24071  pige3  24073  ang180lem2  24340  1cubrlem  24368  log2cnv  24471  log2tlbnd  24472  log2ub  24476  cxploglim2  24505  basellem5  24611  basellem9  24615  cht3  24699  ppiublem1  24727  ppiub  24729  chtub  24737  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem8  24816  bposlem9  24817  lgsdir2lem1  24850  2lgslem3  24929  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  chto1ub  24965  dchrvmasumlem2  24987  dchrvmasumlema  24989  dchrvmasumiflem1  24990  mulog2sumlem2  25024  pntibndlem1  25078  pntibndlem2  25080  pntlemb  25086  pntlemk  25095  pntlemo  25096  istrkg3ld  25160  axlowdimlem8  25629  axlowdimlem9  25630  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  usgraex3elv  25927  constr3pthlem3  26185  4cycl4v4e  26194  4cycl4dv4e  26196  konigsberg  26514  extwwlkfablem2  26605  numclwlk1lem2f1  26621  frgraogt3nreg  26647  friendshipgt3  26648  friendship  26649  ex-dif  26672  ex-in  26674  ex-1st  26693  ex-2nd  26694  ex-fl  26696  ex-ceil  26697  ex-gcd  26706  resvmulr  29166  problem3  30815  problem5  30817  pigt3  32572  poimirlem9  32588  itg2addnclem2  32632  heiborlem5  32784  heiborlem6  32785  heiborlem7  32786  heiborlem8  32787  jm2.23  36581  jm2.20nn  36582  lt4addmuld  38461  stoweidlem11  38904  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  stoweidlem42  38935  stoweidlem59  38952  stoweidlem62  38955  stoweid  38956  wallispilem4  38961  fourierdlem87  39086  smfmullem4  39679  fmtnoge3  39980  fmtnoprmfac2lem1  40016  31prm  40050  gbegt5  40183  gboage9  40186  bgoldbwt  40199  bgoldbst  40200  sgoldbalt  40203  nnsum3primes4  40204  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum3primesgbe  40208  nnsum4primesgbe  40209  nnsum3primesle9  40210  nnsum4primesle9  40211  evengpop3  40214  evengpoap3  40215  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  upgr4cycl4dv4e  41352  konigsbergiedgw  41416  konigsbergiedgwOLD  41417  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  konigsberglem4  41425  av-numclwlk1lem2f1  41524  av-frgraogt3nreg  41551  av-friendshipgt3  41552  av-friendship  41553  pgrpgt2nabl  41941