Theorem subsq

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

	Ref	Expression
Assertion	subsq	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
2		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
3		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
4	1 2 3	adddird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 · ( 𝐴 − 𝐵 ) ) + ( 𝐵 · ( 𝐴 − 𝐵 ) ) ) )
5		subdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) − ( 𝐴 · 𝐵 ) ) )
6	5	3anidm12	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) − ( 𝐴 · 𝐵 ) ) )
7		sqval	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
8	7	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
9	8	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐴 · 𝐵 ) ) = ( ( 𝐴 · 𝐴 ) − ( 𝐴 · 𝐵 ) ) )
10	6 9	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 ↑ 2 ) − ( 𝐴 · 𝐵 ) ) )
11	2 1 2	subdid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐵 · 𝐴 ) − ( 𝐵 · 𝐵 ) ) )
12		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
13		sqval	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
14	13	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
15	12 14	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 · 𝐴 ) − ( 𝐵 · 𝐵 ) ) )
16	11 15	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐵 ↑ 2 ) ) )
17	10 16	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 𝐴 − 𝐵 ) ) + ( 𝐵 · ( 𝐴 − 𝐵 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 𝐴 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) − ( 𝐵 ↑ 2 ) ) ) )
18		sqcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
19	18	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
20		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
21		sqcl	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 2 ) ∈ ℂ )
22	21	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
23	19 20 22	npncand	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) − ( 𝐴 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
24	4 17 23	3eqtrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) )