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

Theorem 2timesd 12397
Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
2timesd.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
Assertion
Ref Expression
2timesd (๐œ‘ โ†’ (2 ยท ๐ด) = (๐ด + ๐ด))

Proof of Theorem 2timesd
StepHypRef Expression
1 2timesd.1 . 2 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
2 2times 12290 . 2 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ๐ด) = (๐ด + ๐ด))
31, 2syl 17 1 (๐œ‘ โ†’ (2 ยท ๐ด) = (๐ด + ๐ด))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7358  โ„‚cc 11050   + caddc 11055   ยท cmul 11057  2c2 12209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-mulcl 11114  ax-mulcom 11116  ax-mulass 11118  ax-distr 11119  ax-1rid 11122  ax-cnre 11125
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-2 12217
This theorem is referenced by:  lt2addmuld  12404  fzctr  13554  flhalf  13736  2submod  13838  modaddmodup  13840  m1expeven  14016  expmulnbnd  14139  discr  14144  crre  15000  imval2  15037  abslem2  15225  sqreulem  15245  amgm2  15255  caucvgrlem  15558  iseraltlem2  15568  iseraltlem3  15569  arisum2  15747  fallrisefac  15909  efival  16035  sinadd  16047  cosadd  16048  addsin  16053  subsin  16054  cosmul  16056  addcos  16057  subcos  16058  sin2t  16060  cos2t  16061  eirrlem  16087  sadadd2lem2  16331  pythagtriplem12  16699  pythagtriplem15  16702  pythagtriplem17  16704  difsqpwdvds  16760  prmreclem6  16794  4sqlem11  16828  4sqlem12  16829  vdwlem3  16856  vdwlem8  16861  vdwlem9  16862  vdwlem10  16863  bl2in  23756  tcphcphlem1  24602  nmparlem  24606  cphipval2  24608  minveclem2  24793  minveclem4  24799  ovolunlem1  24864  uniioombllem5  24954  sineq0  25883  cosordlem  25889  tanarg  25977  heron  26191  dcubic1  26198  dquartlem1  26204  quart1lem  26208  sinasin  26242  asinsin  26245  cosasin  26257  efiatan2  26270  2efiatan  26271  atantan  26276  atantayl2  26291  leibpi  26295  log2cnv  26297  lgamgulmlem2  26382  lgamgulmlem3  26383  basellem5  26437  basellem6  26438  ppiub  26555  chtublem  26562  chtub  26563  bcctr  26626  pcbcctr  26627  bcmono  26628  bcmax  26629  bcp1ctr  26630  bposlem1  26635  bposlem2  26636  bposlem9  26643  gausslemma2d  26725  lgsquadlem1  26731  chebbnd1lem2  26821  dchrisumlem2  26841  dchrisum0lem1b  26866  mulog2sumlem1  26885  logdivbnd  26907  selberg3lem1  26908  pntrsumbnd2  26918  selbergr  26919  selberg3r  26920  selberg34r  26922  pntpbnd1a  26936  pntpbnd2  26938  pntlemg  26949  pntlemr  26953  pntlemo  26958  ostth2lem1  26969  ostth3  26989  finsumvtxdg2ssteplem4  28499  nvge0  29618  minvecolem2  29820  minvecolem4  29825  cdj3lem1  31379  sqsscirc1  32492  bcprod  34314  unbdqndv2lem1  34975  irrdifflemf  35799  mblfinlem3  36120  ftc1anclem7  36160  areacirclem1  36169  areacirc  36174  isbnd3  36246  lcmineqlem18  40506  2xp3dxp2ge1d  40617  3cubeslem2  41011  3cubeslem3r  41013  pellfundex  41212  rmxluc  41263  rmyluc  41264  rmxdbl  41266  rmydbl  41267  jm2.24nn  41286  acongeq  41310  jm2.16nn0  41331  jm3.1lem1  41344  jm3.1lem2  41345  sqrtcval  41920  imo72b2lem0  42445  sineq0ALT  43226  sinmulcos  44113  stirlinglem5  44326  fourierdlem79  44433  fouriercnp  44474  hoicvrrex  44804  2leaddle2  45537  lighneallem4a  45807  nnpw2pmod  46676  itschlc0yqe  46853  sinhpcosh  47192
  Copyright terms: Public domain W3C validator