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 eqtrid
 |-  ( ( 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 eqtrid
 |-  ( ( 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 eqtrid
 |-  ( ( 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 eqtrid
 |-  ( ( 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 ) ) ) )