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

Theorem 2re 9769
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 9758 . 2  |-  2  =  ( 1  +  1 )
2 1re 8791 . . 3  |-  1  e.  RR
32, 2readdcli 8804 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2326 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1621  (class class class)co 5778   RRcr 8690   1c1 8692    + caddc 8694   2c2 9749
This theorem is referenced by:  2cn  9770  3re  9771  2ne0  9783  3pos  9784  2lt3  9840  1lt3  9841  2lt4  9843  1lt4  9844  2lt5  9847  2lt6  9852  1lt6  9853  2lt7  9858  1lt7  9859  2lt8  9865  1lt8  9866  2lt9  9873  1lt9  9874  2lt10  9882  1lt10  9883  halfgt0  9885  halflt1  9886  halfpm6th  9889  rehalfcl  9891  halfpos2  9894  halfnneg2  9896  addltmul  9900  nominpos  9901  avglt1  9902  avglt2  9903  nn0lele2xi  9969  halfnz  10043  2rp  10312  fzprval  10796  fztpval  10797  flhalf  10906  expubnd  11114  expmulnbnd  11185  nn0opthlem2  11236  faclbnd2  11256  faclbnd4lem1  11258  faclbnd5  11263  hashfun  11340  sqrlem7  11685  sqr4  11709  sqr2gt1lt2  11711  abstri  11765  rddif  11775  absrdbnd  11776  sqreulem  11794  amgm2  11804  abs3lemi  11844  caucvgrlem  12096  iseralt  12108  climcndslem1  12256  climcndslem2  12257  climcnds  12258  geoihalfsum  12286  efcllem  12307  ege2le3  12319  ef01bndlem  12412  cos01bnd  12414  cos2bnd  12416  cos01gt0  12419  sin02gt0  12420  sincos2sgn  12422  sin4lt0  12423  eirrlem  12430  egt2lt3  12432  epos  12433  sqr2re  12476  oexpneg  12538  bitsp1o  12572  bitsfzolem  12573  bitsfzo  12574  bitsmod  12575  bitsfi  12576  bitsinv1lem  12580  isprm3  12715  oddprm  12816  iserodd  12836  prmreclem2  12912  prmreclem6  12916  4sqlem11  12950  4sqlem12  12951  2expltfac  13053  oppgtset  14773  efgredleme  15000  mgpsca  15280  mgptset  15281  mgpds  15283  abvtrivd  15553  xmetge0  17857  bl2in  17905  metnrmlem3  18313  iihalf1  18377  iihalf2  18379  pcoass  18470  tchcphlem1  18613  minveclem2  18738  minveclem4  18744  pjthlem1  18749  ovolunlem1a  18803  dyadss  18897  opnmbllem  18904  vitalilem2  18912  vitalilem4  18914  mbfi1fseqlem5  19022  lhop1lem  19308  aaliou3lem1  19670  aaliou3lem2  19671  aaliou3lem3  19672  aaliou3lem8  19673  pilem2  19776  pilem3  19777  pipos  19781  sinhalfpilem  19782  sincosq1lem  19813  sincosq1sgn  19814  sincosq2sgn  19815  sincosq3sgn  19816  sincosq4sgn  19817  tangtx  19821  sinq12gt0  19823  sincos4thpi  19829  tan4thpi  19830  sincos6thpi  19831  sineq0  19837  cosordlem  19841  tanord1  19847  efif1olem1  19852  efif1olem2  19853  efif1olem4  19855  efif1o  19856  efifo  19857  logsqr  19999  cxpcn3lem  20035  root1id  20042  root1eq1  20043  root1cj  20044  cxpeq  20045  ang180lem1  20055  ang180lem2  20056  isosctrlem1  20066  chordthmlem2  20078  1cubrlem  20085  atancj  20154  atantan  20167  atanbndlem  20169  atans2  20175  leibpilem1  20184  leibpi  20186  log2tlbnd  20189  log2ublem2  20191  log2ub  20193  divsqrsumlem  20222  harmonicbnd3  20249  basellem1  20266  basellem2  20267  basellem3  20268  basellem5  20270  ppisval  20289  chtdif  20344  ppidif  20349  ppinncl  20360  chtrpcl  20361  ppieq0  20362  ppiltx  20363  ppiublem1  20389  ppiub  20391  chpeq0  20395  chteq0  20396  chtublem  20398  chtub  20399  chpval2  20405  chpub  20407  mersenne  20414  perfectlem1  20416  perfectlem2  20417  dchrptlem1  20451  dchrptlem2  20452  bcmono  20464  bclbnd  20467  bpos1lem  20469  bposlem1  20471  bposlem2  20472  bposlem3  20473  bposlem4  20474  bposlem5  20475  bposlem6  20476  bposlem7  20477  bposlem8  20478  bposlem9  20479  lgslem1  20483  lgsdirprm  20516  lgseisenlem1  20536  lgseisenlem2  20537  lgseisenlem3  20538  lgseisen  20540  lgsquadlem1  20541  lgsquadlem2  20542  m1lgs  20549  2sqlem11  20562  chebbnd1lem1  20566  chebbnd1lem2  20567  chebbnd1lem3  20568  chebbnd1  20569  chtppilimlem1  20570  chtppilimlem2  20571  chtppilim  20572  chto1ub  20573  chebbnd2  20574  chto1lb  20575  chpchtlim  20576  chpo1ub  20577  chpo1ubb  20578  rplogsumlem1  20581  rplogsumlem2  20582  dchrisumlem2  20587  dchrisumlem3  20588  dchrvmasumiflem1  20598  dchrisum0fno1  20608  dchrisum0re  20610  dchrisum0lem1b  20612  dchrisum0lem1  20613  dchrisum0lem2  20615  rplogsum  20624  mulog2sumlem1  20631  mulog2sumlem2  20632  log2sumbnd  20641  selberglem2  20643  selbergb  20646  selberg2b  20649  chpdifbndlem1  20650  logdivbnd  20653  selberg3lem1  20654  selberg3  20656  selberg4lem1  20657  selberg4  20658  pntrmax  20661  pntrsumbnd2  20664  selberg3r  20666  selberg4r  20667  selberg34r  20668  pntrlog2bndlem2  20675  pntrlog2bndlem3  20676  pntrlog2bndlem4  20677  pntrlog2bndlem5  20678  pntrlog2bndlem6  20680  pntrlog2bnd  20681  pntpbnd1a  20682  pntpbnd1  20683  pntpbnd2  20684  pntpbnd  20685  pntibndlem2  20688  pntibndlem3  20689  pntibnd  20690  pntlemb  20694  pntlemg  20695  pntlemh  20696  pntlemr  20699  pntlemk  20703  pntlemo  20704  pnt2  20710  pnt  20711  ostth2lem1  20715  ostth3  20735  ex-pss  20744  ex-res  20757  ex-fv  20759  ex-fl  20763  nvge0  21186  ipidsq  21232  minvecolem2  21400  minvecolem4  21405  normlem7  21641  norm-ii-i  21662  norm3lem  21674  norm3lemt  21677  normpar2i  21681  bcsiALT  21704  pjhthlem1  21916  opsqrlem6  22671  cdj3lem1  22960  addltmulALT  22972  zetacvg  23047  subfacp1lem1  23068  subfacp1lem5  23073  subfacval3  23078  umgrafi  23232  konigsberg  23269  circum  23365  4bc2eq6  23456  axlowdimlem3  23933  axlowdimlem4  23934  axlowdimlem6  23936  axlowdimlem16  23946  axlowdimlem17  23947  axlowdim  23950  cntrset  24955  mslb1  24960  msra3  24962  fnckle  25398  pgapspf  25405  nn0prpwlem  25591  csbrn  25815  trirn  25816  isbnd2  25860  isbnd3  25861  heiborlem7  25894  rabren3dioph  26251  pellexlem2  26268  pellexlem5  26271  pell14qrgapw  26314  pellfundex  26324  rmspecsqrnq  26344  jm2.24nn  26399  jm2.17a  26400  jm2.17b  26401  jm2.17c  26402  acongrep  26420  acongeq  26423  jm2.22  26441  jm2.23  26442  jm2.20nn  26443  jm3.1lem2  26464  expdiophlem1  26467  matplusg  26822  lhe4.4ex1a  26899  stoweidlem5  27075  stoweidlem13  27083  stoweidlem14  27084  stoweidlem24  27094  stoweidlem26  27096  stoweidlem28  27098  stoweidlem49  27119  stoweidlem52  27122  stoweidlem62  27132
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-addrcl 8752  ax-mulcl 8753  ax-mulrcl 8754  ax-i2m1 8759  ax-1ne0 8760  ax-rrecex 8763  ax-cnre 8764
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-xp 4661  df-cnv 4663  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fv 4675  df-ov 5781  df-2 9758
  Copyright terms: Public domain W3C validator