Metamath Proof Explorer

Theorem cu3addd

Description: Cube of sum of three numbers. (Contributed by Igor Ieskov, 14-Dec-2023)

Ref Expression
Hypotheses cu3addd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
cu3addd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
cu3addd.3 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion cu3addd ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( ( 3 · ( 𝐴 · ( 𝐶 ↑ 2 ) ) ) + ( 3 · ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 cu3addd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 cu3addd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 cu3addd.3 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 1 2 addcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
5 4 3 jca ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
6 binom3 ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( 𝐴 + 𝐵 ) ↑ 3 ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
7 6 a1i ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( 𝐴 + 𝐵 ) ↑ 3 ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) ) )
8 5 7 mpd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( 𝐴 + 𝐵 ) ↑ 3 ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
9 binom3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 3 ) = ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )
10 1 2 9 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑ 3 ) = ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) )
11 10 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ↑ 3 ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) )
12 11 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐴 + 𝐵 ) ↑ 3 ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
13 8 12 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
14 1 2 binom2d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) )
15 14 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) )
16 15 oveq2d ⊢ ( 𝜑 → ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) = ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) )
17 16 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) ) )
18 17 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
19 13 18 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
20 1 sqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
21 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
22 1 2 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
23 21 22 mulcld ⊢ ( 𝜑 → ( 2 · ( 𝐴 · 𝐵 ) ) ∈ ℂ )
24 20 23 addcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) ∈ ℂ )
25 2 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
26 24 25 3 adddird ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
27 26 oveq2d ⊢ ( 𝜑 → ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) = ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) )
28 27 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) )
29 28 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) + ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
30 19 29 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
31 20 23 3 adddird ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) = ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) )
32 31 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) = ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) )
33 32 oveq2d ⊢ ( 𝜑 → ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) = ( 3 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) )
34 33 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) )
35 34 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) + ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
36 30 35 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
37 3cn ⊢ 3 ∈ ℂ
38 37 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
39 20 3 mulcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · 𝐶 ) ∈ ℂ )
40 23 3 mulcld ⊢ ( 𝜑 → ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ∈ ℂ )
41 39 40 addcld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ∈ ℂ )
42 25 3 mulcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) · 𝐶 ) ∈ ℂ )
43 38 41 42 adddid ⊢ ( 𝜑 → ( 3 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) = ( ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) )
44 43 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) )
45 44 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( 3 · ( ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
46 36 45 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
47 38 39 40 adddid ⊢ ( 𝜑 → ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) = ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) )
48 47 oveq1d ⊢ ( 𝜑 → ( ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) = ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) )
49 48 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) )
50 49 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( 3 · ( ( ( 𝐴 ↑ 2 ) · 𝐶 ) + ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
51 46 50 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
52 38 21 22 mulassd ⊢ ( 𝜑 → ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) = ( 3 · ( 2 · ( 𝐴 · 𝐵 ) ) ) )
53 52 oveq1d ⊢ ( 𝜑 → ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) = ( ( 3 · ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) )
54 38 23 3 mulassd ⊢ ( 𝜑 → ( ( 3 · ( 2 · ( 𝐴 · 𝐵 ) ) ) · 𝐶 ) = ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) )
55 53 54 eqtrd ⊢ ( 𝜑 → ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) = ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) )
56 55 oveq2d ⊢ ( 𝜑 → ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) = ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) )
57 56 oveq1d ⊢ ( 𝜑 → ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) = ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) )
58 57 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) )
59 58 eqcomd ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) = ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) )
60 59 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( 3 · ( ( 2 · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
61 51 60 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
62 3 sqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
63 1 2 62 adddird ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) = ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) )
64 63 oveq2d ⊢ ( 𝜑 → ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) = ( 3 · ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) )
65 64 oveq1d ⊢ ( 𝜑 → ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) = ( ( 3 · ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) )
66 65 oveq2d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 + 𝐵 ) · ( 𝐶 ↑ 2 ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
67 61 66 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
68 1 62 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
69 2 62 mulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
70 38 68 69 adddid ⊢ ( 𝜑 → ( 3 · ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) = ( ( 3 · ( 𝐴 · ( 𝐶 ↑ 2 ) ) ) + ( 3 · ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) )
71 70 oveq1d ⊢ ( 𝜑 → ( ( 3 · ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) = ( ( ( 3 · ( 𝐴 · ( 𝐶 ↑ 2 ) ) ) + ( 3 · ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) )
72 71 oveq2d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( 3 · ( ( 𝐴 · ( 𝐶 ↑ 2 ) ) + ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( ( 3 · ( 𝐴 · ( 𝐶 ↑ 2 ) ) ) + ( 3 · ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) ) )
73 67 72 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) ↑ 3 ) = ( ( ( ( ( 𝐴 ↑ 3 ) + ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐵 ) ) ) + ( ( 3 · ( 𝐴 · ( 𝐵 ↑ 2 ) ) ) + ( 𝐵 ↑ 3 ) ) ) + ( ( ( 3 · ( ( 𝐴 ↑ 2 ) · 𝐶 ) ) + ( ( ( 3 · 2 ) · ( 𝐴 · 𝐵 ) ) · 𝐶 ) ) + ( 3 · ( ( 𝐵 ↑ 2 ) · 𝐶 ) ) ) ) + ( ( ( 3 · ( 𝐴 · ( 𝐶 ↑ 2 ) ) ) + ( 3 · ( 𝐵 · ( 𝐶 ↑ 2 ) ) ) ) + ( 𝐶 ↑ 3 ) ) ) )