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 e. NN0 -> sum_ k e. ( 1 ... N ) ( k ^ 3 ) = ( sum_ k e. ( 1 ... N ) k ^ 2 ) )

Proof

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