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