addmulsub

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

		Ref	Expression
	Assertion	addmulsub	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) (C - D) = A C + B C - (A D + B D)$

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A \in ℂ$
2		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B \in ℂ$
3	1 2	addcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B \in ℂ$
4		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C \in ℂ$
5		simprr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D \in ℂ$
6	3 4 5	subdid	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) (C - D) = (A + B) C - (A + B) D$
7	1 2 4	adddird	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) C = A C + B C$
8	1 2 5	adddird	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) D = A D + B D$
9	7 8	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) C - (A + B) D = A C + B C - (A D + B D)$
10	6 9	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B) (C - D) = A C + B C - (A D + B D)$

Metamath Proof Explorer