Theorem mulbinom2

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

	Ref	Expression
Assertion	mulbinom2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐶 · 𝐴 ) + 𝐵 ) ↑ 2 ) = ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 2 · 𝐶 ) · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )

Proof

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