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

Theorem 2re 9815
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 9804 . 2  |-  2  =  ( 1  +  1 )
2 1re 8837 . . 3  |-  1  e.  RR
32, 2readdcli 8850 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2353 1  |-  2  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
This theorem is referenced by:  2cn  9816  3re  9817  2ne0  9829  3pos  9830  2lt3  9887  1lt3  9888  2lt4  9890  1lt4  9891  2lt5  9894  2lt6  9899  1lt6  9900  2lt7  9905  1lt7  9906  2lt8  9912  1lt8  9913  2lt9  9920  1lt9  9921  2lt10  9929  1lt10  9930  halfgt0  9932  halflt1  9933  halfpm6th  9936  rehalfcl  9938  halfpos2  9941  halfnneg2  9943  addltmul  9947  nominpos  9948  avglt1  9949  avglt2  9950  nn0lele2xi  10016  halfnz  10090  2rp  10359  fzprval  10844  fztpval  10845  flhalf  10954  expubnd  11162  expmulnbnd  11233  nn0opthlem2  11284  faclbnd2  11304  faclbnd4lem1  11306  faclbnd5  11311  hashfun  11389  sqrlem7  11734  sqr4  11758  sqr2gt1lt2  11760  abstri  11814  rddif  11824  absrdbnd  11825  sqreulem  11843  amgm2  11853  abs3lemi  11893  caucvgrlem  12145  iseralt  12157  climcndslem1  12308  climcndslem2  12309  climcnds  12310  geoihalfsum  12338  efcllem  12359  ege2le3  12371  ef01bndlem  12464  cos01bnd  12466  cos2bnd  12468  cos01gt0  12471  sin02gt0  12472  sincos2sgn  12474  sin4lt0  12475  eirrlem  12482  egt2lt3  12484  epos  12485  sqr2re  12528  oexpneg  12590  bitsp1o  12624  bitsfzolem  12625  bitsfzo  12626  bitsmod  12627  bitsfi  12628  bitsinv1lem  12632  isprm3  12767  oddprm  12868  iserodd  12888  prmreclem2  12964  prmreclem6  12968  4sqlem11  13002  4sqlem12  13003  2expltfac  13105  oppgtset  14825  efgredleme  15052  mgpsca  15332  mgptset  15333  mgpds  15335  abvtrivd  15605  xmetge0  17909  bl2in  17957  metnrmlem3  18365  iihalf1  18429  iihalf2  18431  pcoass  18522  tchcphlem1  18665  minveclem2  18790  minveclem4  18796  pjthlem1  18801  ovolunlem1a  18855  dyadss  18949  opnmbllem  18956  vitalilem2  18964  vitalilem4  18966  mbfi1fseqlem5  19074  lhop1lem  19360  aaliou3lem1  19722  aaliou3lem2  19723  aaliou3lem3  19724  aaliou3lem8  19725  pilem2  19828  pilem3  19829  pipos  19833  sinhalfpilem  19834  sincosq1lem  19865  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  tangtx  19873  sinq12gt0  19875  sincos4thpi  19881  tan4thpi  19882  sincos6thpi  19883  sineq0  19889  cosordlem  19893  tanord1  19899  efif1olem1  19904  efif1olem2  19905  efif1olem4  19907  efif1o  19908  efifo  19909  logsqr  20051  cxpcn3lem  20087  root1id  20094  root1eq1  20095  root1cj  20096  cxpeq  20097  ang180lem1  20107  ang180lem2  20108  isosctrlem1  20118  chordthmlem2  20130  1cubrlem  20137  atancj  20206  atantan  20219  atanbndlem  20221  atans2  20227  leibpilem1  20236  leibpi  20238  log2tlbnd  20241  log2ublem2  20243  log2ub  20245  divsqrsumlem  20274  harmonicbnd3  20301  basellem1  20318  basellem2  20319  basellem3  20320  basellem5  20322  ppisval  20341  chtdif  20396  ppidif  20401  ppinncl  20412  chtrpcl  20413  ppieq0  20414  ppiltx  20415  ppiublem1  20441  ppiub  20443  chpeq0  20447  chteq0  20448  chtublem  20450  chtub  20451  chpval2  20457  chpub  20459  mersenne  20466  perfectlem1  20468  perfectlem2  20469  dchrptlem1  20503  dchrptlem2  20504  bcmono  20516  bclbnd  20519  bpos1lem  20521  bposlem1  20523  bposlem2  20524  bposlem3  20525  bposlem4  20526  bposlem5  20527  bposlem6  20528  bposlem7  20529  bposlem8  20530  bposlem9  20531  lgslem1  20535  lgsdirprm  20568  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  m1lgs  20601  2sqlem11  20614  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1lem3  20620  chebbnd1  20621  chtppilimlem1  20622  chtppilimlem2  20623  chtppilim  20624  chto1ub  20625  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  chpo1ub  20629  chpo1ubb  20630  rplogsumlem1  20633  rplogsumlem2  20634  dchrisumlem2  20639  dchrisumlem3  20640  dchrvmasumiflem1  20650  dchrisum0fno1  20660  dchrisum0re  20662  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2  20667  rplogsum  20676  mulog2sumlem1  20683  mulog2sumlem2  20684  log2sumbnd  20693  selberglem2  20695  selbergb  20698  selberg2b  20701  chpdifbndlem1  20702  logdivbnd  20705  selberg3lem1  20706  selberg3  20708  selberg4lem1  20709  selberg4  20710  pntrmax  20713  pntrsumbnd2  20716  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntpbnd  20737  pntibndlem2  20740  pntibndlem3  20741  pntibnd  20742  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemr  20751  pntlemk  20755  pntlemo  20756  pnt2  20762  pnt  20763  ostth2lem1  20767  ostth3  20787  ex-pss  20815  ex-res  20828  ex-fv  20830  ex-fl  20834  nvge0  21240  ipidsq  21286  minvecolem2  21454  minvecolem4  21459  normlem7  21695  norm-ii-i  21716  norm3lem  21728  norm3lemt  21731  normpar2i  21735  bcsiALT  21758  pjhthlem1  21970  opsqrlem6  22725  cdj3lem1  23014  addltmulALT  23026  sqsscirc1  23292  rnlogblem  23401  coinfliplem  23679  coinflipspace  23681  zetacvg  23689  subfacp1lem1  23710  subfacp1lem5  23715  subfacval3  23720  umgrafi  23874  konigsberg  23911  circum  24007  4bc2eq6  24099  axlowdimlem3  24572  axlowdimlem4  24573  axlowdimlem6  24575  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  cntrset  25602  mslb1  25607  msra3  25609  fnckle  26045  pgapspf  26052  nn0prpwlem  26238  csbrn  26462  trirn  26463  isbnd2  26507  isbnd3  26508  heiborlem7  26541  rabren3dioph  26898  pellexlem2  26915  pellexlem5  26918  pell14qrgapw  26961  pellfundex  26971  rmspecsqrnq  26991  jm2.24nn  27046  jm2.17a  27047  jm2.17b  27048  jm2.17c  27049  acongrep  27067  acongeq  27070  jm2.22  27088  jm2.23  27089  jm2.20nn  27090  jm3.1lem2  27111  expdiophlem1  27114  matplusg  27469  lhe4.4ex1a  27546  stoweidlem5  27754  stoweidlem13  27762  stoweidlem14  27763  stoweidlem24  27773  stoweidlem26  27775  stoweidlem28  27777  stoweidlem49  27798  stoweidlem52  27801  stoweidlem62  27811  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem11  27833  stirlinglem15  27837  stirlingr  27839  f1oun2prg  28076  usisuslgra  28113  usgraexvlem  28127  usgraexmpldifpr  28132
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
  Copyright terms: Public domain W3C validator