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

Theorem 3re 10055
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 10043 . 2  |-  3  =  ( 2  +  1 )
2 2re 10053 . . 3  |-  2  e.  RR
3 1re 9074 . . 3  |-  1  e.  RR
42, 3readdcli 9087 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2500 1  |-  3  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1725  (class class class)co 6067   RRcr 8973   1c1 8975    + caddc 8977   2c2 10033   3c3 10034
This theorem is referenced by:  3cn  10056  4re  10057  3ne0  10069  4pos  10070  1lt3  10128  3lt4  10129  2lt4  10130  3lt5  10133  3lt6  10138  2lt6  10139  3lt7  10144  2lt7  10145  3lt8  10151  2lt8  10152  3lt9  10159  2lt9  10160  3lt10  10168  2lt10  10169  fztpval  11091  4fvwrd4  11104  expnass  11469  hashtpg  11674  sqrlem7  12037  sqr9  12062  caucvgrlem  12449  caurcvgr  12450  ef01bndlem  12768  sin01bnd  12769  cos2bnd  12772  sin01gt0  12774  cos01gt0  12775  egt2lt3  12788  rpnnen2lem3  12799  rpnnen2lem4  12800  rpnnen2lem9  12805  vitalilem4  19486  iblcnlem1  19662  dveflem  19846  sincosq3sgn  20391  sincosq4sgn  20392  tangtx  20396  sincos6thpi  20406  pige3  20408  ang180lem2  20635  1cubrlem  20664  log2cnv  20767  log2tlbnd  20768  log2ub  20772  cxploglim2  20800  basellem5  20850  basellem9  20854  cht3  20939  ppiublem1  20969  ppiub  20971  chtub  20979  bposlem2  21052  bposlem3  21053  bposlem4  21054  bposlem5  21055  bposlem6  21056  bposlem8  21058  bposlem9  21059  lgsdir2lem1  21090  chebbnd1lem2  21147  chebbnd1lem3  21148  chebbnd1  21149  chto1ub  21153  dchrvmasumlem2  21175  dchrvmasumlema  21177  dchrvmasumiflem1  21178  mulog2sumlem2  21212  pntibndlem1  21266  pntibndlem2  21268  pntlemb  21274  pntlemk  21283  pntlemo  21284  usgraexvlem  21397  usgraex3elv  21401  constr3pthlem3  21627  4cycl4v4e  21636  4cycl4dv4e  21638  konigsberg  21692  ex-dif  21714  ex-in  21716  ex-pss  21719  ex-fv  21734  ex-1st  21735  ex-2nd  21736  ex-fl  21738  stadd3i  23734  axlowdimlem7  25830  axlowdimlem8  25831  axlowdimlem9  25832  axlowdimlem13  25836  axlowdimlem16  25839  axlowdimlem17  25840  axlowdim  25843  bpoly4  26048  itg2addnclem2  26198  heiborlem5  26456  heiborlem6  26457  heiborlem7  26458  heiborlem8  26459  jm2.23  26999  jm2.20nn  27000  matsca  27380  matvsca  27381  stoweidlem11  27669  stoweidlem13  27671  stoweidlem26  27684  stoweidlem34  27692  stoweidlem42  27700  stoweidlem59  27717  stoweidlem62  27720  stoweid  27721  wallispilem4  27726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-1cn 9032  ax-icn 9033  ax-addcl 9034  ax-addrcl 9035  ax-mulcl 9036  ax-mulrcl 9037  ax-i2m1 9042  ax-1ne0 9043  ax-rrecex 9046  ax-cnre 9047
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-iota 5404  df-fv 5448  df-ov 6070  df-2 10042  df-3 10043
  Copyright terms: Public domain W3C validator