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

Theorem 2timesd 10705
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 10578 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  e.wcel 1758  (class class class)co 6222   cc 9417   caddc 9422   cmul 9424  2c2 10509
This theorem is referenced by:  fzctr  11674  flhalf  11819  2submod  11905  modaddmodup  11907  expmulnbnd  12153  discr  12158  crre  12761  imval2  12798  abslem2  12985  sqreulem  13005  amgm2  13015  caucvgrlem  13308  iseraltlem2  13318  iseraltlem3  13319  arisum2  13481  efival  13594  sinadd  13606  cosadd  13607  addsin  13612  subsin  13613  cosmul  13615  addcos  13616  subcos  13617  sin2t  13619  cos2t  13620  eirrlem  13644  sadadd2lem2  13804  pythagtriplem12  14051  pythagtriplem15  14054  pythagtriplem17  14056  prmreclem6  14140  4sqlem11  14174  4sqlem12  14175  vdwlem3  14202  vdwlem8  14207  vdwlem9  14208  vdwlem10  14209  bl2in  20374  tchcphlem1  21149  nmparlem  21153  minveclem2  21312  minveclem4  21318  ovolunlem1  21379  uniioombllem5  21467  sineq0  22383  cosordlem  22387  tanarg  22468  heron  22633  dcubic1  22640  dquartlem1  22646  quart1lem  22650  sinasin  22684  asinsin  22687  cosasin  22699  efiatan2  22712  2efiatan  22713  atantan  22718  atantayl2  22733  leibpi  22737  log2cnv  22739  basellem5  22822  basellem6  22823  ppiub  22943  chtublem  22950  chtub  22951  bcctr  23014  pcbcctr  23015  bcmono  23016  bcmax  23017  bcp1ctr  23018  bposlem1  23023  bposlem2  23024  bposlem9  23031  lgsquadlem1  23093  chebbnd1lem2  23119  dchrisumlem2  23139  dchrisum0lem1b  23164  mulog2sumlem1  23183  logdivbnd  23205  selberg3lem1  23206  pntrsumbnd2  23216  selbergr  23217  selberg3r  23218  selberg34r  23220  pntpbnd1a  23234  pntpbnd2  23236  pntlemg  23247  pntlemr  23251  pntlemo  23256  ostth2lem1  23267  ostth3  23287  nvge0  24531  minvecolem2  24745  minvecolem4  24750  cdj3lem1  26307  sqsscirc1  26795  lgamgulmlem2  27472  lgamgulmlem3  27473  m1expevenALT  27563  fallrisefac  27984  mblfinlem3  28890  ftc1anclem7  28933  areacirclem1  28944  areacirc  28949  isbnd3  29143  pellfundex  29687  rmxluc  29737  rmyluc  29738  rmxdbl  29740  rmydbl  29741  jm2.24nn  29762  acongeq  29786  jm2.16nn0  29813  jm3.1lem1  29826  jm3.1lem2  29827  lt2addmuld  30279  sinmulcos  30430  stirlinglem5  30607  fourierdlem79  30715  fouriercnp  30756  2leaddle2  31052  sinhpcosh  31914  sineq0ALT  32516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-resscn 9476  ax-1cn 9477  ax-icn 9478  ax-addcl 9479  ax-mulcl 9481  ax-mulcom 9483  ax-mulass 9485  ax-distr 9486  ax-1rid 9489  ax-cnre 9492
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-iota 5500  df-fv 5545  df-ov 6225  df-2 10518
  Copyright terms: Public domain W3C validator