Theorem binom4

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom , but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	binom4	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^4=A^4+4A^{3}B+6A^2{B}^2+\left(4A{B}^3+B^4\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-4	$$⊢4=3+1$$
2	1	oveq2i	$$⊢{\left(A+B\right)}^4={\left(A+B\right)}^{3+1}$$
3		addcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B\in ℂ$$
4		3nn0	$$⊢3\in {\mathbb{N}}_0$$
5		expp1	$$⊢\left(A+B\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to {\left(A+B\right)}^{3+1}={\left(A+B\right)}^3\left(A+B\right)$$
6	3 4 5	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^{3+1}={\left(A+B\right)}^3\left(A+B\right)$$
7	2 6	syl5eq	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^4={\left(A+B\right)}^3\left(A+B\right)$$
8		binom3	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^3=A^3+3A^{2}B+3A{B}^2+B^3$$
9	8	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^3\left(A+B\right)=\left(A^3+3A^{2}B+3A{B}^2+B^3\right)\left(A+B\right)$$
10		simpl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\in ℂ$$
11		expcl	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℂ$$
12	10 4 11	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^3\in ℂ$$
13		3cn	$$⊢3\in ℂ$$
14	10	sqcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^2\in ℂ$$
15		simpr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B\in ℂ$$
16	14 15	mulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2}B\in ℂ$$
17		mulcl	$$⊢\left(3\in ℂ\wedge A^{2}B\in ℂ\right)\to 3A^{2}B\in ℂ$$
18	13 16 17	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{2}B\in ℂ$$
19	12 18	addcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^3+3A^{2}B\in ℂ$$
20	15	sqcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^2\in ℂ$$
21	10 20	mulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^2\in ℂ$$
22		mulcl	$$⊢\left(3\in ℂ\wedge A{B}^2\in ℂ\right)\to 3A{B}^2\in ℂ$$
23	13 21 22	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^2\in ℂ$$
24		expcl	$$⊢\left(B\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to B^3\in ℂ$$
25	15 4 24	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^3\in ℂ$$
26	23 25	addcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^2+B^3\in ℂ$$
27	19 26	addcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^3+3A^{2}B+3A{B}^2+B^3\in ℂ$$
28	27 10 15	adddid	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B+3A{B}^2+B^3\right)\left(A+B\right)=\left(A^3+3A^{2}B+3A{B}^2+B^3\right)A+\left(A^3+3A^{2}B+3A{B}^2+B^3\right)B$$
29	1	oveq2i	$$⊢A^4=A^{3+1}$$
30		expp1	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^{3+1}=A^{3}A$$
31	10 4 30	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{3+1}=A^{3}A$$
32	29 31	eqtr2id	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{3}A=A^4$$
33	13	a1i	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3\in ℂ$$
34	33 16 10	mulassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{2}BA=3A^{2}BA$$
35	14 15 10	mul32d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2}BA=A^{2}AB$$
36		df-3	$$⊢3=2+1$$
37	36	oveq2i	$$⊢A^3=A^{2+1}$$
38		2nn0	$$⊢2\in {\mathbb{N}}_0$$
39		expp1	$$⊢\left(A\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to A^{2+1}=A^{2}A$$
40	10 38 39	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2+1}=A^{2}A$$
41	37 40	eqtr2id	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2}A=A^3$$
42	41	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2}AB=A^{3}B$$
43	35 42	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2}BA=A^{3}B$$
44	43	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{2}BA=3A^{3}B$$
45	34 44	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{2}BA=3A^{3}B$$
46	32 45	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{3}A+3A^{2}BA=A^4+3A^{3}B$$
47	12 10 18 46	joinlmuladdmuld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B\right)A=A^4+3A^{3}B$$
48	33 21 10	mulassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}A=3A{B}^{2}A$$
49	10 20 10	mul32d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^{2}A=AA{B}^2$$
50	10	sqvald	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^2=AA$$
51	50	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^2{B}^2=AA{B}^2$$
52	49 51	eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^{2}A=A^2{B}^2$$
53	52	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}A=3A^2{B}^2$$
54	48 53	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}A=3A^2{B}^2$$
55	25 10	mulcomd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^{3}A=A{B}^3$$
56	54 55	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}A+B^{3}A=3A^2{B}^2+A{B}^3$$
57	23 10 25 56	joinlmuladdmuld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(3A{B}^2+B^3\right)A=3A^2{B}^2+A{B}^3$$
58	47 57	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B\right)A+\left(3A{B}^2+B^3\right)A=A^4+3A^{3}B+3A^2{B}^2+A{B}^3$$
59	19 10 26 58	joinlmuladdmuld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B+3A{B}^2+B^3\right)A=A^4+3A^{3}B+3A^2{B}^2+A{B}^3$$
60	19 26 15	adddird	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B+3A{B}^2+B^3\right)B=\left(A^3+3A^{2}B\right)B+\left(3A{B}^2+B^3\right)B$$
61	33 16 15	mulassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{2}BB=3A^{2}BB$$
62	14 15 15	mulassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2}BB=A^{2}BB$$
63	15	sqvald	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^2=BB$$
64	63	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^2{B}^2=A^{2}BB$$
65	62 64	eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{2}BB=A^2{B}^2$$
66	65	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{2}BB=3A^2{B}^2$$
67	61 66	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{2}BB=3A^2{B}^2$$
68	67	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{3}B+3A^{2}BB=A^{3}B+3A^2{B}^2$$
69	12 15 18 68	joinlmuladdmuld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B\right)B=A^{3}B+3A^2{B}^2$$
70	33 21 15	mulassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}B=3A{B}^{2}B$$
71	10 20 15	mulassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^{2}B=A{B}^{2}B$$
72	36	oveq2i	$$⊢B^3=B^{2+1}$$
73		expp1	$$⊢\left(B\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to B^{2+1}=B^{2}B$$
74	15 38 73	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^{2+1}=B^{2}B$$
75	72 74	eqtr2id	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^{2}B=B^3$$
76	75	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^{2}B=A{B}^3$$
77	71 76	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^{2}B=A{B}^3$$
78	77	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}B=3A{B}^3$$
79	70 78	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}B=3A{B}^3$$
80	1	oveq2i	$$⊢B^4=B^{3+1}$$
81		expp1	$$⊢\left(B\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to B^{3+1}=B^{3}B$$
82	15 4 81	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^{3+1}=B^{3}B$$
83	80 82	eqtr2id	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^{3}B=B^4$$
84	79 83	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^{2}B+B^{3}B=3A{B}^3+B^4$$
85	23 15 25 84	joinlmuladdmuld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(3A{B}^2+B^3\right)B=3A{B}^3+B^4$$
86	69 85	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B\right)B+\left(3A{B}^2+B^3\right)B=A^{3}B+3A^2{B}^2+3A{B}^3+B^4$$
87	12 15	mulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{3}B\in ℂ$$
88	14 20	mulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^2{B}^2\in ℂ$$
89		mulcl	$$⊢\left(3\in ℂ\wedge A^2{B}^2\in ℂ\right)\to 3A^2{B}^2\in ℂ$$
90	13 88 89	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^2{B}^2\in ℂ$$
91	10 25	mulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^3\in ℂ$$
92		mulcl	$$⊢\left(3\in ℂ\wedge A{B}^3\in ℂ\right)\to 3A{B}^3\in ℂ$$
93	13 91 92	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^3\in ℂ$$
94		4nn0	$$⊢4\in {\mathbb{N}}_0$$
95		expcl	$$⊢\left(B\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to B^4\in ℂ$$
96	15 94 95	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B^4\in ℂ$$
97	93 96	addcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A{B}^3+B^4\in ℂ$$
98	87 90 97	addassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^{3}B+3A^2{B}^2+3A{B}^3+B^4=A^{3}B+3A^2{B}^2+\left(3A{B}^3+B^4\right)$$
99	60 86 98	3eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B+3A{B}^2+B^3\right)B=A^{3}B+3A^2{B}^2+\left(3A{B}^3+B^4\right)$$
100	59 99	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B+3A{B}^2+B^3\right)A+\left(A^3+3A^{2}B+3A{B}^2+B^3\right)B=\left(A^4+3A^{3}B\right)+\left(3A^2{B}^2+A{B}^3\right)+A^{3}B+\left(3A^2{B}^2+3A{B}^3+B^4\right)$$
101		expcl	$$⊢\left(A\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to A^4\in ℂ$$
102	10 94 101	sylancl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^4\in ℂ$$
103		mulcl	$$⊢\left(3\in ℂ\wedge A^{3}B\in ℂ\right)\to 3A^{3}B\in ℂ$$
104	13 87 103	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{3}B\in ℂ$$
105	102 104	addcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^4+3A^{3}B\in ℂ$$
106	90 91	addcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^2{B}^2+A{B}^3\in ℂ$$
107	90 97	addcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^2{B}^2+3A{B}^3+B^4\in ℂ$$
108	105 106 87 107	add4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^4+3A^{3}B\right)+\left(3A^2{B}^2+A{B}^3\right)+A^{3}B+\left(3A^2{B}^2+3A{B}^3+B^4\right)=\left(A^4+3A^{3}B\right)+A^{3}B+\left(3A^2{B}^2+A{B}^3\right)+\left(3A^2{B}^2+3A{B}^3+B^4\right)$$
109	102 104 87	addassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^4+3A^{3}B+A^{3}B=A^4+3A^{3}B+A^{3}B$$
110	1	oveq1i	$$⊢4A^{3}B=\left(3+1\right)A^{3}B$$
111		ax-1cn	$$⊢1\in ℂ$$
112	111	a1i	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 1\in ℂ$$
113	33 112 87	adddird	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(3+1\right)A^{3}B=3A^{3}B+1A^{3}B$$
114	110 113	syl5eq	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 4A^{3}B=3A^{3}B+1A^{3}B$$
115	87	mulid2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 1A^{3}B=A^{3}B$$
116	115	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^{3}B+1A^{3}B=3A^{3}B+A^{3}B$$
117	114 116	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 4A^{3}B=3A^{3}B+A^{3}B$$
118	117	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^4+4A^{3}B=A^4+3A^{3}B+A^{3}B$$
119	109 118	eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A^4+3A^{3}B+A^{3}B=A^4+4A^{3}B$$
120	90 91 90 97	add4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^2{B}^2+A{B}^3+3A^2{B}^2+\left(3A{B}^3+B^4\right)=3A^2{B}^2+3A^2{B}^2+A{B}^3+\left(3A{B}^3+B^4\right)$$
121		3p3e6	$$⊢3+3=6$$
122	121	oveq1i	$$⊢\left(3+3\right)A^2{B}^2=6A^2{B}^2$$
123	33 33 88	adddird	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(3+3\right)A^2{B}^2=3A^2{B}^2+3A^2{B}^2$$
124	122 123	eqtr3id	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 6A^2{B}^2=3A^2{B}^2+3A^2{B}^2$$
125		3p1e4	$$⊢3+1=4$$
126	13 111 125	addcomli	$$⊢1+3=4$$
127	126	oveq1i	$$⊢\left(1+3\right)A{B}^3=4A{B}^3$$
128	112 33 91	adddird	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+3\right)A{B}^3=1A{B}^3+3A{B}^3$$
129	127 128	eqtr3id	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 4A{B}^3=1A{B}^3+3A{B}^3$$
130	91	mulid2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 1A{B}^3=A{B}^3$$
131	130	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 1A{B}^3+3A{B}^3=A{B}^3+3A{B}^3$$
132	129 131	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 4A{B}^3=A{B}^3+3A{B}^3$$
133	132	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 4A{B}^3+B^4=A{B}^3+3A{B}^3+B^4$$
134	91 93 96	addassd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A{B}^3+3A{B}^3+B^4=A{B}^3+3A{B}^3+B^4$$
135	133 134	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 4A{B}^3+B^4=A{B}^3+3A{B}^3+B^4$$
136	124 135	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 6A^2{B}^2+4A{B}^3+B^4=3A^2{B}^2+3A^2{B}^2+A{B}^3+\left(3A{B}^3+B^4\right)$$
137	120 136	eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 3A^2{B}^2+A{B}^3+3A^2{B}^2+\left(3A{B}^3+B^4\right)=6A^2{B}^2+4A{B}^3+B^4$$
138	119 137	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^4+3A^{3}B\right)+A^{3}B+\left(3A^2{B}^2+A{B}^3\right)+\left(3A^2{B}^2+3A{B}^3+B^4\right)=A^4+4A^{3}B+6A^2{B}^2+\left(4A{B}^3+B^4\right)$$
139	108 138	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^4+3A^{3}B\right)+\left(3A^2{B}^2+A{B}^3\right)+A^{3}B+\left(3A^2{B}^2+3A{B}^3+B^4\right)=A^4+4A^{3}B+6A^2{B}^2+\left(4A{B}^3+B^4\right)$$
140	28 100 139	3eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^3+3A^{2}B+3A{B}^2+B^3\right)\left(A+B\right)=A^4+4A^{3}B+6A^2{B}^2+\left(4A{B}^3+B^4\right)$$
141	7 9 140	3eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A+B\right)}^4=A^4+4A^{3}B+6A^2{B}^2+\left(4A{B}^3+B^4\right)$$