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

Theorem 2times 11022
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 10956 . . 3 2 = (1 + 1)
21oveq1i 6559 . 2 (2 · 𝐴) = ((1 + 1) · 𝐴)
3 1p1times 10086 . 2 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
42, 3syl5eq 2656 1 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  (class class class)co 6549  cc 9813  1c1 9816   + caddc 9818   · cmul 9820  2c2 10947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulcom 9879  ax-mulass 9881  ax-distr 9882  ax-1rid 9885  ax-cnre 9888
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-2 10956
This theorem is referenced by:  times2  11023  2timesi  11024  2txmxeqx  11026  2halves  11137  halfaddsub  11142  avglt2  11148  2timesd  11152  expubnd  12783  subsq2  12835  absmax  13917  sinmul  14741  sin2t  14746  cos2t  14747  sadadd2lem2  15010  pythagtriplem4  15362  pythagtriplem14  15371  pythagtriplem16  15373  cncph  27058  pellexlem2  36412  acongrep  36565  sub2times  38426  2timesgt  38441
  Copyright terms: Public domain W3C validator