Metamath Proof Explorer


Theorem fsumcube

Description: Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015)

Ref Expression
Assertion fsumcube T 0 k = 0 T k 3 = T 2 T + 1 2 4

Proof

Step Hyp Ref Expression
1 3nn0 3 0
2 fsumkthpow 3 0 T 0 k = 0 T k 3 = 3 + 1 BernPoly T + 1 3 + 1 BernPoly 0 3 + 1
3 1 2 mpan T 0 k = 0 T k 3 = 3 + 1 BernPoly T + 1 3 + 1 BernPoly 0 3 + 1
4 df-4 4 = 3 + 1
5 4 oveq1i 4 BernPoly T + 1 = 3 + 1 BernPoly T + 1
6 4 oveq1i 4 BernPoly 0 = 3 + 1 BernPoly 0
7 5 6 oveq12i 4 BernPoly T + 1 4 BernPoly 0 = 3 + 1 BernPoly T + 1 3 + 1 BernPoly 0
8 7 4 oveq12i 4 BernPoly T + 1 4 BernPoly 0 4 = 3 + 1 BernPoly T + 1 3 + 1 BernPoly 0 3 + 1
9 nn0cn T 0 T
10 peano2cn T T + 1
11 9 10 syl T 0 T + 1
12 bpoly4 T + 1 4 BernPoly T + 1 = T + 1 4 2 T + 1 3 + T + 1 2 - 1 30
13 11 12 syl T 0 4 BernPoly T + 1 = T + 1 4 2 T + 1 3 + T + 1 2 - 1 30
14 4nn 4
15 0exp 4 0 4 = 0
16 14 15 ax-mp 0 4 = 0
17 3nn 3
18 0exp 3 0 3 = 0
19 17 18 ax-mp 0 3 = 0
20 19 oveq2i 2 0 3 = 2 0
21 2t0e0 2 0 = 0
22 20 21 eqtri 2 0 3 = 0
23 16 22 oveq12i 0 4 2 0 3 = 0 0
24 0m0e0 0 0 = 0
25 23 24 eqtri 0 4 2 0 3 = 0
26 sq0 0 2 = 0
27 25 26 oveq12i 0 4 - 2 0 3 + 0 2 = 0 + 0
28 00id 0 + 0 = 0
29 27 28 eqtri 0 4 - 2 0 3 + 0 2 = 0
30 29 oveq1i 0 4 2 0 3 + 0 2 - 1 30 = 0 1 30
31 0cn 0
32 bpoly4 0 4 BernPoly 0 = 0 4 2 0 3 + 0 2 - 1 30
33 31 32 ax-mp 4 BernPoly 0 = 0 4 2 0 3 + 0 2 - 1 30
34 df-neg 1 30 = 0 1 30
35 30 33 34 3eqtr4i 4 BernPoly 0 = 1 30
36 35 a1i T 0 4 BernPoly 0 = 1 30
37 13 36 oveq12d T 0 4 BernPoly T + 1 4 BernPoly 0 = T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 - 1 30
38 4nn0 4 0
39 expcl T + 1 4 0 T + 1 4
40 38 39 mpan2 T + 1 T + 1 4
41 2cn 2
42 expcl T + 1 3 0 T + 1 3
43 1 42 mpan2 T + 1 T + 1 3
44 mulcl 2 T + 1 3 2 T + 1 3
45 41 43 44 sylancr T + 1 2 T + 1 3
46 40 45 subcld T + 1 T + 1 4 2 T + 1 3
47 sqcl T + 1 T + 1 2
48 46 47 addcld T + 1 T + 1 4 - 2 T + 1 3 + T + 1 2
49 10 48 syl T T + 1 4 - 2 T + 1 3 + T + 1 2
50 9 49 syl T 0 T + 1 4 - 2 T + 1 3 + T + 1 2
51 0nn0 0 0
52 1 51 deccl 30 0
53 52 nn0cni 30
54 52 nn0rei 30
55 10pos 0 < 10
56 17 51 51 55 declti 0 < 30
57 54 56 gt0ne0ii 30 0
58 53 57 reccli 1 30
59 subcl T + 1 4 - 2 T + 1 3 + T + 1 2 1 30 T + 1 4 2 T + 1 3 + T + 1 2 - 1 30
60 50 58 59 sylancl T 0 T + 1 4 2 T + 1 3 + T + 1 2 - 1 30
61 subneg T + 1 4 2 T + 1 3 + T + 1 2 - 1 30 1 30 T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 - 1 30 = T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 + 1 30
62 60 58 61 sylancl T 0 T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 - 1 30 = T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 + 1 30
63 npcan T + 1 4 - 2 T + 1 3 + T + 1 2 1 30 T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 + 1 30 = T + 1 4 - 2 T + 1 3 + T + 1 2
64 49 58 63 sylancl T T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 + 1 30 = T + 1 4 - 2 T + 1 3 + T + 1 2
65 9 64 syl T 0 T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 + 1 30 = T + 1 4 - 2 T + 1 3 + T + 1 2
66 2p2e4 2 + 2 = 4
67 66 eqcomi 4 = 2 + 2
68 67 oveq2i T + 1 4 = T + 1 2 + 2
69 df-3 3 = 2 + 1
70 69 oveq2i T + 1 3 = T + 1 2 + 1
71 70 oveq2i 2 T + 1 3 = 2 T + 1 2 + 1
72 68 71 oveq12i T + 1 4 2 T + 1 3 = T + 1 2 + 2 2 T + 1 2 + 1
73 72 oveq1i T + 1 4 - 2 T + 1 3 + T + 1 2 = T + 1 2 + 2 - 2 T + 1 2 + 1 + T + 1 2
74 2nn0 2 0
75 expadd T + 1 2 0 2 0 T + 1 2 + 2 = T + 1 2 T + 1 2
76 74 74 75 mp3an23 T + 1 T + 1 2 + 2 = T + 1 2 T + 1 2
77 1nn0 1 0
78 expadd T + 1 2 0 1 0 T + 1 2 + 1 = T + 1 2 T + 1 1
79 74 77 78 mp3an23 T + 1 T + 1 2 + 1 = T + 1 2 T + 1 1
80 79 oveq2d T + 1 2 T + 1 2 + 1 = 2 T + 1 2 T + 1 1
81 76 80 oveq12d T + 1 T + 1 2 + 2 2 T + 1 2 + 1 = T + 1 2 T + 1 2 2 T + 1 2 T + 1 1
82 10 81 syl T T + 1 2 + 2 2 T + 1 2 + 1 = T + 1 2 T + 1 2 2 T + 1 2 T + 1 1
83 10 sqcld T T + 1 2
84 83 mulid1d T T + 1 2 1 = T + 1 2
85 84 eqcomd T T + 1 2 = T + 1 2 1
86 82 85 oveq12d T T + 1 2 + 2 - 2 T + 1 2 + 1 + T + 1 2 = T + 1 2 T + 1 2 - 2 T + 1 2 T + 1 1 + T + 1 2 1
87 10 exp1d T T + 1 1 = T + 1
88 87 oveq2d T 2 T + 1 1 = 2 T + 1
89 88 oveq2d T T + 1 2 2 T + 1 1 = T + 1 2 2 T + 1
90 89 oveq2d T T + 1 2 T + 1 2 T + 1 2 2 T + 1 1 = T + 1 2 T + 1 2 T + 1 2 2 T + 1
91 87 10 eqeltrd T T + 1 1
92 mul12 2 T + 1 2 T + 1 1 2 T + 1 2 T + 1 1 = T + 1 2 2 T + 1 1
93 41 83 91 92 mp3an2i T 2 T + 1 2 T + 1 1 = T + 1 2 2 T + 1 1
94 93 oveq2d T T + 1 2 T + 1 2 2 T + 1 2 T + 1 1 = T + 1 2 T + 1 2 T + 1 2 2 T + 1 1
95 mulcl 2 T + 1 2 T + 1
96 41 10 95 sylancr T 2 T + 1
97 83 83 96 subdid T T + 1 2 T + 1 2 2 T + 1 = T + 1 2 T + 1 2 T + 1 2 2 T + 1
98 90 94 97 3eqtr4d T T + 1 2 T + 1 2 2 T + 1 2 T + 1 1 = T + 1 2 T + 1 2 2 T + 1
99 98 oveq1d T T + 1 2 T + 1 2 - 2 T + 1 2 T + 1 1 + T + 1 2 1 = T + 1 2 T + 1 2 2 T + 1 + T + 1 2 1
100 83 96 subcld T T + 1 2 2 T + 1
101 ax-1cn 1
102 adddi T + 1 2 T + 1 2 2 T + 1 1 T + 1 2 T + 1 2 - 2 T + 1 + 1 = T + 1 2 T + 1 2 2 T + 1 + T + 1 2 1
103 101 102 mp3an3 T + 1 2 T + 1 2 2 T + 1 T + 1 2 T + 1 2 - 2 T + 1 + 1 = T + 1 2 T + 1 2 2 T + 1 + T + 1 2 1
104 83 100 103 syl2anc T T + 1 2 T + 1 2 - 2 T + 1 + 1 = T + 1 2 T + 1 2 2 T + 1 + T + 1 2 1
105 99 104 eqtr4d T T + 1 2 T + 1 2 - 2 T + 1 2 T + 1 1 + T + 1 2 1 = T + 1 2 T + 1 2 - 2 T + 1 + 1
106 adddi 2 T 1 2 T + 1 = 2 T + 2 1
107 41 101 106 mp3an13 T 2 T + 1 = 2 T + 2 1
108 2t1e2 2 1 = 2
109 108 oveq2i 2 T + 2 1 = 2 T + 2
110 107 109 syl6eq T 2 T + 1 = 2 T + 2
111 110 oveq1d T 2 T + 1 1 = 2 T + 2 - 1
112 mulcl 2 T 2 T
113 41 112 mpan T 2 T
114 addsubass 2 T 2 1 2 T + 2 - 1 = 2 T + 2 - 1
115 41 101 114 mp3an23 2 T 2 T + 2 - 1 = 2 T + 2 - 1
116 113 115 syl T 2 T + 2 - 1 = 2 T + 2 - 1
117 2m1e1 2 1 = 1
118 117 oveq2i 2 T + 2 - 1 = 2 T + 1
119 116 118 syl6eq T 2 T + 2 - 1 = 2 T + 1
120 111 119 eqtrd T 2 T + 1 1 = 2 T + 1
121 120 oveq2d T T + 1 2 2 T + 1 1 = T + 1 2 2 T + 1
122 subsub T + 1 2 2 T + 1 1 T + 1 2 2 T + 1 1 = T + 1 2 - 2 T + 1 + 1
123 101 122 mp3an3 T + 1 2 2 T + 1 T + 1 2 2 T + 1 1 = T + 1 2 - 2 T + 1 + 1
124 83 96 123 syl2anc T T + 1 2 2 T + 1 1 = T + 1 2 - 2 T + 1 + 1
125 sqcl T T 2
126 peano2cn 2 T 2 T + 1
127 113 126 syl T 2 T + 1
128 binom21 T T + 1 2 = T 2 + 2 T + 1
129 addass T 2 2 T 1 T 2 + 2 T + 1 = T 2 + 2 T + 1
130 101 129 mp3an3 T 2 2 T T 2 + 2 T + 1 = T 2 + 2 T + 1
131 125 113 130 syl2anc T T 2 + 2 T + 1 = T 2 + 2 T + 1
132 128 131 eqtrd T T + 1 2 = T 2 + 2 T + 1
133 125 127 132 mvrraddd T T + 1 2 2 T + 1 = T 2
134 121 124 133 3eqtr3d T T + 1 2 - 2 T + 1 + 1 = T 2
135 134 oveq2d T T + 1 2 T + 1 2 - 2 T + 1 + 1 = T + 1 2 T 2
136 83 125 mulcomd T T + 1 2 T 2 = T 2 T + 1 2
137 105 135 136 3eqtrd T T + 1 2 T + 1 2 - 2 T + 1 2 T + 1 1 + T + 1 2 1 = T 2 T + 1 2
138 86 137 eqtrd T T + 1 2 + 2 - 2 T + 1 2 + 1 + T + 1 2 = T 2 T + 1 2
139 9 138 syl T 0 T + 1 2 + 2 - 2 T + 1 2 + 1 + T + 1 2 = T 2 T + 1 2
140 73 139 syl5eq T 0 T + 1 4 - 2 T + 1 3 + T + 1 2 = T 2 T + 1 2
141 65 140 eqtrd T 0 T + 1 4 - 2 T + 1 3 + T + 1 2 - 1 30 + 1 30 = T 2 T + 1 2
142 37 62 141 3eqtrd T 0 4 BernPoly T + 1 4 BernPoly 0 = T 2 T + 1 2
143 142 oveq1d T 0 4 BernPoly T + 1 4 BernPoly 0 4 = T 2 T + 1 2 4
144 8 143 syl5eqr T 0 3 + 1 BernPoly T + 1 3 + 1 BernPoly 0 3 + 1 = T 2 T + 1 2 4
145 3 144 eqtrd T 0 k = 0 T k 3 = T 2 T + 1 2 4