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−B2=A2-2⁢A⁢B+B2

Proof

Step Hyp Ref Expression
1 negcl ⊢B∈ℂ→−B∈ℂ
2 binom2 ⊢A∈ℂ∧−B∈ℂ→A+−B2=A2+2⁢A⁢−B+−B2
3 1 2 sylan2 ⊢A∈ℂ∧B∈ℂ→A+−B2=A2+2⁢A⁢−B+−B2
4 negsub ⊢A∈ℂ∧B∈ℂ→A+−B=A−B
5 4 oveq1d ⊢A∈ℂ∧B∈ℂ→A+−B2=A−B2
6 3 5 eqtr3d ⊢A∈ℂ∧B∈ℂ→A2+2⁢A⁢−B+−B2=A−B2
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∈ℂ→A2+−2⁢A⁢B=A2+2⁢A⁢−B
15 sqcl ⊢A∈ℂ→A2∈ℂ
16 15 adantr ⊢A∈ℂ∧B∈ℂ→A2∈ℂ
17 mulcl ⊢2∈ℂ∧A⁢B∈ℂ→2⁢A⁢B∈ℂ
18 9 10 17 sylancr ⊢A∈ℂ∧B∈ℂ→2⁢A⁢B∈ℂ
19 16 18 negsubd ⊢A∈ℂ∧B∈ℂ→A2+−2⁢A⁢B=A2−2⁢A⁢B
20 14 19 eqtr3d ⊢A∈ℂ∧B∈ℂ→A2+2⁢A⁢−B=A2−2⁢A⁢B
21 sqneg ⊢B∈ℂ→−B2=B2
22 21 adantl ⊢A∈ℂ∧B∈ℂ→−B2=B2
23 20 22 oveq12d ⊢A∈ℂ∧B∈ℂ→A2+2⁢A⁢−B+−B2=A2-2⁢A⁢B+B2
24 6 23 eqtr3d ⊢A∈ℂ∧B∈ℂ→A−B2=A2-2⁢A⁢B+B2