Metamath Proof Explorer

Theorem arisum

Description: Arithmetic series sum of the first N positive integers. This is Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006) (Proof shortened by Mario Carneiro, 22-May-2014)

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

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 1zzd 
 |-  ( N e. NN -> 1 e. ZZ )
3 nnz 
 |-  ( N e. NN -> N e. ZZ )
4 elfzelz 
 |-  ( k e. ( 1 ... N ) -> k e. ZZ )
5 4 zcnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
6 5 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> k e. CC )
7 id 
 |-  ( k = ( j + 1 ) -> k = ( j + 1 ) )
8 2 2 3 6 7 fsumshftm 
 |-  ( N e. NN -> sum_ k e. ( 1 ... N ) k = sum_ j e. ( ( 1 - 1 ) ... ( N - 1 ) ) ( j + 1 ) )
9 1m1e0 
 |-  ( 1 - 1 ) = 0
10 9 oveq1i 
 |-  ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) )
11 10 sumeq1i 
 |-  sum_ j e. ( ( 1 - 1 ) ... ( N - 1 ) ) ( j + 1 ) = sum_ j e. ( 0 ... ( N - 1 ) ) ( j + 1 )
12 8 11 eqtrdi 
 |-  ( N e. NN -> sum_ k e. ( 1 ... N ) k = sum_ j e. ( 0 ... ( N - 1 ) ) ( j + 1 ) )
13 elfznn0 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j e. NN0 )
14 13 adantl 
 |-  ( ( N e. NN /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. NN0 )
15 bcnp1n 
 |-  ( j e. NN0 -> ( ( j + 1 ) _C j ) = ( j + 1 ) )
16 14 15 syl 
 |-  ( ( N e. NN /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( j + 1 ) _C j ) = ( j + 1 ) )
17 14 nn0cnd 
 |-  ( ( N e. NN /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. CC )
18 ax-1cn 
 |-  1 e. CC
19 addcom 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( j + 1 ) = ( 1 + j ) )
20 17 18 19 sylancl 
 |-  ( ( N e. NN /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( j + 1 ) = ( 1 + j ) )
21 20 oveq1d 
 |-  ( ( N e. NN /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( j + 1 ) _C j ) = ( ( 1 + j ) _C j ) )
22 16 21 eqtr3d 
 |-  ( ( N e. NN /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( j + 1 ) = ( ( 1 + j ) _C j ) )
23 22 sumeq2dv 
 |-  ( N e. NN -> sum_ j e. ( 0 ... ( N - 1 ) ) ( j + 1 ) = sum_ j e. ( 0 ... ( N - 1 ) ) ( ( 1 + j ) _C j ) )
24 1nn0 
 |-  1 e. NN0
25 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
26 bcxmas 
 |-  ( ( 1 e. NN0 /\ ( N - 1 ) e. NN0 ) -> ( ( ( 1 + 1 ) + ( N - 1 ) ) _C ( N - 1 ) ) = sum_ j e. ( 0 ... ( N - 1 ) ) ( ( 1 + j ) _C j ) )
27 24 25 26 sylancr 
 |-  ( N e. NN -> ( ( ( 1 + 1 ) + ( N - 1 ) ) _C ( N - 1 ) ) = sum_ j e. ( 0 ... ( N - 1 ) ) ( ( 1 + j ) _C j ) )
28 23 27 eqtr4d 
 |-  ( N e. NN -> sum_ j e. ( 0 ... ( N - 1 ) ) ( j + 1 ) = ( ( ( 1 + 1 ) + ( N - 1 ) ) _C ( N - 1 ) ) )
29 1cnd 
 |-  ( N e. NN -> 1 e. CC )
30 nncn 
 |-  ( N e. NN -> N e. CC )
31 29 29 30 ppncand 
 |-  ( N e. NN -> ( ( 1 + 1 ) + ( N - 1 ) ) = ( 1 + N ) )
32 29 30 31 comraddd 
 |-  ( N e. NN -> ( ( 1 + 1 ) + ( N - 1 ) ) = ( N + 1 ) )
33 32 oveq1d 
 |-  ( N e. NN -> ( ( ( 1 + 1 ) + ( N - 1 ) ) _C ( N - 1 ) ) = ( ( N + 1 ) _C ( N - 1 ) ) )
34 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
35 bcp1m1 
 |-  ( N e. NN0 -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( ( N + 1 ) x. N ) / 2 ) )
36 34 35 syl 
 |-  ( N e. NN -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( ( N + 1 ) x. N ) / 2 ) )
37 sqval 
 |-  ( N e. CC -> ( N ^ 2 ) = ( N x. N ) )
38 37 eqcomd 
 |-  ( N e. CC -> ( N x. N ) = ( N ^ 2 ) )
39 mulid2 
 |-  ( N e. CC -> ( 1 x. N ) = N )
40 38 39 oveq12d 
 |-  ( N e. CC -> ( ( N x. N ) + ( 1 x. N ) ) = ( ( N ^ 2 ) + N ) )
41 30 40 syl 
 |-  ( N e. NN -> ( ( N x. N ) + ( 1 x. N ) ) = ( ( N ^ 2 ) + N ) )
42 30 30 29 41 joinlmuladdmuld 
 |-  ( N e. NN -> ( ( N + 1 ) x. N ) = ( ( N ^ 2 ) + N ) )
43 42 oveq1d 
 |-  ( N e. NN -> ( ( ( N + 1 ) x. N ) / 2 ) = ( ( ( N ^ 2 ) + N ) / 2 ) )
44 33 36 43 3eqtrd 
 |-  ( N e. NN -> ( ( ( 1 + 1 ) + ( N - 1 ) ) _C ( N - 1 ) ) = ( ( ( N ^ 2 ) + N ) / 2 ) )
45 12 28 44 3eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 1 ... N ) k = ( ( ( N ^ 2 ) + N ) / 2 ) )
46 oveq2 
 |-  ( N = 0 -> ( 1 ... N ) = ( 1 ... 0 ) )
47 fz10 
 |-  ( 1 ... 0 ) = (/)
48 46 47 eqtrdi 
 |-  ( N = 0 -> ( 1 ... N ) = (/) )
49 48 sumeq1d 
 |-  ( N = 0 -> sum_ k e. ( 1 ... N ) k = sum_ k e. (/) k )
50 sum0 
 |-  sum_ k e. (/) k = 0
51 49 50 eqtrdi 
 |-  ( N = 0 -> sum_ k e. ( 1 ... N ) k = 0 )
52 sq0i 
 |-  ( N = 0 -> ( N ^ 2 ) = 0 )
53 id 
 |-  ( N = 0 -> N = 0 )
54 52 53 oveq12d 
 |-  ( N = 0 -> ( ( N ^ 2 ) + N ) = ( 0 + 0 ) )
55 00id 
 |-  ( 0 + 0 ) = 0
56 54 55 eqtrdi 
 |-  ( N = 0 -> ( ( N ^ 2 ) + N ) = 0 )
57 56 oveq1d 
 |-  ( N = 0 -> ( ( ( N ^ 2 ) + N ) / 2 ) = ( 0 / 2 ) )
58 2cn 
 |-  2 e. CC
59 2ne0 
 |-  2 =/= 0
60 58 59 div0i 
 |-  ( 0 / 2 ) = 0
61 57 60 eqtrdi 
 |-  ( N = 0 -> ( ( ( N ^ 2 ) + N ) / 2 ) = 0 )
62 51 61 eqtr4d 
 |-  ( N = 0 -> sum_ k e. ( 1 ... N ) k = ( ( ( N ^ 2 ) + N ) / 2 ) )
63 45 62 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> sum_ k e. ( 1 ... N ) k = ( ( ( N ^ 2 ) + N ) / 2 ) )
64 1 63 sylbi 
 |-  ( N e. NN0 -> sum_ k e. ( 1 ... N ) k = ( ( ( N ^ 2 ) + N ) / 2 ) )