MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3re Unicode version

Theorem 3re 9996
Description: The number 3 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
3re  |-  3  e.  RR

Proof of Theorem 3re
StepHypRef Expression
1 df-3 9984 . 2  |-  3  =  ( 2  +  1 )
2 2re 9994 . . 3  |-  2  e.  RR
3 1re 9016 . . 3  |-  1  e.  RR
42, 3readdcli 9029 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2450 1  |-  3  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1717  (class class class)co 6013   RRcr 8915   1c1 8917    + caddc 8919   2c2 9974   3c3 9975
This theorem is referenced by:  3cn  9997  4re  9998  3ne0  10010  4pos  10011  1lt3  10069  3lt4  10070  2lt4  10071  3lt5  10074  3lt6  10079  2lt6  10080  3lt7  10085  2lt7  10086  3lt8  10092  2lt8  10093  3lt9  10100  2lt9  10101  3lt10  10109  2lt10  10110  fztpval  11031  4fvwrd4  11044  expnass  11406  hashtpg  11611  sqrlem7  11974  sqr9  11999  caucvgrlem  12386  caurcvgr  12387  ef01bndlem  12705  sin01bnd  12706  cos2bnd  12709  sin01gt0  12711  cos01gt0  12712  egt2lt3  12725  rpnnen2lem3  12736  rpnnen2lem4  12737  rpnnen2lem9  12742  vitalilem4  19363  iblcnlem1  19539  dveflem  19723  sincosq3sgn  20268  sincosq4sgn  20269  tangtx  20273  sincos6thpi  20283  pige3  20285  ang180lem2  20512  1cubrlem  20541  log2cnv  20644  log2tlbnd  20645  log2ub  20649  cxploglim2  20677  basellem5  20727  basellem9  20731  cht3  20816  ppiublem1  20846  ppiub  20848  chtub  20856  bposlem2  20929  bposlem3  20930  bposlem4  20931  bposlem5  20932  bposlem6  20933  bposlem8  20935  bposlem9  20936  lgsdir2lem1  20967  chebbnd1lem2  21024  chebbnd1lem3  21025  chebbnd1  21026  chto1ub  21030  dchrvmasumlem2  21052  dchrvmasumlema  21054  dchrvmasumiflem1  21055  mulog2sumlem2  21089  pntibndlem1  21143  pntibndlem2  21145  pntlemb  21151  pntlemk  21160  pntlemo  21161  usgraexvlem  21273  usgraex3elv  21277  constr3pthlem3  21485  4cycl4v4e  21494  4cycl4dv4e  21496  konigsberg  21550  ex-dif  21572  ex-in  21574  ex-pss  21577  ex-fv  21592  ex-1st  21593  ex-2nd  21594  ex-fl  21596  stadd3i  23592  axlowdimlem7  25594  axlowdimlem8  25595  axlowdimlem9  25596  axlowdimlem13  25600  axlowdimlem16  25603  axlowdimlem17  25604  axlowdim  25607  bpoly4  25812  itg2addnclem2  25951  itg2addnc  25952  heiborlem5  26208  heiborlem6  26209  heiborlem7  26210  heiborlem8  26211  jm2.23  26751  jm2.20nn  26752  matsca  27132  matvsca  27133  stoweidlem11  27421  stoweidlem13  27423  stoweidlem26  27436  stoweidlem34  27444  stoweidlem42  27452  stoweidlem59  27469  stoweidlem62  27472  stoweid  27473  wallispilem4  27478
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-addrcl 8977  ax-mulcl 8978  ax-mulrcl 8979  ax-i2m1 8984  ax-1ne0 8985  ax-rrecex 8988  ax-cnre 8989
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-iota 5351  df-fv 5395  df-ov 6016  df-2 9983  df-3 9984
  Copyright terms: Public domain W3C validator