This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )