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

Theorem 2re 9831
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 9820 . 2  |-  2  =  ( 1  +  1 )
2 1re 8853 . . 3  |-  1  e.  RR
32, 2readdcli 8866 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2366 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1696  (class class class)co 5874   RRcr 8752   1c1 8754    + caddc 8756   2c2 9811
This theorem is referenced by:  2cn  9832  3re  9833  2ne0  9845  3pos  9846  2lt3  9903  1lt3  9904  2lt4  9906  1lt4  9907  2lt5  9910  2lt6  9915  1lt6  9916  2lt7  9921  1lt7  9922  2lt8  9928  1lt8  9929  2lt9  9936  1lt9  9937  2lt10  9945  1lt10  9946  halfgt0  9948  halflt1  9949  halfpm6th  9952  rehalfcl  9954  halfpos2  9957  halfnneg2  9959  addltmul  9963  nominpos  9964  avglt1  9965  avglt2  9966  nn0lele2xi  10032  halfnz  10106  2rp  10375  fzprval  10860  fztpval  10861  flhalf  10970  expubnd  11178  expmulnbnd  11249  nn0opthlem2  11300  faclbnd2  11320  faclbnd4lem1  11322  faclbnd5  11327  hashfun  11405  sqrlem7  11750  sqr4  11774  sqr2gt1lt2  11776  abstri  11830  rddif  11840  absrdbnd  11841  sqreulem  11859  amgm2  11869  abs3lemi  11909  caucvgrlem  12161  iseralt  12173  climcndslem1  12324  climcndslem2  12325  climcnds  12326  geoihalfsum  12354  efcllem  12375  ege2le3  12387  ef01bndlem  12480  cos01bnd  12482  cos2bnd  12484  cos01gt0  12487  sin02gt0  12488  sincos2sgn  12490  sin4lt0  12491  eirrlem  12498  egt2lt3  12500  epos  12501  sqr2re  12544  oexpneg  12606  bitsp1o  12640  bitsfzolem  12641  bitsfzo  12642  bitsmod  12643  bitsfi  12644  bitsinv1lem  12648  isprm3  12783  oddprm  12884  iserodd  12904  prmreclem2  12980  prmreclem6  12984  4sqlem11  13018  4sqlem12  13019  2expltfac  13121  oppgtset  14841  efgredleme  15068  mgpsca  15348  mgptset  15349  mgpds  15351  abvtrivd  15621  xmetge0  17925  bl2in  17973  metnrmlem3  18381  iihalf1  18445  iihalf2  18447  pcoass  18538  tchcphlem1  18681  minveclem2  18806  minveclem4  18812  pjthlem1  18817  ovolunlem1a  18871  dyadss  18965  opnmbllem  18972  vitalilem2  18980  vitalilem4  18982  mbfi1fseqlem5  19090  lhop1lem  19376  aaliou3lem1  19738  aaliou3lem2  19739  aaliou3lem3  19740  aaliou3lem8  19741  pilem2  19844  pilem3  19845  pipos  19849  sinhalfpilem  19850  sincosq1lem  19881  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  tangtx  19889  sinq12gt0  19891  sincos4thpi  19897  tan4thpi  19898  sincos6thpi  19899  sineq0  19905  cosordlem  19909  tanord1  19915  efif1olem1  19920  efif1olem2  19921  efif1olem4  19923  efif1o  19924  efifo  19925  logsqr  20067  cxpcn3lem  20103  root1id  20110  root1eq1  20111  root1cj  20112  cxpeq  20113  ang180lem1  20123  ang180lem2  20124  isosctrlem1  20134  chordthmlem2  20146  1cubrlem  20153  atancj  20222  atantan  20235  atanbndlem  20237  atans2  20243  leibpilem1  20252  leibpi  20254  log2tlbnd  20257  log2ublem2  20259  log2ub  20261  divsqrsumlem  20290  harmonicbnd3  20317  basellem1  20334  basellem2  20335  basellem3  20336  basellem5  20338  ppisval  20357  chtdif  20412  ppidif  20417  ppinncl  20428  chtrpcl  20429  ppieq0  20430  ppiltx  20431  ppiublem1  20457  ppiub  20459  chpeq0  20463  chteq0  20464  chtublem  20466  chtub  20467  chpval2  20473  chpub  20475  mersenne  20482  perfectlem1  20484  perfectlem2  20485  dchrptlem1  20519  dchrptlem2  20520  bcmono  20532  bclbnd  20535  bpos1lem  20537  bposlem1  20539  bposlem2  20540  bposlem3  20541  bposlem4  20542  bposlem5  20543  bposlem6  20544  bposlem7  20545  bposlem8  20546  bposlem9  20547  lgslem1  20551  lgsdirprm  20584  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgseisen  20608  lgsquadlem1  20609  lgsquadlem2  20610  m1lgs  20617  2sqlem11  20630  chebbnd1lem1  20634  chebbnd1lem2  20635  chebbnd1lem3  20636  chebbnd1  20637  chtppilimlem1  20638  chtppilimlem2  20639  chtppilim  20640  chto1ub  20641  chebbnd2  20642  chto1lb  20643  chpchtlim  20644  chpo1ub  20645  chpo1ubb  20646  rplogsumlem1  20649  rplogsumlem2  20650  dchrisumlem2  20655  dchrisumlem3  20656  dchrvmasumiflem1  20666  dchrisum0fno1  20676  dchrisum0re  20678  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2  20683  rplogsum  20692  mulog2sumlem1  20699  mulog2sumlem2  20700  log2sumbnd  20709  selberglem2  20711  selbergb  20714  selberg2b  20717  chpdifbndlem1  20718  logdivbnd  20721  selberg3lem1  20722  selberg3  20724  selberg4lem1  20725  selberg4  20726  pntrmax  20729  pntrsumbnd2  20732  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntrlog2bnd  20749  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntpbnd  20753  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemb  20762  pntlemg  20763  pntlemh  20764  pntlemr  20767  pntlemk  20771  pntlemo  20772  pnt2  20778  pnt  20779  ostth2lem1  20783  ostth3  20803  ex-pss  20831  ex-res  20844  ex-fv  20846  ex-fl  20850  nvge0  21256  ipidsq  21302  minvecolem2  21470  minvecolem4  21475  normlem7  21711  norm-ii-i  21732  norm3lem  21744  norm3lemt  21747  normpar2i  21751  bcsiALT  21774  pjhthlem1  21986  opsqrlem6  22741  cdj3lem1  23030  addltmulALT  23042  sqsscirc1  23307  rnlogblem  23416  coinfliplem  23694  coinflipspace  23696  zetacvg  23704  subfacp1lem1  23725  subfacp1lem5  23730  subfacval3  23735  umgrafi  23889  konigsberg  23926  circum  24022  4bc2eq6  24114  axlowdimlem3  24644  axlowdimlem4  24645  axlowdimlem6  24647  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  itg2addnclem  25003  cntrset  25705  mslb1  25710  msra3  25712  fnckle  26148  pgapspf  26155  nn0prpwlem  26341  csbrn  26565  trirn  26566  isbnd2  26610  isbnd3  26611  heiborlem7  26644  rabren3dioph  27001  pellexlem2  27018  pellexlem5  27021  pell14qrgapw  27064  pellfundex  27074  rmspecsqrnq  27094  jm2.24nn  27149  jm2.17a  27150  jm2.17b  27151  jm2.17c  27152  acongrep  27170  acongeq  27173  jm2.22  27191  jm2.23  27192  jm2.20nn  27193  jm3.1lem2  27214  expdiophlem1  27217  matplusg  27572  lhe4.4ex1a  27649  stoweidlem5  27857  stoweidlem13  27865  stoweidlem14  27866  stoweidlem24  27876  stoweidlem26  27878  stoweidlem28  27880  stoweidlem49  27901  stoweidlem52  27904  stoweidlem62  27914  wallispilem3  27919  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem10  27935  stirlinglem11  27936  stirlinglem15  27940  stirlingr  27942  f1oun2prg  28187  fzo0to42pr  28211  4fvwrd4  28220  usisuslgra  28247  usgraexvlem  28261  usgraexmpldifpr  28266  wlkntrllem3  28347  wlkntrllem4  28348  constr3lem4  28393  constr3trllem3  28398  constr3pthlem1  28401  constr3pthlem3  28403  ene1  28512
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-2 9820
  Copyright terms: Public domain W3C validator