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

Theorem 3re 9817
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 9805 . 2  |-  3  =  ( 2  +  1 )
2 2re 9815 . . 3  |-  2  e.  RR
3 1re 8837 . . 3  |-  1  e.  RR
42, 3readdcli 8850 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2353 1  |-  3  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1684  (class class class)co 5858   RRcr 8736   1c1 8738    + caddc 8740   2c2 9795   3c3 9796
This theorem is referenced by:  3cn  9818  4re  9819  3ne0  9831  4pos  9832  1lt3  9888  3lt4  9889  2lt4  9890  3lt5  9893  3lt6  9898  2lt6  9899  3lt7  9904  2lt7  9905  3lt8  9911  2lt8  9912  3lt9  9919  2lt9  9920  3lt10  9928  2lt10  9929  fztpval  10845  expnass  11208  sqrlem7  11734  sqr9  11759  caucvgrlem  12145  caurcvgr  12146  ef01bndlem  12464  sin01bnd  12465  cos2bnd  12468  sin01gt0  12470  cos01gt0  12471  egt2lt3  12484  rpnnen2lem3  12495  rpnnen2lem4  12496  rpnnen2lem9  12501  vitalilem4  18966  iblcnlem1  19142  dveflem  19326  sincosq3sgn  19868  sincosq4sgn  19869  tangtx  19873  sincos6thpi  19883  pige3  19885  ang180lem2  20108  1cubrlem  20137  log2cnv  20240  log2tlbnd  20241  log2ub  20245  cxploglim2  20273  basellem5  20322  basellem9  20326  cht3  20411  ppiublem1  20441  ppiub  20443  chtub  20451  bposlem2  20524  bposlem3  20525  bposlem4  20526  bposlem5  20527  bposlem6  20528  bposlem8  20530  bposlem9  20531  lgsdir2lem1  20562  chebbnd1lem2  20619  chebbnd1lem3  20620  chebbnd1  20621  chto1ub  20625  dchrvmasumlem2  20647  dchrvmasumlema  20649  dchrvmasumiflem1  20650  mulog2sumlem2  20684  pntibndlem1  20738  pntibndlem2  20740  pntlemb  20746  pntlemk  20755  pntlemo  20756  ex-dif  20810  ex-in  20812  ex-pss  20815  ex-fv  20830  ex-1st  20831  ex-2nd  20832  ex-fl  20834  stadd3i  22828  konigsberg  23911  axlowdimlem7  24576  axlowdimlem8  24577  axlowdimlem9  24578  axlowdimlem13  24582  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  bpoly4  24794  cntrset  25602  heiborlem5  26539  heiborlem6  26540  heiborlem7  26541  heiborlem8  26542  jm2.23  27089  jm2.20nn  27090  matsca  27470  matvsca  27471  stoweidlem11  27760  stoweidlem13  27762  stoweidlem26  27775  stoweidlem34  27783  stoweidlem42  27791  stoweidlem59  27808  stoweidlem62  27811  stoweid  27812  wallispilem4  27817  usgraexvlem  28127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rrecex 8809  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-2 9804  df-3 9805
  Copyright terms: Public domain W3C validator