Metamath Proof Explorer

Theorem addmulsub

Description: The product of a sum and a difference. (Contributed by AV, 5-Mar-2023)

Ref Expression
Assertion addmulsub 
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> A e. CC )
2 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> B e. CC )
3 1 2 addcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A + B ) e. CC )
4 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> C e. CC )
5 simprr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> D e. CC )
6 3 4 5 subdid 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C - D ) ) = ( ( ( A + B ) x. C ) - ( ( A + B ) x. D ) ) )
7 1 2 4 adddird 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )
8 1 2 5 adddird 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. D ) = ( ( A x. D ) + ( B x. D ) ) )
9 7 8 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) x. C ) - ( ( A + B ) x. D ) ) = ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) )
10 6 9 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) )