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

Theorem adddir 11095
Description: Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
Assertion
Ref Expression
adddir ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))

Proof of Theorem adddir
StepHypRef Expression
1 adddi 11087 . . 3 ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐶 · (𝐴 + 𝐵)) = ((𝐶 · 𝐴) + (𝐶 · 𝐵)))
213coml 1127 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶 · (𝐴 + 𝐵)) = ((𝐶 · 𝐴) + (𝐶 · 𝐵)))
3 addcl 11080 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4 mulcom 11084 . . 3 (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = (𝐶 · (𝐴 + 𝐵)))
53, 4stoic3 1777 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = (𝐶 · (𝐴 + 𝐵)))
6 mulcom 11084 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · 𝐶) = (𝐶 · 𝐴))
763adant2 1131 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · 𝐶) = (𝐶 · 𝐴))
8 mulcom 11084 . . . 4 ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
983adant1 1130 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
107, 9oveq12d 7359 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) + (𝐵 · 𝐶)) = ((𝐶 · 𝐴) + (𝐶 · 𝐵)))
112, 5, 103eqtr4d 2775 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1086   = wceq 1541  wcel 2110  (class class class)co 7341  cc 10996   + caddc 11001   · cmul 11003
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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-addcl 11058  ax-mulcom 11062  ax-distr 11065
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344
This theorem is referenced by:  mulrid  11102  adddiri  11117  adddird  11129  muladd11  11275  00id  11280  cnegex2  11287  muladd  11541  ser1const  13957  hashxplem  14332  demoivreALT  16102  dvds2ln  16192  dvds2add  16193  odd2np1lem  16243  cncrng  21318  cncrngOLD  21319  icccvx  24868  cnlmod  25060  sincosq1eq  26441  abssinper  26450  sineq0  26453  bposlem9  27223  cncvcOLD  30553  ipasslem1  30801  ipasslem11  30810  cdj3i  32411  mblfinlem3  37678  expgrowth  44347  fmtnofac2lem  47578  2zrngALT  48264
  Copyright terms: Public domain W3C validator