subsq

Description: Factor the difference of two squares. (Contributed by NM, 21-Feb-2008)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
2		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
3		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
4	1 2 3	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (A + B) (A - B) = A (A - B) + B (A - B)$
5		subdi	$⊢ (A \in ℂ \land A \in ℂ \land B \in ℂ) \to A (A - B) = A A - A B$
6	5	3anidm12	$⊢ (A \in ℂ \land B \in ℂ) \to A (A - B) = A A - A B$
7		sqval	$⊢ A \in ℂ \to A^{2} = A A$
8	7	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} = A A$
9	8	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} - A B = A A - A B$
10	6 9	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to A (A - B) = A^{2} - A B$
11	2 1 2	subdid	$⊢ (A \in ℂ \land B \in ℂ) \to B (A - B) = B A - B B$
12		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
13		sqval	$⊢ B \in ℂ \to B^{2} = B B$
14	13	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to B^{2} = B B$
15	12 14	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to A B - B^{2} = B A - B B$
16	11 15	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to B (A - B) = A B - B^{2}$
17	10 16	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to A (A - B) + B (A - B) = (A^{2} - A B) + A B - B^{2}$
18		sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$
19	18	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} \in ℂ$
20		mulcl	$⊢ (A \in ℂ \land B \in ℂ) \to A B \in ℂ$
21		sqcl	$⊢ B \in ℂ \to B^{2} \in ℂ$
22	21	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to B^{2} \in ℂ$
23	19 20 22	npncand	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} - A B) + A B - B^{2} = A^{2} - B^{2}$
24	4 17 23	3eqtrrd	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} - B^{2} = (A + B) (A - B)$

Metamath Proof Explorer

Theorem subsq

Proof