Metamath Proof Explorer


Theorem sumcubes

Description: The sum of the first N perfect cubes is the sum of the first N nonnegative integers, squared. This is the Proof by Nicomachus from https://proofwiki.org/wiki/Sum_of_Sequence_of_Cubes using induction and index shifting to collect all the odd numbers. (Contributed by SN, 22-Mar-2025)

Ref Expression
Assertion sumcubes N 0 k = 1 N k 3 = k = 1 N k 2

Proof

Step Hyp Ref Expression
1 oveq2 x = 0 1 x = 1 0
2 1 sumeq1d x = 0 k = 1 x l = 1 k k 2 k + 2 l - 1 = k = 1 0 l = 1 k k 2 k + 2 l - 1
3 1 sumeq1d x = 0 k = 1 x k = k = 1 0 k
4 3 oveq2d x = 0 1 k = 1 x k = 1 k = 1 0 k
5 4 sumeq1d x = 0 m = 1 k = 1 x k 2 m 1 = m = 1 k = 1 0 k 2 m 1
6 2 5 eqeq12d x = 0 k = 1 x l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 x k 2 m 1 k = 1 0 l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 0 k 2 m 1
7 oveq2 x = y 1 x = 1 y
8 7 sumeq1d x = y k = 1 x l = 1 k k 2 k + 2 l - 1 = k = 1 y l = 1 k k 2 k + 2 l - 1
9 7 sumeq1d x = y k = 1 x k = k = 1 y k
10 9 oveq2d x = y 1 k = 1 x k = 1 k = 1 y k
11 10 sumeq1d x = y m = 1 k = 1 x k 2 m 1 = m = 1 k = 1 y k 2 m 1
12 8 11 eqeq12d x = y k = 1 x l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 x k 2 m 1 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1
13 oveq2 x = y + 1 1 x = 1 y + 1
14 13 sumeq1d x = y + 1 k = 1 x l = 1 k k 2 k + 2 l - 1 = k = 1 y + 1 l = 1 k k 2 k + 2 l - 1
15 13 sumeq1d x = y + 1 k = 1 x k = k = 1 y + 1 k
16 15 oveq2d x = y + 1 1 k = 1 x k = 1 k = 1 y + 1 k
17 16 sumeq1d x = y + 1 m = 1 k = 1 x k 2 m 1 = m = 1 k = 1 y + 1 k 2 m 1
18 14 17 eqeq12d x = y + 1 k = 1 x l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 x k 2 m 1 k = 1 y + 1 l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y + 1 k 2 m 1
19 oveq2 x = N 1 x = 1 N
20 19 sumeq1d x = N k = 1 x l = 1 k k 2 k + 2 l - 1 = k = 1 N l = 1 k k 2 k + 2 l - 1
21 19 sumeq1d x = N k = 1 x k = k = 1 N k
22 21 oveq2d x = N 1 k = 1 x k = 1 k = 1 N k
23 22 sumeq1d x = N m = 1 k = 1 x k 2 m 1 = m = 1 k = 1 N k 2 m 1
24 20 23 eqeq12d x = N k = 1 x l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 x k 2 m 1 k = 1 N l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 N k 2 m 1
25 sum0 k l = 1 k k 2 k + 2 l - 1 = 0
26 sum0 m 2 m 1 = 0
27 25 26 eqtr4i k l = 1 k k 2 k + 2 l - 1 = m 2 m 1
28 fz10 1 0 =
29 28 sumeq1i k = 1 0 l = 1 k k 2 k + 2 l - 1 = k l = 1 k k 2 k + 2 l - 1
30 28 sumeq1i k = 1 0 k = k k
31 sum0 k k = 0
32 30 31 eqtri k = 1 0 k = 0
33 32 oveq2i 1 k = 1 0 k = 1 0
34 33 28 eqtri 1 k = 1 0 k =
35 34 sumeq1i m = 1 k = 1 0 k 2 m 1 = m 2 m 1
36 27 29 35 3eqtr4i k = 1 0 l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 0 k 2 m 1
37 simpr y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1
38 fzfid y 0 1 y Fin
39 elfznn k 1 y k
40 39 adantl y 0 k 1 y k
41 40 nnnn0d y 0 k 1 y k 0
42 38 41 fsumnn0cl y 0 k = 1 y k 0
43 42 nn0zd y 0 k = 1 y k
44 nn0p1nn k = 1 y k 0 k = 1 y k + 1
45 42 44 syl y 0 k = 1 y k + 1
46 45 nnzd y 0 k = 1 y k + 1
47 peano2nn0 y 0 y + 1 0
48 47 nn0zd y 0 y + 1
49 43 48 zaddcld y 0 k = 1 y k + y + 1
50 2cnd y 0 m k = 1 y k + 1 k = 1 y k + y + 1 2
51 elfzelz m k = 1 y k + 1 k = 1 y k + y + 1 m
52 51 zcnd m k = 1 y k + 1 k = 1 y k + y + 1 m
53 52 adantl y 0 m k = 1 y k + 1 k = 1 y k + y + 1 m
54 50 53 mulcld y 0 m k = 1 y k + 1 k = 1 y k + y + 1 2 m
55 1cnd y 0 m k = 1 y k + 1 k = 1 y k + y + 1 1
56 54 55 subcld y 0 m k = 1 y k + 1 k = 1 y k + y + 1 2 m 1
57 oveq2 m = l + k = 1 y k 2 m = 2 l + k = 1 y k
58 57 oveq1d m = l + k = 1 y k 2 m 1 = 2 l + k = 1 y k 1
59 43 46 49 56 58 fsumshftm y 0 m = k = 1 y k + 1 k = 1 y k + y + 1 2 m 1 = l = k = 1 y k + 1 - k = 1 y k k = 1 y k + y + 1 - k = 1 y k 2 l + k = 1 y k 1
60 elfzelz k 1 y k
61 60 adantl y 0 k 1 y k
62 61 zred y 0 k 1 y k
63 38 62 fsumrecl y 0 k = 1 y k
64 63 recnd y 0 k = 1 y k
65 1cnd y 0 1
66 64 65 pncan2d y 0 k = 1 y k + 1 - k = 1 y k = 1
67 47 nn0cnd y 0 y + 1
68 64 67 pncan2d y 0 k = 1 y k + y + 1 - k = 1 y k = y + 1
69 66 68 oveq12d y 0 k = 1 y k + 1 - k = 1 y k k = 1 y k + y + 1 - k = 1 y k = 1 y + 1
70 elfzelz l k = 1 y k + 1 - k = 1 y k k = 1 y k + y + 1 - k = 1 y k l
71 70 zcnd l k = 1 y k + 1 - k = 1 y k k = 1 y k + y + 1 - k = 1 y k l
72 2cnd y 0 l 2
73 simpr y 0 l l
74 64 adantr y 0 l k = 1 y k
75 72 73 74 adddid y 0 l 2 l + k = 1 y k = 2 l + 2 k = 1 y k
76 75 oveq1d y 0 l 2 l + k = 1 y k 1 = 2 l + 2 k = 1 y k - 1
77 72 73 mulcld y 0 l 2 l
78 72 74 mulcld y 0 l 2 k = 1 y k
79 1cnd y 0 l 1
80 77 78 79 addsubassd y 0 l 2 l + 2 k = 1 y k - 1 = 2 l + 2 k = 1 y k - 1
81 77 78 79 addsub12d y 0 l 2 l + 2 k = 1 y k - 1 = 2 k = 1 y k + 2 l - 1
82 arisum y 0 k = 1 y k = y 2 + y 2
83 82 oveq2d y 0 2 k = 1 y k = 2 y 2 + y 2
84 nn0cn y 0 y
85 84 sqcld y 0 y 2
86 85 84 addcld y 0 y 2 + y
87 2cnd y 0 2
88 2ne0 2 0
89 88 a1i y 0 2 0
90 86 87 89 divcan2d y 0 2 y 2 + y 2 = y 2 + y
91 binom21 y y + 1 2 = y 2 + 2 y + 1
92 84 91 syl y 0 y + 1 2 = y 2 + 2 y + 1
93 92 oveq1d y 0 y + 1 2 y + 1 = y 2 + 2 y + 1 - y + 1
94 87 84 mulcld y 0 2 y
95 85 94 addcld y 0 y 2 + 2 y
96 95 84 65 pnpcan2d y 0 y 2 + 2 y + 1 - y + 1 = y 2 + 2 y - y
97 85 94 84 addsubassd y 0 y 2 + 2 y - y = y 2 + 2 y - y
98 84 2timesd y 0 2 y = y + y
99 84 84 98 mvrladdd y 0 2 y y = y
100 99 oveq2d y 0 y 2 + 2 y - y = y 2 + y
101 97 100 eqtrd y 0 y 2 + 2 y - y = y 2 + y
102 93 96 101 3eqtrrd y 0 y 2 + y = y + 1 2 y + 1
103 83 90 102 3eqtrd y 0 2 k = 1 y k = y + 1 2 y + 1
104 103 adantr y 0 l 2 k = 1 y k = y + 1 2 y + 1
105 104 oveq1d y 0 l 2 k = 1 y k + 2 l - 1 = y + 1 2 y + 1 + 2 l - 1
106 81 105 eqtrd y 0 l 2 l + 2 k = 1 y k - 1 = y + 1 2 y + 1 + 2 l - 1
107 76 80 106 3eqtrd y 0 l 2 l + k = 1 y k 1 = y + 1 2 y + 1 + 2 l - 1
108 71 107 sylan2 y 0 l k = 1 y k + 1 - k = 1 y k k = 1 y k + y + 1 - k = 1 y k 2 l + k = 1 y k 1 = y + 1 2 y + 1 + 2 l - 1
109 69 108 sumeq12dv y 0 l = k = 1 y k + 1 - k = 1 y k k = 1 y k + y + 1 - k = 1 y k 2 l + k = 1 y k 1 = l = 1 y + 1 y + 1 2 y + 1 + 2 l - 1
110 59 109 eqtr2d y 0 l = 1 y + 1 y + 1 2 y + 1 + 2 l - 1 = m = k = 1 y k + 1 k = 1 y k + y + 1 2 m 1
111 110 adantr y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 l = 1 y + 1 y + 1 2 y + 1 + 2 l - 1 = m = k = 1 y k + 1 k = 1 y k + y + 1 2 m 1
112 37 111 oveq12d y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 k = 1 y l = 1 k k 2 k + 2 l - 1 + l = 1 y + 1 y + 1 2 y + 1 + 2 l - 1 = m = 1 k = 1 y k 2 m 1 + m = k = 1 y k + 1 k = 1 y k + y + 1 2 m 1
113 id y 0 y 0
114 fzfid y 0 k 1 y + 1 1 k Fin
115 elfzelz k 1 y + 1 k
116 115 zcnd k 1 y + 1 k
117 116 sqcld k 1 y + 1 k 2
118 117 116 subcld k 1 y + 1 k 2 k
119 2cnd l 1 k 2
120 elfzelz l 1 k l
121 120 zcnd l 1 k l
122 119 121 mulcld l 1 k 2 l
123 1cnd l 1 k 1
124 122 123 subcld l 1 k 2 l 1
125 addcl k 2 k 2 l 1 k 2 k + 2 l - 1
126 118 124 125 syl2an k 1 y + 1 l 1 k k 2 k + 2 l - 1
127 126 adantll y 0 k 1 y + 1 l 1 k k 2 k + 2 l - 1
128 114 127 fsumcl y 0 k 1 y + 1 l = 1 k k 2 k + 2 l - 1
129 oveq2 k = y + 1 1 k = 1 y + 1
130 oveq1 k = y + 1 k 2 = y + 1 2
131 id k = y + 1 k = y + 1
132 130 131 oveq12d k = y + 1 k 2 k = y + 1 2 y + 1
133 132 oveq1d k = y + 1 k 2 k + 2 l - 1 = y + 1 2 y + 1 + 2 l - 1
134 133 adantr k = y + 1 l 1 k k 2 k + 2 l - 1 = y + 1 2 y + 1 + 2 l - 1
135 129 134 sumeq12dv k = y + 1 l = 1 k k 2 k + 2 l - 1 = l = 1 y + 1 y + 1 2 y + 1 + 2 l - 1
136 113 128 135 fz1sump1 y 0 k = 1 y + 1 l = 1 k k 2 k + 2 l - 1 = k = 1 y l = 1 k k 2 k + 2 l - 1 + l = 1 y + 1 y + 1 2 y + 1 + 2 l - 1
137 136 adantr y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 k = 1 y + 1 l = 1 k k 2 k + 2 l - 1 = k = 1 y l = 1 k k 2 k + 2 l - 1 + l = 1 y + 1 y + 1 2 y + 1 + 2 l - 1
138 116 adantl y 0 k 1 y + 1 k
139 113 138 131 fz1sump1 y 0 k = 1 y + 1 k = k = 1 y k + y + 1
140 139 adantr y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 k = 1 y + 1 k = k = 1 y k + y + 1
141 140 oveq2d y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 1 k = 1 y + 1 k = 1 k = 1 y k + y + 1
142 141 sumeq1d y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 m = 1 k = 1 y + 1 k 2 m 1 = m = 1 k = 1 y k + y + 1 2 m 1
143 63 ltp1d y 0 k = 1 y k < k = 1 y k + 1
144 fzdisj k = 1 y k < k = 1 y k + 1 1 k = 1 y k k = 1 y k + 1 k = 1 y k + y + 1 =
145 143 144 syl y 0 1 k = 1 y k k = 1 y k + 1 k = 1 y k + y + 1 =
146 nnuz = 1
147 45 146 eleqtrdi y 0 k = 1 y k + 1 1
148 43 uzidd y 0 k = 1 y k k = 1 y k
149 uzaddcl k = 1 y k k = 1 y k y + 1 0 k = 1 y k + y + 1 k = 1 y k
150 148 47 149 syl2anc y 0 k = 1 y k + y + 1 k = 1 y k
151 fzsplit2 k = 1 y k + 1 1 k = 1 y k + y + 1 k = 1 y k 1 k = 1 y k + y + 1 = 1 k = 1 y k k = 1 y k + 1 k = 1 y k + y + 1
152 147 150 151 syl2anc y 0 1 k = 1 y k + y + 1 = 1 k = 1 y k k = 1 y k + 1 k = 1 y k + y + 1
153 fzfid y 0 1 k = 1 y k + y + 1 Fin
154 2cnd y 0 m 1 k = 1 y k + y + 1 2
155 elfzelz m 1 k = 1 y k + y + 1 m
156 155 zcnd m 1 k = 1 y k + y + 1 m
157 156 adantl y 0 m 1 k = 1 y k + y + 1 m
158 154 157 mulcld y 0 m 1 k = 1 y k + y + 1 2 m
159 1cnd y 0 m 1 k = 1 y k + y + 1 1
160 158 159 subcld y 0 m 1 k = 1 y k + y + 1 2 m 1
161 145 152 153 160 fsumsplit y 0 m = 1 k = 1 y k + y + 1 2 m 1 = m = 1 k = 1 y k 2 m 1 + m = k = 1 y k + 1 k = 1 y k + y + 1 2 m 1
162 161 adantr y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 m = 1 k = 1 y k + y + 1 2 m 1 = m = 1 k = 1 y k 2 m 1 + m = k = 1 y k + 1 k = 1 y k + y + 1 2 m 1
163 142 162 eqtrd y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 m = 1 k = 1 y + 1 k 2 m 1 = m = 1 k = 1 y k 2 m 1 + m = k = 1 y k + 1 k = 1 y k + y + 1 2 m 1
164 112 137 163 3eqtr4d y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 k = 1 y + 1 l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y + 1 k 2 m 1
165 164 ex y 0 k = 1 y l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y k 2 m 1 k = 1 y + 1 l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 y + 1 k 2 m 1
166 6 12 18 24 36 165 nn0ind N 0 k = 1 N l = 1 k k 2 k + 2 l - 1 = m = 1 k = 1 N k 2 m 1
167 fz1ssnn 1 N
168 nnssnn0 0
169 167 168 sstri 1 N 0
170 169 a1i N 0 1 N 0
171 170 sselda N 0 k 1 N k 0
172 nicomachus k 0 l = 1 k k 2 k + 2 l - 1 = k 3
173 171 172 syl N 0 k 1 N l = 1 k k 2 k + 2 l - 1 = k 3
174 173 sumeq2dv N 0 k = 1 N l = 1 k k 2 k + 2 l - 1 = k = 1 N k 3
175 fzfid N 0 1 N Fin
176 175 171 fsumnn0cl N 0 k = 1 N k 0
177 oddnumth k = 1 N k 0 m = 1 k = 1 N k 2 m 1 = k = 1 N k 2
178 176 177 syl N 0 m = 1 k = 1 N k 2 m 1 = k = 1 N k 2
179 166 174 178 3eqtr3d N 0 k = 1 N k 3 = k = 1 N k 2