Theorem 3re 10630

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 10616	. 2 |- 3 = ( 2 + 1 )
2		2re 10626	. . 3 |- 2 e. RR
3		1re 9612	. . 3 |- 1 e. RR
4	2, 3	readdcli 9626	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2541	1 |- 3 e. RR

Syntax hints:   e. wcel 1819  (class class class)co 6296   RRcr 9508   1c1 9510   + caddc 9512   2c2 10606   3c3 10607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-i2m1 9577  ax-1ne0 9578  ax-rrecex 9581  ax-cnre 9582

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299  df-2 10615  df-3 10616

This theorem is referenced by:  3cn  10631  4re  10633  3ne0  10651  4pos  10652  1lt3  10725  3lt4  10726  2lt4  10727  3lt5  10730  3lt6  10735  2lt6  10736  3lt7  10741  2lt7  10742  3lt8  10748  2lt8  10749  3lt9  10756  2lt9  10757  3lt10  10765  2lt10  10766  1le3  10773  uzuzle23  11146  uz3m2nn  11148  nn01to3  11200  expnass  12275  hashtpg  12526  sqrlem7  13093  sqrt9  13118  caucvgrlem  13506  caurcvgr  13507  ef01bndlem  13930  sin01bnd  13931  cos2bnd  13934  sin01gt0  13936  cos01gt0  13937  egt2lt3  13950  rpnnen2lem3  13961  rpnnen2lem4  13962  rpnnen2lem9  13967  matsca  19043  matvsca  19044  vitalilem4  22145  dveflem  22505  sincosq3sgn  23018  sincosq4sgn  23019  tangtx  23023  sincos6thpi  23033  pige3  23035  ang180lem2  23267  1cubrlem  23297  log2cnv  23400  log2tlbnd  23401  log2ub  23405  cxploglim2  23433  basellem5  23483  basellem9  23487  cht3  23572  ppiublem1  23602  ppiub  23604  chtub  23612  bposlem2  23685  bposlem3  23686  bposlem4  23687  bposlem5  23688  bposlem6  23689  bposlem8  23691  bposlem9  23692  lgsdir2lem1  23723  chebbnd1lem2  23780  chebbnd1lem3  23781  chebbnd1  23782  chto1ub  23786  dchrvmasumlem2  23808  dchrvmasumlema  23810  dchrvmasumiflem1  23811  mulog2sumlem2  23845  pntibndlem1  23899  pntibndlem2  23901  pntlemb  23907  pntlemk  23916  pntlemo  23917  axlowdimlem8  24378  axlowdimlem9  24379  axlowdimlem16  24386  axlowdimlem17  24387  axlowdim  24390  usgraexvlem  24521  usgraex3elv  24525  constr3pthlem3  24783  4cycl4v4e  24792  4cycl4dv4e  24794  konigsberg  25113  extwwlkfablem2  25204  numclwlk1lem2f1  25220  frgraogt3nreg  25246  friendshipgt3  25247  friendship  25248  ex-dif  25270  ex-in  25272  ex-1st  25291  ex-2nd  25292  ex-fl  25294  stadd3i  27293  resvmulr  27978  problem3  29196  problem5  29198  bpoly4  29983  itg2addnclem2  30229  heiborlem5  30473  heiborlem6  30474  heiborlem7  30475  heiborlem8  30476  jm2.23  31100  jm2.20nn  31101  3rp  31632  lt4addmuld  31667  stoweidlem11  31954  stoweidlem13  31956  stoweidlem26  31969  stoweidlem34  31977  stoweidlem42  31985  stoweidlem59  32002  stoweidlem62  32005  stoweid  32006  wallispilem4  32011  fourierdlem87  32137  pgrpgt2nabl  33061