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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( ( 𝐴 − 𝐵 ) ↑ 2 ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) ∈ ℂ )
3	1 2	mpan	⊢ ( 𝐵 ∈ ℂ → ( 2 · 𝐵 ) ∈ ℂ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · 𝐵 ) ∈ ℂ )
5		subadd23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 2 · 𝐵 ) ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) = ( 𝐴 + ( ( 2 · 𝐵 ) − 𝐵 ) ) )
6	4 5	mpd3an3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) = ( 𝐴 + ( ( 2 · 𝐵 ) − 𝐵 ) ) )
7		2txmxeqx	⊢ ( 𝐵 ∈ ℂ → ( ( 2 · 𝐵 ) − 𝐵 ) = 𝐵 )
8	7	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · 𝐵 ) − 𝐵 ) = 𝐵 )
9	8	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + ( ( 2 · 𝐵 ) − 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
10	6 9	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
11	10	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
12		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
13	12 4 12	adddird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + ( 2 · 𝐵 ) ) · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )
14	11 13	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )
15		subsq	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
16		sqval	⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( 𝐴 − 𝐵 ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
17	12 16	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) ↑ 2 ) = ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) )
18	17	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) ↑ 2 ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) = ( ( ( 𝐴 − 𝐵 ) · ( 𝐴 − 𝐵 ) ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )
19	14 15 18	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( ( 𝐴 − 𝐵 ) ↑ 2 ) + ( ( 2 · 𝐵 ) · ( 𝐴 − 𝐵 ) ) ) )