mulsubaddmulsub

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

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

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B \in ℂ$
2		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C \in ℂ$
3	1 2	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C \in ℂ$
4		subaddmulsub	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land B C \in ℂ) \to B C - (A + B) (C - D) = (B C - A C - B C) + A D + B D$
5	3 4	mpd3an3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C - (A + B) (C - D) = (B C - A C - B C) + A D + B D$
6		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A \in ℂ$
7	6 2	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C \in ℂ$
8	3 7 3	sub32d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C - A C - B C = B C - B C - A C$
9	3	subidd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C - B C = 0$
10	9	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C - B C - A C = 0 - A C$
11	8 10	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C - A C - B C = 0 - A C$
12		df-neg	$⊢ - A C = 0 - A C$
13	11 12	syl6eqr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C - A C - B C = - A C$
14	13	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (B C - A C - B C) + A D + B D = (- A C) + A D + B D$
15	7	negcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to - A C \in ℂ$
16		simprr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D \in ℂ$
17	6 16	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A D \in ℂ$
18	1 16	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B D \in ℂ$
19	17 18	addcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A D + B D \in ℂ$
20	15 19	addcomd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (- A C) + A D + B D = A D + B D + (- A C)$
21	19 7	negsubd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A D + B D + (- A C) = A D + B D - A C$
22	20 21	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (- A C) + A D + B D = A D + B D - A C$
23	14 22	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (B C - A C - B C) + A D + B D = A D + B D - A C$
24	5 23	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C - (A + B) (C - D) = A D + B D - A C$

Metamath Proof Explorer

Theorem mulsubaddmulsub

Proof