Metamath Proof Explorer

Theorem binom3

Description: The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015)

Ref Expression
Assertion binom3 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 3 ) = ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-3 ⊢ 3 = ( 2 + 1 )
2 1 oveq2i ⊢ ( ( 𝐴 + 𝐵 ) ↑ 3 ) = ( ( 𝐴 + 𝐵 ) ↑ ( 2 + 1 ) )
3 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
4 2nn0 ⊢ 2 ∈ ℕ0
5 expp1 ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑ ( 2 + 1 ) ) = ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · ( 𝐴 + 𝐵 ) ) )
6 3 4 5 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ ( 2 + 1 ) ) = ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · ( 𝐴 + 𝐵 ) ) )
7 2 6 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 3 ) = ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · ( 𝐴 + 𝐵 ) ) )
8 sqcl ⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( ( 𝐴 + 𝐵 ) ↑ 2 ) ∈ ℂ )
9 3 8 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) ∈ ℂ )
10 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
11 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
12 9 10 11 adddid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐴 ) + ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐵 ) ) )
13 binom2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
14 13 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐴 ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐴 ) )
15 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
16 10 15 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
17 2cn ⊢ 2 ∈ ℂ
18 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
19 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝐴 · 𝐵 ) ∈ ℂ ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
20 17 18 19 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
21 16 20 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) ∈ ℂ )
22 sqcl ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 2 ) ∈ ℂ )
23 11 22 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
24 21 23 10 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐴 ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐴 ) + ( ( 𝐵 ↑ 2 ) · 𝐴 ) ) )
25 16 20 10 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐴 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐴 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐴 ) ) )
26 1 oveq2i ⊢ ( 𝐴 ↑ 3 ) = ( 𝐴 ↑ ( 2 + 1 ) )
27 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝐴 ↑ ( 2 + 1 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
28 10 4 27 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ ( 2 + 1 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
29 26 28 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 3 ) = ( ( 𝐴 ↑ 2 ) · 𝐴 ) )
30 sqval ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
31 10 30 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
32 31 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · 𝐵 ) = ( ( 𝐴 · 𝐴 ) · 𝐵 ) )
33 10 10 11 mul32d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐴 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) · 𝐴 ) )
34 32 33 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) · 𝐴 ) )
35 34 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( 2 · ( ( 𝐴 · 𝐵 ) · 𝐴 ) ) )
36 2cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 2 ∈ ℂ )
37 36 18 10 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐴 ) = ( 2 · ( ( 𝐴 · 𝐵 ) · 𝐴 ) ) )
38 35 37 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐴 ) )
39 29 38 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐴 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐴 ) ) )
40 25 39 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐴 ) = ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) )
41 23 10 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐵 ↑ 2 ) · 𝐴 ) = ( 𝐴 · ( 𝐵 ↑ 2 ) ) )
42 40 41 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐴 ) + ( ( 𝐵 ↑ 2 ) · 𝐴 ) ) = ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) )
43 14 24 42 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐴 ) = ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) )
44 13 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐵 ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐵 ) )
45 21 23 11 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐵 ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐵 ) + ( ( 𝐵 ↑ 2 ) · 𝐵 ) ) )
46 sqval ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
47 11 46 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 ) )
48 47 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 𝐵 ↑ 2 ) ) = ( 𝐴 · ( 𝐵 · 𝐵 ) ) )
49 10 11 11 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · 𝐵 ) = ( 𝐴 · ( 𝐵 · 𝐵 ) ) )
50 48 49 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 · 𝐵 ) · 𝐵 ) )
51 50 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) = ( 2 · ( ( 𝐴 · 𝐵 ) · 𝐵 ) ) )
52 36 18 11 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐵 ) = ( 2 · ( ( 𝐴 · 𝐵 ) · 𝐵 ) ) )
53 51 52 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) = ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐵 ) )
54 53 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐵 ) ) )
55 16 20 11 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐵 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐵 ) ) )
56 54 55 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐵 ) )
57 1 oveq2i ⊢ ( 𝐵 ↑ 3 ) = ( 𝐵 ↑ ( 2 + 1 ) )
58 expp1 ⊢ ( ( 𝐵 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 𝐵 ↑ ( 2 + 1 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐵 ) )
59 11 4 58 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ ( 2 + 1 ) ) = ( ( 𝐵 ↑ 2 ) · 𝐵 ) )
60 57 59 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 3 ) = ( ( 𝐵 ↑ 2 ) · 𝐵 ) )
61 56 60 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) + ( 𝐵 ↑ 3 ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐵 ) + ( ( 𝐵 ↑ 2 ) · 𝐵 ) ) )
62 16 11 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · 𝐵 ) ∈ ℂ )
63 10 23 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
64 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝐴 · ( 𝐵 ↑ 2 ) ) ∈ ℂ ) → ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ∈ ℂ )
65 17 63 64 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ∈ ℂ )
66 3nn0 ⊢ 3 ∈ ℕ0
67 expcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐵 ↑ 3 ) ∈ ℂ )
68 11 66 67 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 3 ) ∈ ℂ )
69 62 65 68 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) + ( 𝐵 ↑ 3 ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )
70 61 69 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐵 ) + ( ( 𝐵 ↑ 2 ) · 𝐵 ) ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )
71 44 45 70 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐵 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )
72 43 71 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐴 ) + ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐵 ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) ) )
73 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
74 10 66 73 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
75 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) · 𝐵 ) ∈ ℂ ) → ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ∈ ℂ )
76 17 62 75 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ∈ ℂ )
77 74 76 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) ∈ ℂ )
78 65 68 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ∈ ℂ )
79 77 63 62 78 add4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) ) )
80 12 72 79 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) ) )
81 74 76 62 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 𝐴 ↑ 3 ) + ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) )
82 1 oveq1i ⊢ ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 2 + 1 ) · ( ( 𝐴 ↑ 2 ) · 𝐵 ) )
83 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 1 ∈ ℂ )
84 36 83 62 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 + 1 ) · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( 1 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) )
85 82 84 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( 1 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) )
86 62 mulid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 𝐴 ↑ 2 ) · 𝐵 ) )
87 86 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( 1 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) = ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) )
88 85 87 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) )
89 88 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) = ( ( 𝐴 ↑ 3 ) + ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) )
90 81 89 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) )
91 1p2e3 ⊢ ( 1 + 2 ) = 3
92 91 oveq1i ⊢ ( ( 1 + 2 ) · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) = ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) )
93 83 36 63 adddird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 1 + 2 ) · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) = ( ( 1 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) )
94 92 93 eqtr3id ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) = ( ( 1 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) )
95 63 mulid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) = ( 𝐴 · ( 𝐵 ↑ 2 ) ) )
96 95 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 1 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) = ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) )
97 94 96 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) )
98 97 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) = ( ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) + ( 𝐵 ↑ 3 ) ) )
99 63 65 68 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) ) + ( 𝐵 ↑ 3 ) ) = ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )
100 98 99 eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) = ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) )
101 90 100 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 3 ) + ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( ( 𝐴 · ( 𝐵 ↑ 2 ) ) + ( ( 2 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) ) = ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )
102 7 80 101 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 3 ) = ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )