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

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

Proof of Theorem 2re
StepHypRef Expression
1 df-2 9806 . 2  |-  2  =  ( 1  +  1 )
2 1re 8839 . . 3  |-  1  e.  RR
32, 2readdcli 8852 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2355 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1686  (class class class)co 5860   RRcr 8738   1c1 8740    + caddc 8742   2c2 9797
This theorem is referenced by:  2cn  9818  3re  9819  2ne0  9831  3pos  9832  2lt3  9889  1lt3  9890  2lt4  9892  1lt4  9893  2lt5  9896  2lt6  9901  1lt6  9902  2lt7  9907  1lt7  9908  2lt8  9914  1lt8  9915  2lt9  9922  1lt9  9923  2lt10  9931  1lt10  9932  halfgt0  9934  halflt1  9935  halfpm6th  9938  rehalfcl  9940  halfpos2  9943  halfnneg2  9945  addltmul  9949  nominpos  9950  avglt1  9951  avglt2  9952  nn0lele2xi  10018  halfnz  10092  2rp  10361  fzprval  10846  fztpval  10847  flhalf  10956  expubnd  11164  expmulnbnd  11235  nn0opthlem2  11286  faclbnd2  11306  faclbnd4lem1  11308  faclbnd5  11313  hashfun  11391  sqrlem7  11736  sqr4  11760  sqr2gt1lt2  11762  abstri  11816  rddif  11826  absrdbnd  11827  sqreulem  11845  amgm2  11855  abs3lemi  11895  caucvgrlem  12147  iseralt  12159  climcndslem1  12310  climcndslem2  12311  climcnds  12312  geoihalfsum  12340  efcllem  12361  ege2le3  12373  ef01bndlem  12466  cos01bnd  12468  cos2bnd  12470  cos01gt0  12473  sin02gt0  12474  sincos2sgn  12476  sin4lt0  12477  eirrlem  12484  egt2lt3  12486  epos  12487  sqr2re  12530  oexpneg  12592  bitsp1o  12626  bitsfzolem  12627  bitsfzo  12628  bitsmod  12629  bitsfi  12630  bitsinv1lem  12634  isprm3  12769  oddprm  12870  iserodd  12890  prmreclem2  12966  prmreclem6  12970  4sqlem11  13004  4sqlem12  13005  2expltfac  13107  oppgtset  14827  efgredleme  15054  mgpsca  15334  mgptset  15335  mgpds  15337  abvtrivd  15607  xmetge0  17911  bl2in  17959  metnrmlem3  18367  iihalf1  18431  iihalf2  18433  pcoass  18524  tchcphlem1  18667  minveclem2  18792  minveclem4  18798  pjthlem1  18803  ovolunlem1a  18857  dyadss  18951  opnmbllem  18958  vitalilem2  18966  vitalilem4  18968  mbfi1fseqlem5  19076  lhop1lem  19362  aaliou3lem1  19724  aaliou3lem2  19725  aaliou3lem3  19726  aaliou3lem8  19727  pilem2  19830  pilem3  19831  pipos  19835  sinhalfpilem  19836  sincosq1lem  19867  sincosq1sgn  19868  sincosq2sgn  19869  sincosq3sgn  19870  sincosq4sgn  19871  tangtx  19875  sinq12gt0  19877  sincos4thpi  19883  tan4thpi  19884  sincos6thpi  19885  sineq0  19891  cosordlem  19895  tanord1  19901  efif1olem1  19906  efif1olem2  19907  efif1olem4  19909  efif1o  19910  efifo  19911  logsqr  20053  cxpcn3lem  20089  root1id  20096  root1eq1  20097  root1cj  20098  cxpeq  20099  ang180lem1  20109  ang180lem2  20110  isosctrlem1  20120  chordthmlem2  20132  1cubrlem  20139  atancj  20208  atantan  20221  atanbndlem  20223  atans2  20229  leibpilem1  20238  leibpi  20240  log2tlbnd  20243  log2ublem2  20245  log2ub  20247  divsqrsumlem  20276  harmonicbnd3  20303  basellem1  20320  basellem2  20321  basellem3  20322  basellem5  20324  ppisval  20343  chtdif  20398  ppidif  20403  ppinncl  20414  chtrpcl  20415  ppieq0  20416  ppiltx  20417  ppiublem1  20443  ppiub  20445  chpeq0  20449  chteq0  20450  chtublem  20452  chtub  20453  chpval2  20459  chpub  20461  mersenne  20468  perfectlem1  20470  perfectlem2  20471  dchrptlem1  20505  dchrptlem2  20506  bcmono  20518  bclbnd  20521  bpos1lem  20523  bposlem1  20525  bposlem2  20526  bposlem3  20527  bposlem4  20528  bposlem5  20529  bposlem6  20530  bposlem7  20531  bposlem8  20532  bposlem9  20533  lgslem1  20537  lgsdirprm  20570  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem3  20592  lgseisen  20594  lgsquadlem1  20595  lgsquadlem2  20596  m1lgs  20603  2sqlem11  20616  chebbnd1lem1  20620  chebbnd1lem2  20621  chebbnd1lem3  20622  chebbnd1  20623  chtppilimlem1  20624  chtppilimlem2  20625  chtppilim  20626  chto1ub  20627  chebbnd2  20628  chto1lb  20629  chpchtlim  20630  chpo1ub  20631  chpo1ubb  20632  rplogsumlem1  20635  rplogsumlem2  20636  dchrisumlem2  20641  dchrisumlem3  20642  dchrvmasumiflem1  20652  dchrisum0fno1  20662  dchrisum0re  20664  dchrisum0lem1b  20666  dchrisum0lem1  20667  dchrisum0lem2  20669  rplogsum  20678  mulog2sumlem1  20685  mulog2sumlem2  20686  log2sumbnd  20695  selberglem2  20697  selbergb  20700  selberg2b  20703  chpdifbndlem1  20704  logdivbnd  20707  selberg3lem1  20708  selberg3  20710  selberg4lem1  20711  selberg4  20712  pntrmax  20715  pntrsumbnd2  20718  selberg3r  20720  selberg4r  20721  selberg34r  20722  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntrlog2bndlem6  20734  pntrlog2bnd  20735  pntpbnd1a  20736  pntpbnd1  20737  pntpbnd2  20738  pntpbnd  20739  pntibndlem2  20742  pntibndlem3  20743  pntibnd  20744  pntlemb  20748  pntlemg  20749  pntlemh  20750  pntlemr  20753  pntlemk  20757  pntlemo  20758  pnt2  20764  pnt  20765  ostth2lem1  20769  ostth3  20789  ex-pss  20817  ex-res  20830  ex-fv  20832  ex-fl  20836  nvge0  21242  ipidsq  21288  minvecolem2  21456  minvecolem4  21461  normlem7  21697  norm-ii-i  21718  norm3lem  21730  norm3lemt  21733  normpar2i  21737  bcsiALT  21760  pjhthlem1  21972  opsqrlem6  22727  cdj3lem1  23016  addltmulALT  23028  sqsscirc1  23294  rnlogblem  23403  coinfliplem  23681  coinflipspace  23683  zetacvg  23691  subfacp1lem1  23712  subfacp1lem5  23717  subfacval3  23722  umgrafi  23876  konigsberg  23913  circum  24009  4bc2eq6  24101  axlowdimlem3  24574  axlowdimlem4  24575  axlowdimlem6  24577  axlowdimlem16  24587  axlowdimlem17  24588  axlowdim  24591  itg2addnclem  24933  cntrset  25613  mslb1  25618  msra3  25620  fnckle  26056  pgapspf  26063  nn0prpwlem  26249  csbrn  26473  trirn  26474  isbnd2  26518  isbnd3  26519  heiborlem7  26552  rabren3dioph  26909  pellexlem2  26926  pellexlem5  26929  pell14qrgapw  26972  pellfundex  26982  rmspecsqrnq  27002  jm2.24nn  27057  jm2.17a  27058  jm2.17b  27059  jm2.17c  27060  acongrep  27078  acongeq  27081  jm2.22  27099  jm2.23  27100  jm2.20nn  27101  jm3.1lem2  27122  expdiophlem1  27125  matplusg  27480  lhe4.4ex1a  27557  stoweidlem5  27765  stoweidlem13  27773  stoweidlem14  27774  stoweidlem24  27784  stoweidlem26  27786  stoweidlem28  27788  stoweidlem49  27809  stoweidlem52  27812  stoweidlem62  27822  wallispilem3  27827  wallispilem4  27828  wallispilem5  27829  wallispi  27830  wallispi2lem1  27831  wallispi2lem2  27832  wallispi2  27833  stirlinglem1  27834  stirlinglem3  27836  stirlinglem5  27838  stirlinglem6  27839  stirlinglem7  27840  stirlinglem10  27843  stirlinglem11  27844  stirlinglem15  27848  stirlingr  27850  f1oun2prg  28087  usisuslgra  28124  usgraexvlem  28138  usgraexmpldifpr  28143  ene1  28269
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-i2m1 8807  ax-1ne0 8808  ax-rrecex 8811  ax-cnre 8812
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-2 9806
  Copyright terms: Public domain W3C validator