Theorem 3re 10505

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 10491	. 2 |- 3 = ( 2 + 1 )
2		2re 10501	. . 3 |- 2 e. RR
3		1re 9495	. . 3 |- 1 e. RR
4	2, 3	readdcli 9509	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2538	1 |- 3 e. RR

Syntax hints:   e. wcel 1758  (class class class)co 6199   RRcr 9391   1c1 9393   + caddc 9395   2c2 10481   3c3 10482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-i2m1 9460  ax-1ne0 9461  ax-rrecex 9464  ax-cnre 9465

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202  df-2 10490  df-3 10491

This theorem is referenced by:  3cn  10506  4re  10508  3ne0  10526  4pos  10527  1lt3  10600  3lt4  10601  2lt4  10602  3lt5  10605  3lt6  10610  2lt6  10611  3lt7  10616  2lt7  10617  3lt8  10623  2lt8  10624  3lt9  10631  2lt9  10632  3lt10  10640  2lt10  10641  1le3  10648  4fvwrd4  11649  expnass  12087  hashtpg  12303  sqrlem7  12855  sqr9  12880  caucvgrlem  13267  caurcvgr  13268  ef01bndlem  13585  sin01bnd  13586  cos2bnd  13589  sin01gt0  13591  cos01gt0  13592  egt2lt3  13605  rpnnen2lem3  13616  rpnnen2lem4  13617  rpnnen2lem9  13622  matsca  18440  matvsca  18441  vitalilem4  21223  dveflem  21583  sincosq3sgn  22094  sincosq4sgn  22095  tangtx  22099  sincos6thpi  22109  pige3  22111  ang180lem2  22338  1cubrlem  22368  log2cnv  22471  log2tlbnd  22472  log2ub  22476  cxploglim2  22504  basellem5  22554  basellem9  22558  cht3  22643  ppiublem1  22673  ppiub  22675  chtub  22683  bposlem2  22756  bposlem3  22757  bposlem4  22758  bposlem5  22759  bposlem6  22760  bposlem8  22762  bposlem9  22763  lgsdir2lem1  22794  chebbnd1lem2  22851  chebbnd1lem3  22852  chebbnd1  22853  chto1ub  22857  dchrvmasumlem2  22879  dchrvmasumlema  22881  dchrvmasumiflem1  22882  mulog2sumlem2  22916  pntibndlem1  22970  pntibndlem2  22972  pntlemb  22978  pntlemk  22987  pntlemo  22988  axlowdimlem8  23346  axlowdimlem9  23347  axlowdimlem16  23354  axlowdimlem17  23355  axlowdim  23358  usgraexvlem  23464  usgraex3elv  23468  constr3pthlem3  23694  4cycl4v4e  23703  4cycl4dv4e  23705  konigsberg  23759  ex-dif  23781  ex-in  23783  ex-1st  23802  ex-2nd  23803  ex-fl  23805  stadd3i  25803  resvmulr  26447  problem3  27443  problem5  27445  bpoly4  28345  itg2addnclem2  28591  heiborlem5  28861  heiborlem6  28862  heiborlem7  28863  heiborlem8  28864  jm2.23  29492  jm2.20nn  29493  stoweidlem11  29953  stoweidlem13  29955  stoweidlem26  29968  stoweidlem34  29976  stoweidlem42  29984  stoweidlem59  30001  stoweidlem62  30004  stoweid  30005  wallispilem4  30010  nn01to3  30334  uzuzle23  30340  uz3m2nn  30342  extwwlkfablem2  30818  numclwlk1lem2f1  30834  frgraogt3nreg  30860  friendshipgt3  30861  friendship  30862  pgrpgt2nabel  30918