Theorem adddir 9047

Description: Distributive law for complex numbers. (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

Step	Hyp	Ref	Expression
1		adddi 9043	. . 3 |- ( ( C e. CC /\ A e. CC /\ B e. CC ) -> ( C x. ( A + B ) ) = ( ( C x. A ) + ( C x. B ) ) )
2	1	3coml 1160	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C x. ( A + B ) ) = ( ( C x. A ) + ( C x. B ) ) )
3		addcl 9036	. . . 4 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4		mulcom 9040	. . . 4 |- ( ( ( A + B ) e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( C x. ( A + B ) ) )
5	3, 4	sylan 458	. . 3 |- ( ( ( A e. CC /\ B e. CC ) /\ C e. CC ) -> ( ( A + B ) x. C ) = ( C x. ( A + B ) ) )
6	5	3impa 1148	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( C x. ( A + B ) ) )
7		mulcom 9040	. . . 4 |- ( ( A e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
8	7	3adant2 976	. . 3 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
9		mulcom 9040	. . . 4 |- ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
10	9	3adant1 975	. . 3 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
11	8, 10	oveq12d 6066	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. C ) + ( B x. C ) ) = ( ( C x. A ) + ( C x. B ) ) )
12	2, 6, 11	3eqtr4d 2454	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721  (class class class)co 6048   CCcc 8952   + caddc 8957   x. cmul 8959

This theorem is referenced by:  mulid1  9052  adddiri  9065  adddird  9077  muladd11  9200  00id  9205  cnegex2  9212  muladd  9430  ser1const  11342  hashxplem  11659  demoivreALT  12765  dvds2ln  12843  dvds2add  12844  odd2np1lem  12870  cncrng  16685  icccvx  18936  sincosq1eq  20381  abssinper  20387  sineq0  20390  bposlem9  21037  cnrngo  21952  cncvc  22023  ipasslem1  22293  ipasslem11  22302  cdj3i  23905  mblfinlem2  26152  expgrowth  27428

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-addcl 9014  ax-mulcom 9018  ax-distr 9021

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-iota 5385  df-fv 5429  df-ov 6051