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 ) )