Theorem binom2i

Description: The square of a binomial. (Contributed by NM, 11-Aug-1999)

	Ref	Expression
Hypotheses	binom2.1	$$⊢A\in ℂ$$
	binom2.2	$$⊢B\in ℂ$$
Assertion	binom2i	$$⊢{\left(A+B\right)}^2=A^2+2AB+B^2$$

Proof

Step	Hyp	Ref	Expression
1		binom2.1	$$⊢A\in ℂ$$
2		binom2.2	$$⊢B\in ℂ$$
3	1 2	addcli	$$⊢A+B\in ℂ$$
4	3 1 2	adddii	$$⊢\left(A+B\right)\left(A+B\right)=\left(A+B\right)A+\left(A+B\right)B$$
5	1 2 1	adddiri	$$⊢\left(A+B\right)A=AA+BA$$
6	2 1	mulcomi	$$⊢BA=AB$$
7	6	oveq2i	$$⊢AA+BA=AA+AB$$
8	5 7	eqtri	$$⊢\left(A+B\right)A=AA+AB$$
9	1 2 2	adddiri	$$⊢\left(A+B\right)B=AB+BB$$
10	8 9	oveq12i	$$⊢\left(A+B\right)A+\left(A+B\right)B=AA+AB+AB+BB$$
11	1 1	mulcli	$$⊢AA\in ℂ$$
12	1 2	mulcli	$$⊢AB\in ℂ$$
13	11 12	addcli	$$⊢AA+AB\in ℂ$$
14	2 2	mulcli	$$⊢BB\in ℂ$$
15	13 12 14	addassi	$$⊢\left(AA+AB\right)+AB+BB=AA+AB+AB+BB$$
16	11 12 12	addassi	$$⊢AA+AB+AB=AA+AB+AB$$
17	16	oveq1i	$$⊢\left(AA+AB\right)+AB+BB=AA+\left(AB+AB\right)+BB$$
18	10 15 17	3eqtr2i	$$⊢\left(A+B\right)A+\left(A+B\right)B=AA+\left(AB+AB\right)+BB$$
19	4 18	eqtri	$$⊢\left(A+B\right)\left(A+B\right)=AA+\left(AB+AB\right)+BB$$
20	3	sqvali	$$⊢{\left(A+B\right)}^2=\left(A+B\right)\left(A+B\right)$$
21	1	sqvali	$$⊢A^2=AA$$
22	12	2timesi	$$⊢2AB=AB+AB$$
23	21 22	oveq12i	$$⊢A^2+2AB=AA+AB+AB$$
24	2	sqvali	$$⊢B^2=BB$$
25	23 24	oveq12i	$$⊢A^2+2AB+B^2=AA+\left(AB+AB\right)+BB$$
26	19 20 25	3eqtr4i	$$⊢{\left(A+B\right)}^2=A^2+2AB+B^2$$