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

Theorem 3re 9833
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 9821 . 2  |-  3  =  ( 2  +  1 )
2 2re 9831 . . 3  |-  2  e.  RR
3 1re 8853 . . 3  |-  1  e.  RR
42, 3readdcli 8866 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2366 1  |-  3  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1696  (class class class)co 5874   RRcr 8752   1c1 8754    + caddc 8756   2c2 9811   3c3 9812
This theorem is referenced by:  3cn  9834  4re  9835  3ne0  9847  4pos  9848  1lt3  9904  3lt4  9905  2lt4  9906  3lt5  9909  3lt6  9914  2lt6  9915  3lt7  9920  2lt7  9921  3lt8  9927  2lt8  9928  3lt9  9935  2lt9  9936  3lt10  9944  2lt10  9945  fztpval  10861  expnass  11224  sqrlem7  11750  sqr9  11775  caucvgrlem  12161  caurcvgr  12162  ef01bndlem  12480  sin01bnd  12481  cos2bnd  12484  sin01gt0  12486  cos01gt0  12487  egt2lt3  12500  rpnnen2lem3  12511  rpnnen2lem4  12512  rpnnen2lem9  12517  vitalilem4  18982  iblcnlem1  19158  dveflem  19342  sincosq3sgn  19884  sincosq4sgn  19885  tangtx  19889  sincos6thpi  19899  pige3  19901  ang180lem2  20124  1cubrlem  20153  log2cnv  20256  log2tlbnd  20257  log2ub  20261  cxploglim2  20289  basellem5  20338  basellem9  20342  cht3  20427  ppiublem1  20457  ppiub  20459  chtub  20467  bposlem2  20540  bposlem3  20541  bposlem4  20542  bposlem5  20543  bposlem6  20544  bposlem8  20546  bposlem9  20547  lgsdir2lem1  20578  chebbnd1lem2  20635  chebbnd1lem3  20636  chebbnd1  20637  chto1ub  20641  dchrvmasumlem2  20663  dchrvmasumlema  20665  dchrvmasumiflem1  20666  mulog2sumlem2  20700  pntibndlem1  20754  pntibndlem2  20756  pntlemb  20762  pntlemk  20771  pntlemo  20772  ex-dif  20826  ex-in  20828  ex-pss  20831  ex-fv  20846  ex-1st  20847  ex-2nd  20848  ex-fl  20850  stadd3i  22844  konigsberg  23926  axlowdimlem7  24648  axlowdimlem8  24649  axlowdimlem9  24650  axlowdimlem13  24654  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  bpoly4  24866  itg2addnclem2  25004  itg2addnc  25005  cntrset  25705  heiborlem5  26642  heiborlem6  26643  heiborlem7  26644  heiborlem8  26645  jm2.23  27192  jm2.20nn  27193  matsca  27573  matvsca  27574  stoweidlem11  27863  stoweidlem13  27865  stoweidlem26  27878  stoweidlem34  27886  stoweidlem42  27894  stoweidlem59  27911  stoweidlem62  27914  stoweid  27915  wallispilem4  27920  hashtpg  28217  4fvwrd4  28220  usgraexvlem  28261  constr3pthlem3  28403  4cycl4v4e  28412  4cycl4dv4e  28414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-2 9820  df-3 9821
  Copyright terms: Public domain W3C validator