Metamath Proof Explorer

Theorem subsq2

Description: Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008)

		Ref	Expression
	Assertion	subsq2	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} - B^{2} = {(A - B)}^{2} + 2 B (A - B)$

Proof

Step	Hyp	Ref	Expression
1		2cn	$⊢ 2 \in ℂ$
2		mulcl	$⊢ (2 \in ℂ \land B \in ℂ) \to 2 B \in ℂ$
3	1 2	mpan	$⊢ B \in ℂ \to 2 B \in ℂ$
4	3	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to 2 B \in ℂ$
5		subadd23	$⊢ (A \in ℂ \land B \in ℂ \land 2 B \in ℂ) \to A - B + 2 B = A + 2 B - B$
6	4 5	mpd3an3	$⊢ (A \in ℂ \land B \in ℂ) \to A - B + 2 B = A + 2 B - B$
7		2txmxeqx	$⊢ B \in ℂ \to 2 B - B = B$
8	7	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to 2 B - B = B$
9	8	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to A + 2 B - B = A + B$
10	6 9	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to A - B + 2 B = A + B$
11	10	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to (A - B + 2 B) (A - B) = (A + B) (A - B)$
12		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
13	12 4 12	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (A - B + 2 B) (A - B) = (A - B) (A - B) + 2 B (A - B)$
14	11 13	eqtr3d	$⊢ (A \in ℂ \land B \in ℂ) \to (A + B) (A - B) = (A - B) (A - B) + 2 B (A - B)$
15		subsq	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} - B^{2} = (A + B) (A - B)$
16		sqval	$⊢ A - B \in ℂ \to {(A - B)}^{2} = (A - B) (A - B)$
17	12 16	syl	$⊢ (A \in ℂ \land B \in ℂ) \to {(A - B)}^{2} = (A - B) (A - B)$
18	17	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to {(A - B)}^{2} + 2 B (A - B) = (A - B) (A - B) + 2 B (A - B)$
19	14 15 18	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} - B^{2} = {(A - B)}^{2} + 2 B (A - B)$