Theorem 3re 10683

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

Assertion

Ref	Expression
3re	|- 3 e. RR

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 10669	. 2 |- 3 = ( 2 + 1 )
2		2re 10679	. . 3 |- 2 e. RR
3		1re 9641	. . 3 |- 1 e. RR
4	2, 3	readdcli 9655	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2513	1 |- 3 e. RR

Syntax hints:   e. wcel 1870  (class class class)co 6305   RRcr 9537   1c1 9539   + caddc 9541   2c2 10659   3c3 10660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-i2m1 9606  ax-1ne0 9607  ax-rrecex 9610  ax-cnre 9611

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-2 10668  df-3 10669

This theorem is referenced by:  3cn  10684  4re  10686  3ne0  10704  4pos  10705  1lt3  10778  3lt4  10779  2lt4  10780  3lt5  10783  3lt6  10788  2lt6  10789  3lt7  10794  2lt7  10795  3lt8  10801  2lt8  10802  3lt9  10809  2lt9  10810  3lt10  10818  2lt10  10819  1le3  10826  uzuzle23  11199  uz3m2nn  11201  nn01to3  11257  expnass  12377  hashtpg  12632  sqrlem7  13291  sqrt9  13316  caucvgrlem  13714  caucvgrlemOLD  13715  caurcvgr  13716  caurcvgrOLD  13717  bpoly4  14090  ef01bndlem  14216  sin01bnd  14217  cos2bnd  14220  sin01gt0  14222  cos01gt0  14223  egt2lt3  14236  rpnnen2lem3  14247  rpnnen2lem4  14248  rpnnen2lem9  14253  matsca  19371  matvsca  19372  vitalilem4  22446  dveflem  22808  sincosq3sgn  23320  sincosq4sgn  23321  tangtx  23325  sincos6thpi  23335  pige3  23337  ang180lem2  23604  1cubrlem  23632  log2cnv  23735  log2tlbnd  23736  log2ub  23740  cxploglim2  23769  basellem5  23874  basellem9  23878  cht3  23963  ppiublem1  23993  ppiub  23995  chtub  24003  bposlem2  24076  bposlem3  24077  bposlem4  24078  bposlem5  24079  bposlem6  24080  bposlem8  24082  bposlem9  24083  lgsdir2lem1  24114  chebbnd1lem2  24171  chebbnd1lem3  24172  chebbnd1  24173  chto1ub  24177  dchrvmasumlem2  24199  dchrvmasumlema  24201  dchrvmasumiflem1  24202  mulog2sumlem2  24236  pntibndlem1  24290  pntibndlem2  24292  pntlemb  24298  pntlemk  24307  pntlemo  24308  istrkg3ld  24372  axlowdimlem8  24825  axlowdimlem9  24826  axlowdimlem16  24833  axlowdimlem17  24834  axlowdim  24837  usgraexvlem  24968  usgraex3elv  24972  constr3pthlem3  25230  4cycl4v4e  25239  4cycl4dv4e  25241  konigsberg  25560  extwwlkfablem2  25651  numclwlk1lem2f1  25667  frgraogt3nreg  25693  friendshipgt3  25694  friendship  25695  ex-dif  25718  ex-in  25720  ex-1st  25739  ex-2nd  25740  ex-fl  25742  stadd3i  27736  resvmulr  28437  problem3  30087  problem5  30089  pigt3  31642  poimirlem9  31653  itg2addnclem2  31698  heiborlem5  31851  heiborlem6  31852  heiborlem7  31853  heiborlem8  31854  jm2.23  35557  jm2.20nn  35558  3rp  37106  lt4addmuld  37133  stoweidlem11  37440  stoweidlem13  37442  stoweidlem26  37455  stoweidlem34  37464  stoweidlem42  37472  stoweidlem59  37489  stoweidlem62  37492  stoweidlem62OLD  37493  stoweid  37494  wallispilem4  37499  fourierdlem87  37625  gbegt5  38252  gboage9  38255  bgoldbwt  38268  bgoldbst  38269  sgoldbalt  38272  nnsum3primes4  38273  nnsum4primes4  38274  nnsum3primesprm  38275  nnsum4primesprm  38276  nnsum3primesgbe  38277  nnsum4primesgbe  38278  nnsum3primesle9  38279  nnsum4primesle9  38280  evengpop3  38283  evengpoap3  38284  nnsum4primeseven  38285  nnsum4primesevenALTV  38286  wtgoldbnnsum4prm  38287  bgoldbnnsum3prm  38289  pgrpgt2nabl  38911  3halfnz  39078