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

Theorem 3re 10605
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 10591 . 2  |-  3  =  ( 2  +  1 )
2 2re 10601 . . 3  |-  2  e.  RR
3 1re 9591 . . 3  |-  1  e.  RR
42, 3readdcli 9605 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2551 1  |-  3  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767  (class class class)co 6282   RRcr 9487   1c1 9489    + caddc 9491   2c2 10581   3c3 10582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-i2m1 9556  ax-1ne0 9557  ax-rrecex 9560  ax-cnre 9561
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285  df-2 10590  df-3 10591
This theorem is referenced by:  3cn  10606  4re  10608  3ne0  10626  4pos  10627  1lt3  10700  3lt4  10701  2lt4  10702  3lt5  10705  3lt6  10710  2lt6  10711  3lt7  10716  2lt7  10717  3lt8  10723  2lt8  10724  3lt9  10731  2lt9  10732  3lt10  10740  2lt10  10741  1le3  10748  uzuzle23  11118  uz3m2nn  11120  nn01to3  11171  4fvwrd4  11786  expnass  12235  hashtpg  12483  sqrlem7  13039  sqrt9  13064  caucvgrlem  13451  caurcvgr  13452  ef01bndlem  13773  sin01bnd  13774  cos2bnd  13777  sin01gt0  13779  cos01gt0  13780  egt2lt3  13793  rpnnen2lem3  13804  rpnnen2lem4  13805  rpnnen2lem9  13810  matsca  18681  matvsca  18682  vitalilem4  21752  dveflem  22112  sincosq3sgn  22623  sincosq4sgn  22624  tangtx  22628  sincos6thpi  22638  pige3  22640  ang180lem2  22867  1cubrlem  22897  log2cnv  23000  log2tlbnd  23001  log2ub  23005  cxploglim2  23033  basellem5  23083  basellem9  23087  cht3  23172  ppiublem1  23202  ppiub  23204  chtub  23212  bposlem2  23285  bposlem3  23286  bposlem4  23287  bposlem5  23288  bposlem6  23289  bposlem8  23291  bposlem9  23292  lgsdir2lem1  23323  chebbnd1lem2  23380  chebbnd1lem3  23381  chebbnd1  23382  chto1ub  23386  dchrvmasumlem2  23408  dchrvmasumlema  23410  dchrvmasumiflem1  23411  mulog2sumlem2  23445  pntibndlem1  23499  pntibndlem2  23501  pntlemb  23507  pntlemk  23516  pntlemo  23517  axlowdimlem8  23925  axlowdimlem9  23926  axlowdimlem16  23933  axlowdimlem17  23934  axlowdim  23937  usgraexvlem  24068  usgraex3elv  24072  constr3pthlem3  24330  4cycl4v4e  24339  4cycl4dv4e  24341  konigsberg  24660  extwwlkfablem2  24752  numclwlk1lem2f1  24768  frgraogt3nreg  24794  friendshipgt3  24795  friendship  24796  ex-dif  24818  ex-in  24820  ex-1st  24839  ex-2nd  24840  ex-fl  24842  stadd3i  26840  resvmulr  27485  problem3  28493  problem5  28495  bpoly4  29395  itg2addnclem2  29642  heiborlem5  29912  heiborlem6  29913  heiborlem7  29914  heiborlem8  29915  jm2.23  30542  jm2.20nn  30543  3rp  31048  lt4addmuld  31083  stoweidlem11  31311  stoweidlem13  31313  stoweidlem26  31326  stoweidlem34  31334  stoweidlem42  31342  stoweidlem59  31359  stoweidlem62  31362  stoweid  31363  wallispilem4  31368  fourierdlem87  31494  pgrpgt2nabl  32024
  Copyright terms: Public domain W3C validator