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

Proof

Step Hyp Ref Expression
1 elnn0 N 0 N N = 0
2 nnm1nn0 N N 1 0
3 nn0uz 0 = 0
4 2 3 eleqtrdi N N 1 0
5 elfznn0 k 0 N 1 k 0
6 5 adantl N k 0 N 1 k 0
7 6 nn0cnd N k 0 N 1 k
8 id k = 0 k = 0
9 4 7 8 fsum1p N k = 0 N 1 k = 0 + k = 0 + 1 N 1 k
10 1e0p1 1 = 0 + 1
11 10 oveq1i 1 N 1 = 0 + 1 N 1
12 11 sumeq1i k = 1 N 1 k = k = 0 + 1 N 1 k
13 12 oveq2i 0 + k = 1 N 1 k = 0 + k = 0 + 1 N 1 k
14 fzfid N 1 N 1 Fin
15 elfznn k 1 N 1 k
16 15 adantl N k 1 N 1 k
17 16 nncnd N k 1 N 1 k
18 14 17 fsumcl N k = 1 N 1 k
19 18 addid2d N 0 + k = 1 N 1 k = k = 1 N 1 k
20 13 19 eqtr3id N 0 + k = 0 + 1 N 1 k = k = 1 N 1 k
21 arisum N 1 0 k = 1 N 1 k = N 1 2 + N - 1 2
22 2 21 syl N k = 1 N 1 k = N 1 2 + N - 1 2
23 nncn N N
24 23 2timesd N 2 N = N + N
25 24 oveq2d N N 2 2 N = N 2 N + N
26 23 sqcld N N 2
27 26 23 23 subsub4d N N 2 - N - N = N 2 N + N
28 25 27 eqtr4d N N 2 2 N = N 2 - N - N
29 28 oveq1d N N 2 - 2 N + 1 = N 2 N - N + 1
30 binom2sub1 N N 1 2 = N 2 - 2 N + 1
31 23 30 syl N N 1 2 = N 2 - 2 N + 1
32 26 23 subcld N N 2 N
33 1cnd N 1
34 32 23 33 subsubd N N 2 - N - N 1 = N 2 N - N + 1
35 29 31 34 3eqtr4d N N 1 2 = N 2 - N - N 1
36 35 oveq1d N N 1 2 + N - 1 = N 2 - N - N 1 + N - 1
37 ax-1cn 1
38 subcl N 1 N 1
39 23 37 38 sylancl N N 1
40 32 39 npcand N N 2 - N - N 1 + N - 1 = N 2 N
41 36 40 eqtrd N N 1 2 + N - 1 = N 2 N
42 41 oveq1d N N 1 2 + N - 1 2 = N 2 N 2
43 22 42 eqtrd N k = 1 N 1 k = N 2 N 2
44 20 43 eqtrd N 0 + k = 0 + 1 N 1 k = N 2 N 2
45 9 44 eqtrd N k = 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
49 ltm1 0 0 1 < 0
50 48 49 ax-mp 0 1 < 0
51 0z 0
52 peano2zm 0 0 1
53 51 52 ax-mp 0 1
54 fzn 0 0 1 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 k = 0 N 1 k = k k
59 sum0 k k = 0
60 58 59 eqtrdi N = 0 k = 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
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 k = 0 N 1 k = N 2 N 2
72 45 71 jaoi N N = 0 k = 0 N 1 k = N 2 N 2
73 1 72 sylbi N 0 k = 0 N 1 k = N 2 N 2