Metamath Proof Explorer

Theorem subsq

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

Ref Expression
Assertion subsq ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 − B 2 = A + B ⁢ A − B

Proof

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