Theorem binom2

Description: The square of a binomial. (Contributed by FL, 10-Dec-2006)

	Ref	Expression
Assertion	binom2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^2=A^2+2AB+B^2$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to A+B=if\left(A\in ℂ,A,0\right)+B$$
2	1	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to {\left(A+B\right)}^2={\left(if\left(A\in ℂ,A,0\right)+B\right)}^2$$
3		oveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to A^2={if\left(A\in ℂ,A,0\right)}^2$$
4		oveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to AB=if\left(A\in ℂ,A,0\right)B$$
5	4	oveq2d	$$⊢A=if\left(A\in ℂ,A,0\right)\to 2AB=2if\left(A\in ℂ,A,0\right)B$$
6	3 5	oveq12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to A^2+2AB={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)B$$
7	6	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to A^2+2AB+B^2={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)B+B^2$$
8	2 7	eqeq12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left({\left(A+B\right)}^2=A^2+2AB+B^2\leftrightarrow {\left(if\left(A\in ℂ,A,0\right)+B\right)}^2={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)B+B^2\right)$$
9		oveq2	$$⊢B=if\left(B\in ℂ,B,0\right)\to if\left(A\in ℂ,A,0\right)+B=if\left(A\in ℂ,A,0\right)+if\left(B\in ℂ,B,0\right)$$
10	9	oveq1d	$$⊢B=if\left(B\in ℂ,B,0\right)\to {\left(if\left(A\in ℂ,A,0\right)+B\right)}^2={\left(if\left(A\in ℂ,A,0\right)+if\left(B\in ℂ,B,0\right)\right)}^2$$
11		oveq2	$$⊢B=if\left(B\in ℂ,B,0\right)\to if\left(A\in ℂ,A,0\right)B=if\left(A\in ℂ,A,0\right)if\left(B\in ℂ,B,0\right)$$
12	11	oveq2d	$$⊢B=if\left(B\in ℂ,B,0\right)\to 2if\left(A\in ℂ,A,0\right)B=2if\left(A\in ℂ,A,0\right)if\left(B\in ℂ,B,0\right)$$
13	12	oveq2d	$$⊢B=if\left(B\in ℂ,B,0\right)\to {if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)B={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)if\left(B\in ℂ,B,0\right)$$
14		oveq1	$$⊢B=if\left(B\in ℂ,B,0\right)\to B^2={if\left(B\in ℂ,B,0\right)}^2$$
15	13 14	oveq12d	$$⊢B=if\left(B\in ℂ,B,0\right)\to {if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)B+B^2={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)if\left(B\in ℂ,B,0\right)+{if\left(B\in ℂ,B,0\right)}^2$$
16	10 15	eqeq12d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left({\left(if\left(A\in ℂ,A,0\right)+B\right)}^2={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)B+B^2\leftrightarrow {\left(if\left(A\in ℂ,A,0\right)+if\left(B\in ℂ,B,0\right)\right)}^2={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)if\left(B\in ℂ,B,0\right)+{if\left(B\in ℂ,B,0\right)}^2\right)$$
17		0cn	$$⊢0\in ℂ$$
18	17	elimel	$$⊢if\left(A\in ℂ,A,0\right)\in ℂ$$
19	17	elimel	$$⊢if\left(B\in ℂ,B,0\right)\in ℂ$$
20	18 19	binom2i	$$⊢{\left(if\left(A\in ℂ,A,0\right)+if\left(B\in ℂ,B,0\right)\right)}^2={if\left(A\in ℂ,A,0\right)}^2+2if\left(A\in ℂ,A,0\right)if\left(B\in ℂ,B,0\right)+{if\left(B\in ℂ,B,0\right)}^2$$
21	8 16 20	dedth2h	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^2=A^2+2AB+B^2$$