Theorem 3re 10383

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 10369	. 2 |- 3 = ( 2 + 1 )
2		2re 10379	. . 3 |- 2 e. RR
3		1re 9373	. . 3 |- 1 e. RR
4	2, 3	readdcli 9387	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2503	1 |- 3 e. RR

Syntax hints:   e. wcel 1755  (class class class)co 6080   RRcr 9269   1c1 9271   + caddc 9273   2c2 10359   3c3 10360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rrecex 9342  ax-cnre 9343

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-2 10368  df-3 10369

This theorem is referenced by:  3cn  10384  4re  10386  3ne0  10404  4pos  10405  1lt3  10478  3lt4  10479  2lt4  10480  3lt5  10483  3lt6  10488  2lt6  10489  3lt7  10494  2lt7  10495  3lt8  10501  2lt8  10502  3lt9  10509  2lt9  10510  3lt10  10518  2lt10  10519  1le3  10526  4fvwrd4  11517  expnass  11955  hashtpg  12170  sqrlem7  12722  sqr9  12747  caucvgrlem  13134  caurcvgr  13135  ef01bndlem  13451  sin01bnd  13452  cos2bnd  13455  sin01gt0  13457  cos01gt0  13458  egt2lt3  13471  rpnnen2lem3  13482  rpnnen2lem4  13483  rpnnen2lem9  13488  matsca  18158  matvsca  18159  vitalilem4  20933  dveflem  21293  sincosq3sgn  21847  sincosq4sgn  21848  tangtx  21852  sincos6thpi  21862  pige3  21864  ang180lem2  22091  1cubrlem  22121  log2cnv  22224  log2tlbnd  22225  log2ub  22229  cxploglim2  22257  basellem5  22307  basellem9  22311  cht3  22396  ppiublem1  22426  ppiub  22428  chtub  22436  bposlem2  22509  bposlem3  22510  bposlem4  22511  bposlem5  22512  bposlem6  22513  bposlem8  22515  bposlem9  22516  lgsdir2lem1  22547  chebbnd1lem2  22604  chebbnd1lem3  22605  chebbnd1  22606  chto1ub  22610  dchrvmasumlem2  22632  dchrvmasumlema  22634  dchrvmasumiflem1  22635  mulog2sumlem2  22669  pntibndlem1  22723  pntibndlem2  22725  pntlemb  22731  pntlemk  22740  pntlemo  22741  axlowdimlem8  23018  axlowdimlem9  23019  axlowdimlem16  23026  axlowdimlem17  23027  axlowdim  23030  usgraexvlem  23136  usgraex3elv  23140  constr3pthlem3  23366  4cycl4v4e  23375  4cycl4dv4e  23377  konigsberg  23431  ex-dif  23453  ex-in  23455  ex-1st  23474  ex-2nd  23475  ex-fl  23477  stadd3i  25475  resvmulr  26157  problem3  27148  problem5  27150  bpoly4  28049  itg2addnclem2  28288  heiborlem5  28558  heiborlem6  28559  heiborlem7  28560  heiborlem8  28561  jm2.23  29190  jm2.20nn  29191  stoweidlem11  29652  stoweidlem13  29654  stoweidlem26  29667  stoweidlem34  29675  stoweidlem42  29683  stoweidlem59  29700  stoweidlem62  29703  stoweid  29704  wallispilem4  29709  nn01to3  30033  uzuzle23  30039  uz3m2nn  30041  extwwlkfablem2  30517  numclwlk1lem2f1  30533  frgraogt3nreg  30559  friendshipgt3  30560  friendship  30561  pgrpgt2nabel  30601