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

Theorem 2re 9962
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 9951 . 2  |-  2  =  ( 1  +  1 )
2 1re 8984 . . 3  |-  1  e.  RR
32, 2readdcli 8997 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2436 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1715  (class class class)co 5981   RRcr 8883   1c1 8885    + caddc 8887   2c2 9942
This theorem is referenced by:  2cn  9963  3re  9964  2ne0  9976  3pos  9977  2lt3  10036  1lt3  10037  2lt4  10039  1lt4  10040  2lt5  10043  2lt6  10048  1lt6  10049  2lt7  10054  1lt7  10055  2lt8  10061  1lt8  10062  2lt9  10069  1lt9  10070  2lt10  10078  1lt10  10079  halfgt0  10081  halflt1  10082  halfpm6th  10085  rehalfcl  10087  halfpos2  10090  halfnneg2  10092  addltmul  10096  nominpos  10097  avglt1  10098  avglt2  10099  nn0lele2xi  10165  nn0n0n1ge2b  10174  halfnz  10241  2rp  10510  fzprval  10997  fztpval  10998  4fvwrd4  11011  fzo0to42pr  11073  flhalf  11118  expubnd  11327  expmulnbnd  11398  nn0opthlem2  11449  faclbnd2  11469  faclbnd4lem1  11471  faclbnd5  11476  hashfun  11587  f1oun2prg  11751  sqrlem7  11941  sqr4  11965  sqr2gt1lt2  11967  abstri  12021  rddif  12031  absrdbnd  12032  sqreulem  12050  amgm2  12060  abs3lemi  12100  caucvgrlem  12353  iseralt  12365  climcndslem1  12516  climcndslem2  12517  climcnds  12518  geoihalfsum  12546  efcllem  12567  ege2le3  12579  ef01bndlem  12672  cos01bnd  12674  cos2bnd  12676  cos01gt0  12679  sin02gt0  12680  sincos2sgn  12682  sin4lt0  12683  eirrlem  12690  egt2lt3  12692  epos  12693  sqr2re  12736  oexpneg  12798  bitsp1o  12832  bitsfzolem  12833  bitsfzo  12834  bitsmod  12835  bitsfi  12836  bitsinv1lem  12840  isprm3  12975  oddprm  13076  iserodd  13096  prmreclem2  13172  prmreclem6  13176  4sqlem11  13210  4sqlem12  13211  2expltfac  13313  oppgtset  15035  efgredleme  15262  mgpsca  15542  mgptset  15543  mgpds  15545  abvtrivd  15815  xmetge0  18122  bl2in  18170  metnrmlem3  18579  iihalf1  18644  iihalf2  18646  pcoass  18737  tchcphlem1  18880  minveclem2  19005  minveclem4  19011  pjthlem1  19016  ovolunlem1a  19070  dyadss  19164  opnmbllem  19171  vitalilem2  19179  vitalilem4  19181  mbfi1fseqlem5  19289  lhop1lem  19575  aaliou3lem1  19937  aaliou3lem2  19938  aaliou3lem3  19939  aaliou3lem8  19940  pilem2  20046  pilem3  20047  pipos  20051  sinhalfpilem  20052  sincosq1lem  20083  sincosq1sgn  20084  sincosq2sgn  20085  sincosq3sgn  20086  sincosq4sgn  20087  tangtx  20091  sinq12gt0  20093  sincos4thpi  20099  tan4thpi  20100  sincos6thpi  20101  sineq0  20107  cosordlem  20111  tanord1  20117  efif1olem1  20122  efif1olem2  20123  efif1olem4  20125  efif1o  20126  efifo  20127  logsqr  20273  cxpcn3lem  20309  root1id  20316  root1eq1  20317  root1cj  20318  cxpeq  20319  ang180lem1  20329  ang180lem2  20330  isosctrlem1  20340  chordthmlem2  20352  1cubrlem  20359  atancj  20428  atantan  20441  atanbndlem  20443  atans2  20449  leibpilem1  20458  leibpi  20460  log2tlbnd  20463  log2ublem2  20465  log2ub  20467  divsqrsumlem  20496  harmonicbnd3  20524  basellem1  20541  basellem2  20542  basellem3  20543  basellem5  20545  ppisval  20564  chtdif  20619  ppidif  20624  ppinncl  20635  chtrpcl  20636  ppieq0  20637  ppiltx  20638  ppiublem1  20664  ppiub  20666  chpeq0  20670  chteq0  20671  chtublem  20673  chtub  20674  chpval2  20680  chpub  20682  mersenne  20689  perfectlem1  20691  perfectlem2  20692  dchrptlem1  20726  dchrptlem2  20727  bcmono  20739  bclbnd  20742  bpos1lem  20744  bposlem1  20746  bposlem2  20747  bposlem3  20748  bposlem4  20749  bposlem5  20750  bposlem6  20751  bposlem7  20752  bposlem8  20753  bposlem9  20754  lgslem1  20758  lgsdirprm  20791  lgseisenlem1  20811  lgseisenlem2  20812  lgseisenlem3  20813  lgseisen  20815  lgsquadlem1  20816  lgsquadlem2  20817  m1lgs  20824  2sqlem11  20837  chebbnd1lem1  20841  chebbnd1lem2  20842  chebbnd1lem3  20843  chebbnd1  20844  chtppilimlem1  20845  chtppilimlem2  20846  chtppilim  20847  chto1ub  20848  chebbnd2  20849  chto1lb  20850  chpchtlim  20851  chpo1ub  20852  chpo1ubb  20853  rplogsumlem1  20856  rplogsumlem2  20857  dchrisumlem2  20862  dchrisumlem3  20863  dchrvmasumiflem1  20873  dchrisum0fno1  20883  dchrisum0re  20885  dchrisum0lem1b  20887  dchrisum0lem1  20888  dchrisum0lem2  20890  rplogsum  20899  mulog2sumlem1  20906  mulog2sumlem2  20907  log2sumbnd  20916  selberglem2  20918  selbergb  20921  selberg2b  20924  chpdifbndlem1  20925  logdivbnd  20928  selberg3lem1  20929  selberg3  20931  selberg4lem1  20932  selberg4  20933  pntrmax  20936  pntrsumbnd2  20939  selberg3r  20941  selberg4r  20942  selberg34r  20943  pntrlog2bndlem2  20950  pntrlog2bndlem3  20951  pntrlog2bndlem4  20952  pntrlog2bndlem5  20953  pntrlog2bndlem6  20955  pntrlog2bnd  20956  pntpbnd1a  20957  pntpbnd1  20958  pntpbnd2  20959  pntpbnd  20960  pntibndlem2  20963  pntibndlem3  20964  pntibnd  20965  pntlemb  20969  pntlemg  20970  pntlemh  20971  pntlemr  20974  pntlemk  20978  pntlemo  20979  pnt2  20985  pnt  20986  ostth2lem1  20990  ostth3  21010  umgrafi  21035  usisuslgra  21065  ex-pss  21126  ex-res  21139  ex-fv  21141  ex-fl  21145  nvge0  21553  ipidsq  21599  minvecolem2  21767  minvecolem4  21772  normlem7  22008  norm-ii-i  22029  norm3lem  22041  norm3lemt  22044  normpar2i  22048  bcsiALT  22071  pjhthlem1  22283  opsqrlem6  23038  cdj3lem1  23327  addltmulALT  23339  sqsscirc1  23661  rnlogblem  23864  dya2iocucvr  24097  coinfliplem  24184  coinflipspace  24186  zetacvg  24247  lgamgulmlem2  24262  lgamgulmlem3  24263  lgamgulmlem4  24264  lgamgulmlem6  24266  lgamucov  24270  subfacp1lem1  24313  subfacp1lem5  24318  subfacval3  24323  konigsberg  24498  circum  24594  4bc2eq6  24688  axlowdimlem3  25314  axlowdimlem4  25315  axlowdimlem6  25317  axlowdimlem16  25327  axlowdimlem17  25328  axlowdim  25331  itg2addnclem  25675  nn0prpwlem  25745  csbrn  25969  trirn  25970  isbnd2  26013  isbnd3  26014  heiborlem7  26047  rabren3dioph  26404  pellexlem2  26421  pellexlem5  26424  pell14qrgapw  26467  pellfundex  26477  rmspecsqrnq  26497  jm2.24nn  26552  jm2.17a  26553  jm2.17b  26554  jm2.17c  26555  acongrep  26573  acongeq  26576  jm2.22  26594  jm2.23  26595  jm2.20nn  26596  jm3.1lem2  26617  expdiophlem1  26620  matplusg  26975  lhe4.4ex1a  27052  stoweidlem5  27260  stoweidlem13  27268  stoweidlem14  27269  stoweidlem24  27279  stoweidlem26  27281  stoweidlem28  27283  stoweidlem49  27304  stoweidlem52  27307  stoweidlem62  27317  wallispilem3  27322  wallispilem4  27323  wallispilem5  27324  wallispi  27325  wallispi2lem1  27326  wallispi2lem2  27327  wallispi2  27328  stirlinglem1  27329  stirlinglem3  27331  stirlinglem5  27333  stirlinglem6  27334  stirlinglem7  27335  stirlinglem10  27338  stirlinglem11  27339  stirlinglem15  27343  stirlingr  27345  usgraexvlem  27579  usgraex2elv  27582  usgraexmpldifpr  27584  wlkntrllem3  27705  wlkntrllem4  27706  constr3lem4  27773  constr3trllem3  27778  constr3pthlem1  27781  constr3pthlem3  27783  vdgfrgragt2  27864  ene1  27960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-i2m1 8952  ax-1ne0 8953  ax-rrecex 8956  ax-cnre 8957
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984  df-2 9951
  Copyright terms: Public domain W3C validator