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

Theorem 2timesd 10806
Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
2timesd.1
Assertion
Ref Expression
2timesd

Proof of Theorem 2timesd
StepHypRef Expression
1 2timesd.1 . 2
2 2times 10679 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516   cmul 9518  2c2 10610
This theorem is referenced by:  fzctr  11816  flhalf  11962  2submod  12048  modaddmodup  12050  expmulnbnd  12298  discr  12303  crre  12947  imval2  12984  abslem2  13172  sqreulem  13192  amgm2  13202  caucvgrlem  13495  iseraltlem2  13505  iseraltlem3  13506  arisum2  13672  efival  13887  sinadd  13899  cosadd  13900  addsin  13905  subsin  13906  cosmul  13908  addcos  13909  subcos  13910  sin2t  13912  cos2t  13913  eirrlem  13937  sadadd2lem2  14100  pythagtriplem12  14350  pythagtriplem15  14353  pythagtriplem17  14355  prmreclem6  14439  4sqlem11  14473  4sqlem12  14474  vdwlem3  14501  vdwlem8  14506  vdwlem9  14507  vdwlem10  14508  bl2in  20903  tchcphlem1  21678  nmparlem  21682  minveclem2  21841  minveclem4  21847  ovolunlem1  21908  uniioombllem5  21996  sineq0  22914  cosordlem  22918  tanarg  23004  heron  23169  dcubic1  23176  dquartlem1  23182  quart1lem  23186  sinasin  23220  asinsin  23223  cosasin  23235  efiatan2  23248  2efiatan  23249  atantan  23254  atantayl2  23269  leibpi  23273  log2cnv  23275  basellem5  23358  basellem6  23359  ppiub  23479  chtublem  23486  chtub  23487  bcctr  23550  pcbcctr  23551  bcmono  23552  bcmax  23553  bcp1ctr  23554  bposlem1  23559  bposlem2  23560  bposlem9  23567  lgsquadlem1  23629  chebbnd1lem2  23655  dchrisumlem2  23675  dchrisum0lem1b  23700  mulog2sumlem1  23719  logdivbnd  23741  selberg3lem1  23742  pntrsumbnd2  23752  selbergr  23753  selberg3r  23754  selberg34r  23756  pntpbnd1a  23770  pntpbnd2  23772  pntlemg  23783  pntlemr  23787  pntlemo  23792  ostth2lem1  23803  ostth3  23823  nvge0  25577  minvecolem2  25791  minvecolem4  25796  cdj3lem1  27353  sqsscirc1  27890  lgamgulmlem2  28572  lgamgulmlem3  28573  m1expevenALT  28663  fallrisefac  29147  mblfinlem3  30053  ftc1anclem7  30096  areacirclem1  30107  areacirc  30112  isbnd3  30280  pellfundex  30822  rmxluc  30872  rmyluc  30873  rmxdbl  30875  rmydbl  30876  jm2.24nn  30897  acongeq  30921  jm2.16nn0  30946  jm3.1lem1  30959  jm3.1lem2  30960  lt2addmuld  31473  sinmulcos  31665  stirlinglem5  31860  fourierdlem79  31968  fouriercnp  32009  2leaddle2  32320  sinhpcosh  33134  sineq0ALT  33737  imo72b2lem0  37982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-mulcom 9577  ax-mulass 9579  ax-distr 9580  ax-1rid 9583  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-2 10619
  Copyright terms: Public domain W3C validator