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

Theorem adddir 9377
Description: Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
Assertion
Ref Expression
adddir  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )

Proof of Theorem adddir
StepHypRef Expression
1 adddi 9371 . . 3  |-  ( ( C  e.  CC  /\  A  e.  CC  /\  B  e.  CC )  ->  ( C  x.  ( A  +  B ) )  =  ( ( C  x.  A )  +  ( C  x.  B ) ) )
213coml 1194 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( C  x.  ( A  +  B ) )  =  ( ( C  x.  A )  +  ( C  x.  B ) ) )
3 addcl 9364 . . . 4  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
4 mulcom 9368 . . . 4  |-  ( ( ( A  +  B
)  e.  CC  /\  C  e.  CC )  ->  ( ( A  +  B )  x.  C
)  =  ( C  x.  ( A  +  B ) ) )
53, 4sylan 471 . . 3  |-  ( ( ( A  e.  CC  /\  B  e.  CC )  /\  C  e.  CC )  ->  ( ( A  +  B )  x.  C )  =  ( C  x.  ( A  +  B ) ) )
653impa 1182 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( C  x.  ( A  +  B
) ) )
7 mulcom 9368 . . . 4  |-  ( ( A  e.  CC  /\  C  e.  CC )  ->  ( A  x.  C
)  =  ( C  x.  A ) )
873adant2 1007 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  C )  =  ( C  x.  A ) )
9 mulcom 9368 . . . 4  |-  ( ( B  e.  CC  /\  C  e.  CC )  ->  ( B  x.  C
)  =  ( C  x.  B ) )
1093adant1 1006 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( B  x.  C )  =  ( C  x.  B ) )
118, 10oveq12d 6109 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  C
)  +  ( B  x.  C ) )  =  ( ( C  x.  A )  +  ( C  x.  B
) ) )
122, 6, 113eqtr4d 2485 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756  (class class class)co 6091   CCcc 9280    + caddc 9285    x. cmul 9287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-addcl 9342  ax-mulcom 9346  ax-distr 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094
This theorem is referenced by:  mulid1  9383  adddiri  9397  adddird  9411  muladd11  9539  00id  9544  cnegex2  9551  muladd  9777  ser1const  11862  hashxplem  12195  demoivreALT  13485  dvds2ln  13563  dvds2add  13564  odd2np1lem  13591  cncrng  17837  icccvx  20522  sincosq1eq  21974  abssinper  21980  sineq0  21983  bposlem9  22631  cnrngo  23890  cncvc  23961  ipasslem1  24231  ipasslem11  24240  cdj3i  25845  mblfinlem3  28430  expgrowth  29609
  Copyright terms: Public domain W3C validator