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 0 k = 1 N k = N 2 + N 2

Proof

Step Hyp Ref Expression
1 elnn0 N 0 N N = 0
2 1zzd N 1
3 nnz N N
4 elfzelz k 1 N k
5 4 zcnd k 1 N k
6 5 adantl N k 1 N k
7 id k = j + 1 k = j + 1
8 2 2 3 6 7 fsumshftm N k = 1 N k = j = 1 1 N 1 j + 1
9 1m1e0 1 1 = 0
10 9 oveq1i 1 1 N 1 = 0 N 1
11 10 sumeq1i j = 1 1 N 1 j + 1 = j = 0 N 1 j + 1
12 8 11 eqtrdi N k = 1 N k = j = 0 N 1 j + 1
13 elfznn0 j 0 N 1 j 0
14 13 adantl N j 0 N 1 j 0
15 bcnp1n j 0 ( j + 1 j) = j + 1
16 14 15 syl N j 0 N 1 ( j + 1 j) = j + 1
17 14 nn0cnd N j 0 N 1 j
18 ax-1cn 1
19 addcom j 1 j + 1 = 1 + j
20 17 18 19 sylancl N j 0 N 1 j + 1 = 1 + j
21 20 oveq1d N j 0 N 1 ( j + 1 j) = ( 1 + j j)
22 16 21 eqtr3d N j 0 N 1 j + 1 = ( 1 + j j)
23 22 sumeq2dv N j = 0 N 1 j + 1 = j = 0 N 1 ( 1 + j j)
24 1nn0 1 0
25 nnm1nn0 N N 1 0
26 bcxmas 1 0 N 1 0 ( 1 + 1 + N 1 N 1 ) = j = 0 N 1 ( 1 + j j)
27 24 25 26 sylancr N ( 1 + 1 + N 1 N 1 ) = j = 0 N 1 ( 1 + j j)
28 23 27 eqtr4d N j = 0 N 1 j + 1 = ( 1 + 1 + N 1 N 1 )
29 1cnd N 1
30 nncn N N
31 29 29 30 ppncand N 1 + 1 + N 1 = 1 + N
32 29 30 31 comraddd N 1 + 1 + N 1 = N + 1
33 32 oveq1d N ( 1 + 1 + N 1 N 1 ) = ( N + 1 N 1 )
34 nnnn0 N N 0
35 bcp1m1 N 0 ( N + 1 N 1 ) = N + 1 N 2
36 34 35 syl N ( N + 1 N 1 ) = N + 1 N 2
37 sqval N N 2 = N N
38 37 eqcomd N N N = N 2
39 mulid2 N 1 N = N
40 38 39 oveq12d N N N + 1 N = N 2 + N
41 30 40 syl N N N + 1 N = N 2 + N
42 30 30 29 41 joinlmuladdmuld N N + 1 N = N 2 + N
43 42 oveq1d N N + 1 N 2 = N 2 + N 2
44 33 36 43 3eqtrd N ( 1 + 1 + N 1 N 1 ) = N 2 + N 2
45 12 28 44 3eqtrd N k = 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 k = 1 N k = k k
50 sum0 k k = 0
51 49 50 eqtrdi N = 0 k = 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
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 k = 1 N k = N 2 + N 2
63 45 62 jaoi N N = 0 k = 1 N k = N 2 + N 2
64 1 63 sylbi N 0 k = 1 N k = N 2 + N 2