Metamath Proof Explorer

Theorem mulbinom2

Description: The square of a binomial with factor. (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion mulbinom2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A + B 2 = C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B + B 2

Proof

Step Hyp Ref Expression
1 mulcl ⊢ C ∈ ℂ ∧ A ∈ ℂ → C ⁢ A ∈ ℂ
2 1 ancoms ⊢ A ∈ ℂ ∧ C ∈ ℂ → C ⁢ A ∈ ℂ
3 2 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A ∈ ℂ
4 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
5 binom2 ⊢ C ⁢ A ∈ ℂ ∧ B ∈ ℂ → C ⁢ A + B 2 = C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B + B 2
6 3 4 5 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A + B 2 = C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B + B 2
7 mulass ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → C ⁢ A ⁢ B = C ⁢ A ⁢ B
8 7 3coml ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A ⁢ B = C ⁢ A ⁢ B
9 8 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → 2 ⁢ C ⁢ A ⁢ B = 2 ⁢ C ⁢ A ⁢ B
10 2cnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → 2 ∈ ℂ
11 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
12 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
13 12 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ∈ ℂ
14 10 11 13 mulassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → 2 ⁢ C ⁢ A ⁢ B = 2 ⁢ C ⁢ A ⁢ B
15 9 14 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → 2 ⁢ C ⁢ A ⁢ B = 2 ⁢ C ⁢ A ⁢ B
16 15 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B = C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B
17 16 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B + B 2 = C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B + B 2
18 6 17 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A + B 2 = C ⁢ A 2 + 2 ⁢ C ⁢ A ⁢ B + B 2