Metamath Proof Explorer

Theorem binom2sub

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

Ref Expression
Assertion binom2sub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )

Proof

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