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

Theorem 2times 11761
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 11688 . . 3 2 = (1 + 1)
21oveq1i 7150 . 2 (2 · 𝐴) = ((1 + 1) · 𝐴)
3 1p1times 10800 . 2 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
42, 3syl5eq 2869 1 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2114  (class class class)co 7140  cc 10524  1c1 10527   + caddc 10529   · cmul 10531  2c2 11680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ral 3135  df-rex 3136  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143  df-2 11688
This theorem is referenced by:  times2  11762  2timesi  11763  2txmxeqx  11765  2halves  11853  halfaddsub  11858  avglt2  11864  2timesd  11868  expubnd  13537  absmax  14680  sinmul  15516  sin2t  15521  cos2t  15522  sadadd2lem2  15788  pythagtriplem4  16145  pythagtriplem14  16154  pythagtriplem16  16156  2sqreultlem  26029  2sqreunnltlem  26032  cncph  28600  pellexlem2  39701  acongrep  39851  sub2times  41844  2timesgt  41858
  Copyright terms: Public domain W3C validator