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 ∈ ℂ ∧ B ∈ ℂ → A 2 − B 2 = A − B 2 + 2 ⁢ B ⁢ A − B

Proof

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