Metamath Proof Explorer

Theorem binom3

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

Ref Expression
Assertion 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 ) ) ) )

Proof

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