Metamath Proof Explorer

Theorem cu3addd

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

Ref Expression
Hypotheses cu3addd.1 
|- ( ph -> A e. CC )
cu3addd.2 
|- ( ph -> B e. CC )
cu3addd.3 
|- ( ph -> C e. CC )
Assertion cu3addd 
|- ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( ( 3 x. ( A x. ( C ^ 2 ) ) ) + ( 3 x. ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 cu3addd.1 
 |-  ( ph -> A e. CC )
2 cu3addd.2 
 |-  ( ph -> B e. CC )
3 cu3addd.3 
 |-  ( ph -> C e. CC )
4 1 2 addcld 
 |-  ( ph -> ( A + B ) e. CC )
5 4 3 jca 
 |-  ( ph -> ( ( A + B ) e. CC /\ C e. CC ) )
6 binom3 
 |-  ( ( ( A + B ) e. CC /\ C e. CC ) -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( A + B ) ^ 3 ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
7 6 a1i 
 |-  ( ph -> ( ( ( A + B ) e. CC /\ C e. CC ) -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( A + B ) ^ 3 ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) ) )
8 5 7 mpd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( A + B ) ^ 3 ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
9 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 ) ) ) )
10 1 2 9 syl2anc 
 |-  ( ph -> ( ( A + B ) ^ 3 ) = ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) )
11 10 oveq1d 
 |-  ( ph -> ( ( ( A + B ) ^ 3 ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) )
12 11 oveq1d 
 |-  ( ph -> ( ( ( ( A + B ) ^ 3 ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
13 8 12 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
14 1 2 binom2d 
 |-  ( ph -> ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
15 14 oveq1d 
 |-  ( ph -> ( ( ( A + B ) ^ 2 ) x. C ) = ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) )
16 15 oveq2d 
 |-  ( ph -> ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) = ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) ) )
17 16 oveq2d 
 |-  ( ph -> ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) ) ) )
18 17 oveq1d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( A + B ) ^ 2 ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
19 13 18 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
20 1 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
21 2cnd 
 |-  ( ph -> 2 e. CC )
22 1 2 mulcld 
 |-  ( ph -> ( A x. B ) e. CC )
23 21 22 mulcld 
 |-  ( ph -> ( 2 x. ( A x. B ) ) e. CC )
24 20 23 addcld 
 |-  ( ph -> ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) e. CC )
25 2 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
26 24 25 3 adddird 
 |-  ( ph -> ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) = ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) )
27 26 oveq2d 
 |-  ( ph -> ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) ) = ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) ) )
28 27 oveq2d 
 |-  ( ph -> ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) ) ) )
29 28 oveq1d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) x. C ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
30 19 29 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
31 20 23 3 adddird 
 |-  ( ph -> ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) = ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) )
32 31 oveq1d 
 |-  ( ph -> ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) = ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) )
33 32 oveq2d 
 |-  ( ph -> ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) ) = ( 3 x. ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) ) )
34 33 oveq2d 
 |-  ( ph -> ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) ) ) )
35 34 oveq1d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) x. C ) + ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
36 30 35 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
37 3cn 
 |-  3 e. CC
38 37 a1i 
 |-  ( ph -> 3 e. CC )
39 20 3 mulcld 
 |-  ( ph -> ( ( A ^ 2 ) x. C ) e. CC )
40 23 3 mulcld 
 |-  ( ph -> ( ( 2 x. ( A x. B ) ) x. C ) e. CC )
41 39 40 addcld 
 |-  ( ph -> ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) e. CC )
42 25 3 mulcld 
 |-  ( ph -> ( ( B ^ 2 ) x. C ) e. CC )
43 38 41 42 adddid 
 |-  ( ph -> ( 3 x. ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) ) = ( ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) )
44 43 oveq2d 
 |-  ( ph -> ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) )
45 44 oveq1d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( 3 x. ( ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) + ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
46 36 45 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
47 38 39 40 adddid 
 |-  ( ph -> ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) = ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) )
48 47 oveq1d 
 |-  ( ph -> ( ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) = ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) )
49 48 oveq2d 
 |-  ( ph -> ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) )
50 49 oveq1d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( 3 x. ( ( ( A ^ 2 ) x. C ) + ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
51 46 50 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
52 38 21 22 mulassd 
 |-  ( ph -> ( ( 3 x. 2 ) x. ( A x. B ) ) = ( 3 x. ( 2 x. ( A x. B ) ) ) )
53 52 oveq1d 
 |-  ( ph -> ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) = ( ( 3 x. ( 2 x. ( A x. B ) ) ) x. C ) )
54 38 23 3 mulassd 
 |-  ( ph -> ( ( 3 x. ( 2 x. ( A x. B ) ) ) x. C ) = ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) )
55 53 54 eqtrd 
 |-  ( ph -> ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) = ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) )
56 55 oveq2d 
 |-  ( ph -> ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) = ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) )
57 56 oveq1d 
 |-  ( ph -> ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) = ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) )
58 57 oveq2d 
 |-  ( ph -> ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) )
59 58 eqcomd 
 |-  ( ph -> ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) = ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) )
60 59 oveq1d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( 3 x. ( ( 2 x. ( A x. B ) ) x. C ) ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
61 51 60 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) )
62 3 sqcld 
 |-  ( ph -> ( C ^ 2 ) e. CC )
63 1 2 62 adddird 
 |-  ( ph -> ( ( A + B ) x. ( C ^ 2 ) ) = ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) )
64 63 oveq2d 
 |-  ( ph -> ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) = ( 3 x. ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) ) )
65 64 oveq1d 
 |-  ( ph -> ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) = ( ( 3 x. ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) )
66 65 oveq2d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A + B ) x. ( C ^ 2 ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) ) )
67 61 66 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) ) )
68 1 62 mulcld 
 |-  ( ph -> ( A x. ( C ^ 2 ) ) e. CC )
69 2 62 mulcld 
 |-  ( ph -> ( B x. ( C ^ 2 ) ) e. CC )
70 38 68 69 adddid 
 |-  ( ph -> ( 3 x. ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) ) = ( ( 3 x. ( A x. ( C ^ 2 ) ) ) + ( 3 x. ( B x. ( C ^ 2 ) ) ) ) )
71 70 oveq1d 
 |-  ( ph -> ( ( 3 x. ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) = ( ( ( 3 x. ( A x. ( C ^ 2 ) ) ) + ( 3 x. ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) )
72 71 oveq2d 
 |-  ( ph -> ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( 3 x. ( ( A x. ( C ^ 2 ) ) + ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( ( 3 x. ( A x. ( C ^ 2 ) ) ) + ( 3 x. ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) ) )
73 67 72 eqtrd 
 |-  ( ph -> ( ( ( A + B ) + C ) ^ 3 ) = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) ) + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) ) + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) ) + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) ) + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( ( 3 x. ( A x. ( C ^ 2 ) ) ) + ( 3 x. ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) ) )