Metamath Proof Explorer

Theorem arisum2

Description: Arithmetic series sum of the first N nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 2-Aug-2021) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

Ref Expression
Assertion arisum2 
|- ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
3 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
4 2 3 eleqtrdi 
 |-  ( N e. NN -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
5 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
6 5 adantl 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. NN0 )
7 6 nn0cnd 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. CC )
8 id 
 |-  ( k = 0 -> k = 0 )
9 4 7 8 fsum1p 
 |-  ( N e. NN -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k ) )
10 1e0p1 
 |-  1 = ( 0 + 1 )
11 10 oveq1i 
 |-  ( 1 ... ( N - 1 ) ) = ( ( 0 + 1 ) ... ( N - 1 ) )
12 11 sumeq1i 
 |-  sum_ k e. ( 1 ... ( N - 1 ) ) k = sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k
13 12 oveq2i 
 |-  ( 0 + sum_ k e. ( 1 ... ( N - 1 ) ) k ) = ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k )
14 fzfid 
 |-  ( N e. NN -> ( 1 ... ( N - 1 ) ) e. Fin )
15 elfznn 
 |-  ( k e. ( 1 ... ( N - 1 ) ) -> k e. NN )
16 15 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... ( N - 1 ) ) ) -> k e. NN )
17 16 nncnd 
 |-  ( ( N e. NN /\ k e. ( 1 ... ( N - 1 ) ) ) -> k e. CC )
18 14 17 fsumcl 
 |-  ( N e. NN -> sum_ k e. ( 1 ... ( N - 1 ) ) k e. CC )
19 18 addlidd 
 |-  ( N e. NN -> ( 0 + sum_ k e. ( 1 ... ( N - 1 ) ) k ) = sum_ k e. ( 1 ... ( N - 1 ) ) k )
20 13 19 eqtr3id 
 |-  ( N e. NN -> ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k ) = sum_ k e. ( 1 ... ( N - 1 ) ) k )
21 arisum 
 |-  ( ( N - 1 ) e. NN0 -> sum_ k e. ( 1 ... ( N - 1 ) ) k = ( ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) / 2 ) )
22 2 21 syl 
 |-  ( N e. NN -> sum_ k e. ( 1 ... ( N - 1 ) ) k = ( ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) / 2 ) )
23 nncn 
 |-  ( N e. NN -> N e. CC )
24 23 sqcld 
 |-  ( N e. NN -> ( N ^ 2 ) e. CC )
25 24 23 subcld 
 |-  ( N e. NN -> ( ( N ^ 2 ) - N ) e. CC )
26 2 nn0cnd 
 |-  ( N e. NN -> ( N - 1 ) e. CC )
27 23 2timesd 
 |-  ( N e. NN -> ( 2 x. N ) = ( N + N ) )
28 27 oveq2d 
 |-  ( N e. NN -> ( ( N ^ 2 ) - ( 2 x. N ) ) = ( ( N ^ 2 ) - ( N + N ) ) )
29 24 23 23 subsub4d 
 |-  ( N e. NN -> ( ( ( N ^ 2 ) - N ) - N ) = ( ( N ^ 2 ) - ( N + N ) ) )
30 28 29 eqtr4d 
 |-  ( N e. NN -> ( ( N ^ 2 ) - ( 2 x. N ) ) = ( ( ( N ^ 2 ) - N ) - N ) )
31 30 oveq1d 
 |-  ( N e. NN -> ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) = ( ( ( ( N ^ 2 ) - N ) - N ) + 1 ) )
32 binom2sub1 
 |-  ( N e. CC -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) )
33 23 32 syl 
 |-  ( N e. NN -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) )
34 1cnd 
 |-  ( N e. NN -> 1 e. CC )
35 25 23 34 subsubd 
 |-  ( N e. NN -> ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) = ( ( ( ( N ^ 2 ) - N ) - N ) + 1 ) )
36 31 33 35 3eqtr4d 
 |-  ( N e. NN -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) )
37 25 26 36 mvrrsubd 
 |-  ( N e. NN -> ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) = ( ( N ^ 2 ) - N ) )
38 37 oveq1d 
 |-  ( N e. NN -> ( ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) / 2 ) = ( ( ( N ^ 2 ) - N ) / 2 ) )
39 22 38 eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 1 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
40 9 20 39 3eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
41 oveq1 
 |-  ( N = 0 -> ( N - 1 ) = ( 0 - 1 ) )
42 41 oveq2d 
 |-  ( N = 0 -> ( 0 ... ( N - 1 ) ) = ( 0 ... ( 0 - 1 ) ) )
43 fz00m1 
 |-  ( 0 ... ( 0 - 1 ) ) = (/)
44 42 43 eqtrdi 
 |-  ( N = 0 -> ( 0 ... ( N - 1 ) ) = (/) )
45 44 sumeq1d 
 |-  ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = sum_ k e. (/) k )
46 sum0 
 |-  sum_ k e. (/) k = 0
47 45 46 eqtrdi 
 |-  ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = 0 )
48 sq0i 
 |-  ( N = 0 -> ( N ^ 2 ) = 0 )
49 id 
 |-  ( N = 0 -> N = 0 )
50 48 49 oveq12d 
 |-  ( N = 0 -> ( ( N ^ 2 ) - N ) = ( 0 - 0 ) )
51 0m0e0 
 |-  ( 0 - 0 ) = 0
52 50 51 eqtrdi 
 |-  ( N = 0 -> ( ( N ^ 2 ) - N ) = 0 )
53 52 oveq1d 
 |-  ( N = 0 -> ( ( ( N ^ 2 ) - N ) / 2 ) = ( 0 / 2 ) )
54 2cn 
 |-  2 e. CC
55 2ne0 
 |-  2 =/= 0
56 54 55 div0i 
 |-  ( 0 / 2 ) = 0
57 53 56 eqtrdi 
 |-  ( N = 0 -> ( ( ( N ^ 2 ) - N ) / 2 ) = 0 )
58 47 57 eqtr4d 
 |-  ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
59 40 58 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
60 1 59 sylbi 
 |-  ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )