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

Theorem 2timesd 10513
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 10386 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1687  e.wcel 1749  (class class class)co 6061   cc 9226   caddc 9231   cmul 9233  2c2 10317
This theorem is referenced by:  fzctr  11470  flhalf  11615  2submod  11701  modaddmodup  11703  expmulnbnd  11937  discr  11942  crre  12544  imval2  12581  abslem2  12768  sqreulem  12788  amgm2  12798  caucvgrlem  13091  iseraltlem2  13101  iseraltlem3  13102  arisum2  13263  efival  13376  sinadd  13388  cosadd  13389  addsin  13394  subsin  13395  cosmul  13397  addcos  13398  subcos  13399  sin2t  13401  cos2t  13402  eirrlem  13426  sadadd2lem2  13586  pythagtriplem12  13833  pythagtriplem15  13836  pythagtriplem17  13838  prmreclem6  13922  4sqlem11  13956  4sqlem12  13957  vdwlem3  13984  vdwlem8  13989  vdwlem9  13990  vdwlem10  13991  bl2in  19675  tchcphlem1  20450  nmparlem  20454  minveclem2  20613  minveclem4  20619  ovolunlem1  20680  uniioombllem5  20767  sineq0  21724  cosordlem  21728  tanarg  21809  heron  21974  dcubic1  21981  dquartlem1  21987  quart1lem  21991  sinasin  22025  asinsin  22028  cosasin  22040  efiatan2  22053  2efiatan  22054  atantan  22059  atantayl2  22074  leibpi  22078  log2cnv  22080  basellem5  22163  basellem6  22164  ppiub  22284  chtublem  22291  chtub  22292  bcctr  22355  pcbcctr  22356  bcmono  22357  bcmax  22358  bcp1ctr  22359  bposlem1  22364  bposlem2  22365  bposlem9  22372  lgsquadlem1  22434  chebbnd1lem2  22460  dchrisumlem2  22480  dchrisum0lem1b  22505  mulog2sumlem1  22524  logdivbnd  22546  selberg3lem1  22547  pntrsumbnd2  22557  selbergr  22558  selberg3r  22559  selberg34r  22561  pntpbnd1a  22575  pntpbnd2  22577  pntlemg  22588  pntlemr  22592  pntlemo  22597  ostth2lem1  22608  ostth3  22628  nvge0  23741  minvecolem2  23955  minvecolem4  23960  cdj3lem1  25517  sqsscirc1  26047  lgamgulmlem2  26719  lgamgulmlem3  26720  m1expevenALT  26810  fallrisefac  27230  mblfinlem3  28101  ftc1anclem7  28144  areacirclem1  28155  areacirc  28160  isbnd3  28354  pellfundex  28900  rmxluc  28950  rmyluc  28951  rmxdbl  28953  rmydbl  28954  jm2.24nn  28975  acongeq  28999  jm2.16nn0  29026  jm3.1lem1  29039  jm3.1lem2  29040  stirlinglem5  29547  2leaddle2  29849  sinhpcosh  30659  sineq0ALT  31251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-mulcl 9290  ax-mulcom 9292  ax-mulass 9294  ax-distr 9295  ax-1rid 9298  ax-cnre 9301
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-iota 5353  df-fv 5398  df-ov 6064  df-2 10326
  Copyright terms: Public domain W3C validator