Metamath Proof Explorer


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 A B A + B 4 = A 4 + 4 A 3 B + 6 A 2 B 2 + 4 A B 3 + B 4

Proof

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