Metamath Proof Explorer


Theorem mulbinom2

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

Ref Expression
Assertion mulbinom2 ABCCA+B2=CA2+2CAB+B2

Proof

Step Hyp Ref Expression
1 mulcl CACA
2 1 ancoms ACCA
3 2 3adant2 ABCCA
4 simp2 ABCB
5 binom2 CABCA+B2=CA2+2CAB+B2
6 3 4 5 syl2anc ABCCA+B2=CA2+2CAB+B2
7 mulass CABCAB=CAB
8 7 3coml ABCCAB=CAB
9 8 oveq2d ABC2CAB=2CAB
10 2cnd ABC2
11 simp3 ABCC
12 mulcl ABAB
13 12 3adant3 ABCAB
14 10 11 13 mulassd ABC2CAB=2CAB
15 9 14 eqtr4d ABC2CAB=2CAB
16 15 oveq2d ABCCA2+2CAB=CA2+2CAB
17 16 oveq1d ABCCA2+2CAB+B2=CA2+2CAB+B2
18 6 17 eqtrd ABCCA+B2=CA2+2CAB+B2