Metamath Proof Explorer

Theorem muladdi

Description: Product of two sums. (Contributed by NM, 17-May-1999)

Ref Expression
Hypotheses mulm1.1 
|- A e. CC
mulneg.2 
|- B e. CC
subdi.3 
|- C e. CC
muladdi.4 
|- D e. CC
Assertion muladdi 
|- ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) )

Proof

Step Hyp Ref Expression
1 mulm1.1 
 |-  A e. CC
2 mulneg.2 
 |-  B e. CC
3 subdi.3 
 |-  C e. CC
4 muladdi.4 
 |-  D e. CC
5 muladd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )
6 1 2 3 4 5 mp4an 
 |-  ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) )