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	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 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	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑ 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	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ↑ 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	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) = ( ( 2 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) + ( 1 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) )
86	62	mullidd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 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	mullidd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 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 ) ) ) )