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

Theorem 2times 12296
Description: Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
Assertion
Ref Expression
2times (๐ด โˆˆ โ„‚ โ†’ (2 ยท ๐ด) = (๐ด + ๐ด))

Proof of Theorem 2times
StepHypRef Expression
1 df-2 12223 . . 3 2 = (1 + 1)
21oveq1i 7372 . 2 (2 ยท ๐ด) = ((1 + 1) ยท ๐ด)
3 1p1times 11333 . 2 (๐ด โˆˆ โ„‚ โ†’ ((1 + 1) ยท ๐ด) = (๐ด + ๐ด))
42, 3eqtrid 2789 1 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ๐ด) = (๐ด + ๐ด))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7362  โ„‚cc 11056  1c1 11059   + caddc 11061   ยท cmul 11063  2c2 12215
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 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-mulcl 11120  ax-mulcom 11122  ax-mulass 11124  ax-distr 11125  ax-1rid 11128  ax-cnre 11131
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 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12223
This theorem is referenced by:  times2  12297  2timesi  12298  2txmxeqx  12300  2halves  12388  halfaddsub  12393  avglt2  12399  2timesd  12403  expubnd  14089  absmax  15221  sinmul  16061  sin2t  16066  cos2t  16067  sadadd2lem2  16337  pythagtriplem4  16698  pythagtriplem14  16707  pythagtriplem16  16709  2sqreultlem  26811  2sqreunnltlem  26814  cncph  29803  pellexlem2  41182  acongrep  41333  sub2times  43580  2timesgt  43596
  Copyright terms: Public domain W3C validator