Metamath Proof Explorer

Theorem nicomachus

Description: Nicomachus's Theorem. The sum of the odd numbers from N ^ 2 - N + 1 to N ^ 2 + N - 1 is N ^ 3 . Proof 2 from https://proofwiki.org/wiki/Nicomachus%27s_Theorem . (Contributed by SN, 21-Mar-2025)

Ref Expression
Assertion nicomachus 
|- ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( ( N ^ 2 ) - N ) + ( ( 2 x. k ) - 1 ) ) = ( N ^ 3 ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
2 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
3 2 adantr 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> N e. CC )
4 3 sqcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( N ^ 2 ) e. CC )
5 4 3 subcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( ( N ^ 2 ) - N ) e. CC )
6 2cnd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 2 e. CC )
7 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
8 7 nncnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
9 8 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. CC )
10 6 9 mulcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( 2 x. k ) e. CC )
11 1cnd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 e. CC )
12 10 11 subcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( ( 2 x. k ) - 1 ) e. CC )
13 1 5 12 fsumadd 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( ( N ^ 2 ) - N ) + ( ( 2 x. k ) - 1 ) ) = ( sum_ k e. ( 1 ... N ) ( ( N ^ 2 ) - N ) + sum_ k e. ( 1 ... N ) ( ( 2 x. k ) - 1 ) ) )
14 id 
 |-  ( N e. NN0 -> N e. NN0 )
15 2 sqcld 
 |-  ( N e. NN0 -> ( N ^ 2 ) e. CC )
16 15 2 subcld 
 |-  ( N e. NN0 -> ( ( N ^ 2 ) - N ) e. CC )
17 14 16 fz1sumconst 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( N ^ 2 ) - N ) = ( N x. ( ( N ^ 2 ) - N ) ) )
18 2 15 2 subdid 
 |-  ( N e. NN0 -> ( N x. ( ( N ^ 2 ) - N ) ) = ( ( N x. ( N ^ 2 ) ) - ( N x. N ) ) )
19 df-3 
 |-  3 = ( 2 + 1 )
20 19 oveq2i 
 |-  ( N ^ 3 ) = ( N ^ ( 2 + 1 ) )
21 2nn0 
 |-  2 e. NN0
22 21 a1i 
 |-  ( N e. NN0 -> 2 e. NN0 )
23 2 22 expp1d 
 |-  ( N e. NN0 -> ( N ^ ( 2 + 1 ) ) = ( ( N ^ 2 ) x. N ) )
24 20 23 eqtrid 
 |-  ( N e. NN0 -> ( N ^ 3 ) = ( ( N ^ 2 ) x. N ) )
25 15 2 mulcomd 
 |-  ( N e. NN0 -> ( ( N ^ 2 ) x. N ) = ( N x. ( N ^ 2 ) ) )
26 24 25 eqtr2d 
 |-  ( N e. NN0 -> ( N x. ( N ^ 2 ) ) = ( N ^ 3 ) )
27 2 sqvald 
 |-  ( N e. NN0 -> ( N ^ 2 ) = ( N x. N ) )
28 27 eqcomd 
 |-  ( N e. NN0 -> ( N x. N ) = ( N ^ 2 ) )
29 26 28 oveq12d 
 |-  ( N e. NN0 -> ( ( N x. ( N ^ 2 ) ) - ( N x. N ) ) = ( ( N ^ 3 ) - ( N ^ 2 ) ) )
30 17 18 29 3eqtrd 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( N ^ 2 ) - N ) = ( ( N ^ 3 ) - ( N ^ 2 ) ) )
31 oddnumth 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( 2 x. k ) - 1 ) = ( N ^ 2 ) )
32 30 31 oveq12d 
 |-  ( N e. NN0 -> ( sum_ k e. ( 1 ... N ) ( ( N ^ 2 ) - N ) + sum_ k e. ( 1 ... N ) ( ( 2 x. k ) - 1 ) ) = ( ( ( N ^ 3 ) - ( N ^ 2 ) ) + ( N ^ 2 ) ) )
33 3nn0 
 |-  3 e. NN0
34 33 a1i 
 |-  ( N e. NN0 -> 3 e. NN0 )
35 2 34 expcld 
 |-  ( N e. NN0 -> ( N ^ 3 ) e. CC )
36 35 15 npcand 
 |-  ( N e. NN0 -> ( ( ( N ^ 3 ) - ( N ^ 2 ) ) + ( N ^ 2 ) ) = ( N ^ 3 ) )
37 13 32 36 3eqtrd 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( ( N ^ 2 ) - N ) + ( ( 2 x. k ) - 1 ) ) = ( N ^ 3 ) )