Metamath Proof Explorer

Theorem binom2sub

Description: Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 binom2 ⊢ A ∈ ℂ ∧ − B ∈ ℂ → A + − B 2 = A 2 + 2 ⁢ A ⁢ − B + − B 2
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B 2 = A 2 + 2 ⁢ A ⁢ − B + − B 2
4 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
5 4 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B 2 = A − B 2
6 3 5 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 + 2 ⁢ A ⁢ − B + − B 2 = A − B 2
7 mulneg2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ − B = − A ⁢ B
8 7 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ A ⁢ − B = 2 ⁢ − A ⁢ B
9 2cn ⊢ 2 ∈ ℂ
10 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
11 mulneg2 ⊢ 2 ∈ ℂ ∧ A ⁢ B ∈ ℂ → 2 ⁢ − A ⁢ B = − 2 ⁢ A ⁢ B
12 9 10 11 sylancr ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ − A ⁢ B = − 2 ⁢ A ⁢ B
13 8 12 eqtr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − 2 ⁢ A ⁢ B = 2 ⁢ A ⁢ − B
14 13 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 + − 2 ⁢ A ⁢ B = A 2 + 2 ⁢ A ⁢ − B
15 sqcl ⊢ A ∈ ℂ → A 2 ∈ ℂ
16 15 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 ∈ ℂ
17 mulcl ⊢ 2 ∈ ℂ ∧ A ⁢ B ∈ ℂ → 2 ⁢ A ⁢ B ∈ ℂ
18 9 10 17 sylancr ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ A ⁢ B ∈ ℂ
19 16 18 negsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 + − 2 ⁢ A ⁢ B = A 2 − 2 ⁢ A ⁢ B
20 14 19 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 + 2 ⁢ A ⁢ − B = A 2 − 2 ⁢ A ⁢ B
21 sqneg ⊢ B ∈ ℂ → − B 2 = B 2
22 21 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → − B 2 = B 2
23 20 22 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 + 2 ⁢ A ⁢ − B + − B 2 = A 2 - 2 ⁢ A ⁢ B + B 2
24 6 23 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B 2 = A 2 - 2 ⁢ A ⁢ B + B 2