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)

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 addid2d 
 |-  ( 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 2timesd 
 |-  ( N e. NN -> ( 2 x. N ) = ( N + N ) )
25 24 oveq2d 
 |-  ( N e. NN -> ( ( N ^ 2 ) - ( 2 x. N ) ) = ( ( N ^ 2 ) - ( N + N ) ) )
26 23 sqcld 
 |-  ( N e. NN -> ( N ^ 2 ) e. CC )
27 26 23 23 subsub4d 
 |-  ( N e. NN -> ( ( ( N ^ 2 ) - N ) - N ) = ( ( N ^ 2 ) - ( N + N ) ) )
28 25 27 eqtr4d 
 |-  ( N e. NN -> ( ( N ^ 2 ) - ( 2 x. N ) ) = ( ( ( N ^ 2 ) - N ) - N ) )
29 28 oveq1d 
 |-  ( N e. NN -> ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) = ( ( ( ( N ^ 2 ) - N ) - N ) + 1 ) )
30 binom2sub1 
 |-  ( N e. CC -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) )
31 23 30 syl 
 |-  ( N e. NN -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - ( 2 x. N ) ) + 1 ) )
32 26 23 subcld 
 |-  ( N e. NN -> ( ( N ^ 2 ) - N ) e. CC )
33 1cnd 
 |-  ( N e. NN -> 1 e. CC )
34 32 23 33 subsubd 
 |-  ( N e. NN -> ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) = ( ( ( ( N ^ 2 ) - N ) - N ) + 1 ) )
35 29 31 34 3eqtr4d 
 |-  ( N e. NN -> ( ( N - 1 ) ^ 2 ) = ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) )
36 35 oveq1d 
 |-  ( N e. NN -> ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) = ( ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) + ( N - 1 ) ) )
37 ax-1cn 
 |-  1 e. CC
38 subcl 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N - 1 ) e. CC )
39 23 37 38 sylancl 
 |-  ( N e. NN -> ( N - 1 ) e. CC )
40 32 39 npcand 
 |-  ( N e. NN -> ( ( ( ( N ^ 2 ) - N ) - ( N - 1 ) ) + ( N - 1 ) ) = ( ( N ^ 2 ) - N ) )
41 36 40 eqtrd 
 |-  ( N e. NN -> ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) = ( ( N ^ 2 ) - N ) )
42 41 oveq1d 
 |-  ( N e. NN -> ( ( ( ( N - 1 ) ^ 2 ) + ( N - 1 ) ) / 2 ) = ( ( ( N ^ 2 ) - N ) / 2 ) )
43 22 42 eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 1 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
44 20 43 eqtrd 
 |-  ( N e. NN -> ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) k ) = ( ( ( N ^ 2 ) - N ) / 2 ) )
45 9 44 eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
46 oveq1 
 |-  ( N = 0 -> ( N - 1 ) = ( 0 - 1 ) )
47 46 oveq2d 
 |-  ( N = 0 -> ( 0 ... ( N - 1 ) ) = ( 0 ... ( 0 - 1 ) ) )
48 0re 
 |-  0 e. RR
49 ltm1 
 |-  ( 0 e. RR -> ( 0 - 1 ) < 0 )
50 48 49 ax-mp 
 |-  ( 0 - 1 ) < 0
51 0z 
 |-  0 e. ZZ
52 peano2zm 
 |-  ( 0 e. ZZ -> ( 0 - 1 ) e. ZZ )
53 51 52 ax-mp 
 |-  ( 0 - 1 ) e. ZZ
54 fzn 
 |-  ( ( 0 e. ZZ /\ ( 0 - 1 ) e. ZZ ) -> ( ( 0 - 1 ) < 0 <-> ( 0 ... ( 0 - 1 ) ) = (/) ) )
55 51 53 54 mp2an 
 |-  ( ( 0 - 1 ) < 0 <-> ( 0 ... ( 0 - 1 ) ) = (/) )
56 50 55 mpbi 
 |-  ( 0 ... ( 0 - 1 ) ) = (/)
57 47 56 eqtrdi 
 |-  ( N = 0 -> ( 0 ... ( N - 1 ) ) = (/) )
58 57 sumeq1d 
 |-  ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = sum_ k e. (/) k )
59 sum0 
 |-  sum_ k e. (/) k = 0
60 58 59 eqtrdi 
 |-  ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = 0 )
61 sq0i 
 |-  ( N = 0 -> ( N ^ 2 ) = 0 )
62 id 
 |-  ( N = 0 -> N = 0 )
63 61 62 oveq12d 
 |-  ( N = 0 -> ( ( N ^ 2 ) - N ) = ( 0 - 0 ) )
64 0m0e0 
 |-  ( 0 - 0 ) = 0
65 63 64 eqtrdi 
 |-  ( N = 0 -> ( ( N ^ 2 ) - N ) = 0 )
66 65 oveq1d 
 |-  ( N = 0 -> ( ( ( N ^ 2 ) - N ) / 2 ) = ( 0 / 2 ) )
67 2cn 
 |-  2 e. CC
68 2ne0 
 |-  2 =/= 0
69 67 68 div0i 
 |-  ( 0 / 2 ) = 0
70 66 69 eqtrdi 
 |-  ( N = 0 -> ( ( ( N ^ 2 ) - N ) / 2 ) = 0 )
71 60 70 eqtr4d 
 |-  ( N = 0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
72 45 71 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )
73 1 72 sylbi 
 |-  ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) k = ( ( ( N ^ 2 ) - N ) / 2 ) )