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

Theorem 2re 10001
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 9990 . 2  |-  2  =  ( 1  +  1 )
2 1re 9023 . . 3  |-  1  e.  RR
32, 2readdcli 9036 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2457 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1717  (class class class)co 6020   RRcr 8922   1c1 8924    + caddc 8926   2c2 9981
This theorem is referenced by:  2cn  10002  3re  10003  2ne0  10015  3pos  10016  2lt3  10075  1lt3  10076  2lt4  10078  1lt4  10079  2lt5  10082  2lt6  10087  1lt6  10088  2lt7  10093  1lt7  10094  2lt8  10100  1lt8  10101  2lt9  10108  1lt9  10109  2lt10  10117  1lt10  10118  halfgt0  10120  halflt1  10121  halfpm6th  10124  rehalfcl  10126  halfpos2  10129  halfnneg2  10131  addltmul  10135  nominpos  10136  avglt1  10137  avglt2  10138  nn0lele2xi  10204  nn0n0n1ge2b  10213  halfnz  10280  2rp  10549  fzprval  11037  fztpval  11038  4fvwrd4  11051  fzo0to42pr  11113  flhalf  11158  expubnd  11367  expmulnbnd  11438  nn0opthlem2  11489  faclbnd2  11509  faclbnd4lem1  11511  faclbnd5  11516  hashfun  11627  f1oun2prg  11791  sqrlem7  11981  sqr4  12005  sqr2gt1lt2  12007  abstri  12061  rddif  12071  absrdbnd  12072  sqreulem  12090  amgm2  12100  caucvgrlem  12393  iseralt  12405  climcndslem1  12556  climcndslem2  12557  climcnds  12558  geoihalfsum  12586  efcllem  12607  ege2le3  12619  ef01bndlem  12712  cos01bnd  12714  cos2bnd  12716  cos01gt0  12719  sin02gt0  12720  sincos2sgn  12722  sin4lt0  12723  eirrlem  12730  egt2lt3  12732  epos  12733  sqr2re  12776  oexpneg  12838  bitsp1o  12872  bitsfzolem  12873  bitsfzo  12874  bitsmod  12875  bitsfi  12876  bitsinv1lem  12880  isprm3  13015  oddprm  13116  iserodd  13136  prmreclem2  13212  prmreclem6  13216  4sqlem11  13250  4sqlem12  13251  2expltfac  13353  oppgtset  15075  efgredleme  15302  mgpsca  15582  mgptset  15583  mgpds  15585  abvtrivd  15855  xmetge0  18283  bl2in  18331  metnrmlem3  18762  iihalf1  18827  iihalf2  18829  pcoass  18920  tchcphlem1  19063  minveclem2  19194  minveclem4  19200  pjthlem1  19205  ovolunlem1a  19259  dyadss  19353  opnmbllem  19360  vitalilem2  19368  vitalilem4  19370  mbfi1fseqlem5  19478  lhop1lem  19764  aaliou3lem1  20126  aaliou3lem2  20127  aaliou3lem3  20128  aaliou3lem8  20129  pilem2  20235  pilem3  20236  pipos  20240  sinhalfpilem  20241  sincosq1lem  20272  sincosq4sgn  20276  tangtx  20280  sinq12gt0  20282  sincos4thpi  20288  tan4thpi  20289  sincos6thpi  20290  sineq0  20296  cosordlem  20300  tanord1  20306  efif1olem1  20311  efif1olem2  20312  efif1olem4  20314  efif1o  20315  efifo  20316  logsqr  20462  cxpcn3lem  20498  root1id  20505  root1eq1  20506  root1cj  20507  cxpeq  20508  ang180lem1  20518  ang180lem2  20519  chordthmlem2  20541  1cubrlem  20548  atancj  20617  atantan  20630  atanbndlem  20632  atans2  20638  leibpilem1  20647  leibpi  20649  log2tlbnd  20652  log2ublem2  20654  log2ub  20656  divsqrsumlem  20685  harmonicbnd3  20713  basellem1  20730  basellem2  20731  basellem3  20732  basellem5  20734  ppisval  20753  chtdif  20808  ppidif  20813  ppinncl  20824  chtrpcl  20825  ppieq0  20826  ppiltx  20827  ppiublem1  20853  ppiub  20855  chpeq0  20859  chteq0  20860  chtublem  20862  chtub  20863  chpval2  20869  chpub  20871  mersenne  20878  perfectlem1  20880  perfectlem2  20881  dchrptlem1  20915  dchrptlem2  20916  bcmono  20928  bclbnd  20931  bpos1lem  20933  bposlem1  20935  bposlem2  20936  bposlem3  20937  bposlem4  20938  bposlem5  20939  bposlem6  20940  bposlem7  20941  bposlem8  20942  bposlem9  20943  lgslem1  20947  lgsdirprm  20980  lgseisenlem1  21000  lgseisenlem2  21001  lgseisenlem3  21002  lgseisen  21004  lgsquadlem1  21005  lgsquadlem2  21006  m1lgs  21013  2sqlem11  21026  chebbnd1lem1  21030  chebbnd1lem2  21031  chebbnd1lem3  21032  chebbnd1  21033  chtppilimlem1  21034  chtppilimlem2  21035  chtppilim  21036  chto1ub  21037  chebbnd2  21038  chto1lb  21039  chpchtlim  21040  chpo1ub  21041  chpo1ubb  21042  rplogsumlem1  21045  rplogsumlem2  21046  dchrisumlem2  21051  dchrisumlem3  21052  dchrvmasumiflem1  21062  dchrisum0fno1  21072  dchrisum0re  21074  dchrisum0lem1b  21076  dchrisum0lem1  21077  dchrisum0lem2  21079  rplogsum  21088  mulog2sumlem1  21095  mulog2sumlem2  21096  log2sumbnd  21105  selberglem2  21107  selbergb  21110  selberg2b  21113  chpdifbndlem1  21114  logdivbnd  21117  selberg3lem1  21118  selberg3  21120  selberg4lem1  21121  selberg4  21122  pntrmax  21125  pntrsumbnd2  21128  selberg3r  21130  selberg4r  21131  selberg34r  21132  pntrlog2bndlem2  21139  pntrlog2bndlem3  21140  pntrlog2bndlem4  21141  pntrlog2bndlem5  21142  pntrlog2bndlem6  21144  pntrlog2bnd  21145  pntpbnd1a  21146  pntpbnd1  21147  pntpbnd2  21148  pntpbnd  21149  pntibndlem2  21152  pntibndlem3  21153  pntibnd  21154  pntlemb  21158  pntlemg  21159  pntlemh  21160  pntlemr  21163  pntlemk  21167  pntlemo  21168  pnt2  21174  pnt  21175  ostth2lem1  21179  ostth3  21199  umgrafi  21224  usisuslgra  21254  usgraexvlem  21280  usgraex2elv  21283  usgraexmpldifpr  21285  wlkntrllem3  21415  wlkntrllem4  21416  constr3lem4  21482  constr3trllem3  21487  constr3pthlem1  21490  constr3pthlem3  21492  konigsberg  21557  ex-pss  21584  ex-res  21597  ex-fv  21599  ex-fl  21603  nvge0  22011  ipidsq  22057  minvecolem2  22225  minvecolem4  22230  normlem7  22466  norm-ii-i  22487  norm3lemt  22502  normpar2i  22506  bcsiALT  22529  pjhthlem1  22741  opsqrlem6  23496  cdj3lem1  23785  addltmulALT  23797  sqsscirc1  24110  rnlogblem  24195  dya2iocucvr  24428  coinfliplem  24515  coinflipspace  24517  ballotlem2  24525  zetacvg  24578  lgamgulmlem2  24593  lgamgulmlem3  24594  lgamgulmlem4  24595  lgamgulmlem6  24597  lgamucov  24601  subfacp1lem1  24644  subfacp1lem5  24649  subfacval3  24654  circum  24890  4bc2eq6  24983  axlowdimlem3  25597  axlowdimlem4  25598  axlowdimlem6  25600  axlowdimlem16  25610  axlowdimlem17  25611  axlowdim  25614  itg2addnclem  25957  nn0prpwlem  26016  csbrn  26147  trirn  26148  isbnd2  26183  isbnd3  26184  heiborlem7  26217  rabren3dioph  26567  pellexlem2  26584  pellexlem5  26587  pell14qrgapw  26630  pellfundex  26640  rmspecsqrnq  26660  jm2.24nn  26715  jm2.17a  26716  jm2.17b  26717  jm2.17c  26718  acongrep  26736  acongeq  26739  jm2.22  26757  jm2.23  26758  jm2.20nn  26759  jm3.1lem2  26780  expdiophlem1  26783  matplusg  27138  lhe4.4ex1a  27215  stoweidlem13  27430  stoweidlem14  27431  stoweidlem26  27443  stoweidlem49  27466  stoweidlem52  27469  wallispilem4  27485  wallispilem5  27486  wallispi  27487  wallispi2lem1  27488  wallispi2lem2  27489  wallispi2  27490  stirlinglem1  27491  stirlinglem3  27493  stirlinglem5  27495  stirlinglem6  27496  stirlinglem7  27497  stirlinglem10  27500  stirlinglem11  27501  stirlinglem15  27505  stirlingr  27507  vdgfrgragt2  27781  ene1  27877
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-i2m1 8991  ax-1ne0 8992  ax-rrecex 8995  ax-cnre 8996
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-2 9990
  Copyright terms: Public domain W3C validator