Metamath Proof Explorer

Theorem oddnumth

Description: The Odd Number Theorem. The sum of the first N odd numbers is N ^ 2 . A corollary of arisum . (Contributed by SN, 21-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
2 2cnd 
 |-  ( k e. ( 1 ... N ) -> 2 e. CC )
3 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
4 3 nncnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
5 2 4 mulcld 
 |-  ( k e. ( 1 ... N ) -> ( 2 x. k ) e. CC )
6 5 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> ( 2 x. k ) e. CC )
7 1cnd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 e. CC )
8 1 6 7 fsumsub 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( 2 x. k ) - 1 ) = ( sum_ k e. ( 1 ... N ) ( 2 x. k ) - sum_ k e. ( 1 ... N ) 1 ) )
9 arisum 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) k = ( ( ( N ^ 2 ) + N ) / 2 ) )
10 9 oveq2d 
 |-  ( N e. NN0 -> ( 2 x. sum_ k e. ( 1 ... N ) k ) = ( 2 x. ( ( ( N ^ 2 ) + N ) / 2 ) ) )
11 2cnd 
 |-  ( N e. NN0 -> 2 e. CC )
12 4 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. CC )
13 1 11 12 fsummulc2 
 |-  ( N e. NN0 -> ( 2 x. sum_ k e. ( 1 ... N ) k ) = sum_ k e. ( 1 ... N ) ( 2 x. k ) )
14 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
15 14 sqcld 
 |-  ( N e. NN0 -> ( N ^ 2 ) e. CC )
16 15 14 addcld 
 |-  ( N e. NN0 -> ( ( N ^ 2 ) + N ) e. CC )
17 2ne0 
 |-  2 =/= 0
18 17 a1i 
 |-  ( N e. NN0 -> 2 =/= 0 )
19 16 11 18 divcan2d 
 |-  ( N e. NN0 -> ( 2 x. ( ( ( N ^ 2 ) + N ) / 2 ) ) = ( ( N ^ 2 ) + N ) )
20 10 13 19 3eqtr3d 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( 2 x. k ) = ( ( N ^ 2 ) + N ) )
21 id 
 |-  ( N e. NN0 -> N e. NN0 )
22 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
23 21 22 fz1sumconst 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) 1 = ( N x. 1 ) )
24 14 mulridd 
 |-  ( N e. NN0 -> ( N x. 1 ) = N )
25 23 24 eqtrd 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) 1 = N )
26 20 25 oveq12d 
 |-  ( N e. NN0 -> ( sum_ k e. ( 1 ... N ) ( 2 x. k ) - sum_ k e. ( 1 ... N ) 1 ) = ( ( ( N ^ 2 ) + N ) - N ) )
27 15 14 pncand 
 |-  ( N e. NN0 -> ( ( ( N ^ 2 ) + N ) - N ) = ( N ^ 2 ) )
28 8 26 27 3eqtrd 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) ( ( 2 x. k ) - 1 ) = ( N ^ 2 ) )