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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 4 ) = ( ( ( 𝐴 ↑ 4 ) + ( 4 · ( ( 𝐴 ↑ 3 ) · 𝐵 ) ) ) + ( ( 6 · ( ( 𝐴 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) + ( ( 4 · ( 𝐴 · ( 𝐵 ↑ 3 ) ) ) + ( 𝐵 ↑ 4 ) ) ) ) )

Proof

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