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

Theorem 2timesi 11752
Description: Two times a number. (Contributed by NM, 1-Aug-1999.)
Hypothesis
Ref Expression
2timesi.1 𝐴 ∈ ℂ
Assertion
Ref Expression
2timesi (2 · 𝐴) = (𝐴 + 𝐴)

Proof of Theorem 2timesi
StepHypRef Expression
1 2timesi.1 . 2 𝐴 ∈ ℂ
2 2times 11750 . 2 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
31, 2ax-mp 5 1 (2 · 𝐴) = (𝐴 + 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2114  (class class class)co 7131  cc 10511   + caddc 10516   · cmul 10518  2c2 11669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-resscn 10570  ax-1cn 10571  ax-icn 10572  ax-addcl 10573  ax-mulcl 10575  ax-mulcom 10577  ax-mulass 10579  ax-distr 10580  ax-1rid 10583  ax-cnre 10586
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-dif 3915  df-un 3917  df-in 3919  df-ss 3928  df-nul 4268  df-if 4442  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4813  df-br 5041  df-iota 6288  df-fv 6337  df-ov 7134  df-2 11677
This theorem is referenced by:  2t2e4  11778  nn0le2xi  11928  binom2i  13557  rddif  14678  abs3lemi  14748  iseraltlem2  15017  prmreclem6  16233  mod2xi  16381  numexp2x  16391  prmlem2  16429  iihalf2  23514  pcoass  23605  ovolunlem1a  24076  tangtx  25074  sinq34lt0t  25078  eff1o  25117  ang180lem2  25372  dvatan  25497  basellem2  25643  basellem5  25646  chtub  25772  bposlem9  25852  ex-dvds  28217  norm3lem  28908  normpari  28913  polid2i  28916  ballotth  31800  heiborlem6  35127  sqsumi  39274  dirkertrigeqlem1  42518  fourierdlem94  42620  fourierdlem102  42628  fourierdlem111  42637  fourierdlem112  42638  fourierdlem113  42639  fourierdlem114  42640  sqwvfoura  42648  sqwvfourb  42649  fouriersw  42651  fmtnorec3  43840  2t6m3t4e0  44526  zlmodzxzequa  44681
  Copyright terms: Public domain W3C validator