Metamath Proof Explorer

Theorem muldivbinom2

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

Ref Expression
Assertion muldivbinom2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 C = C ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 C

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
2 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
3 0cnd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 0 ∈ ℂ
4 1 2 3 3jca ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ ∧ B ∈ ℂ ∧ 0 ∈ ℂ
5 mulsubdivbinom2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ 0 ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 − 0 C = C ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 0 C
6 4 5 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 − 0 C = C ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 0 C
7 simp3l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
8 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ∈ ℂ
9 7 8 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A ∈ ℂ
10 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
11 9 10 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B ∈ ℂ
12 11 sqcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 ∈ ℂ
13 12 subid1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 − 0 = C ⁢ A + B 2
14 13 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 = C ⁢ A + B 2 − 0
15 14 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 C = C ⁢ A + B 2 − 0 C
16 sqcl ⊢ B ∈ ℂ → B 2 ∈ ℂ
17 16 subid1d ⊢ B ∈ ℂ → B 2 − 0 = B 2
18 17 3ad2ant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B 2 − 0 = B 2
19 18 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B 2 = B 2 − 0
20 19 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B 2 C = B 2 − 0 C
21 20 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 C = C ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 − 0 C
22 6 15 21 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A + B 2 C = C ⁢ A 2 + 2 ⁢ A ⁢ B + B 2 C