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 ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 nnm1nn0 ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
3 nn0uz 0 = ( ℤ ‘ 0 )
4 2 3 eleqtrdi ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ ‘ 0 ) )
5 elfznn0 ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
6 5 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
7 6 nn0cnd ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
8 id ( 𝑘 = 0 → 𝑘 = 0 )
9 4 7 8 fsum1p ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 ) )
10 1e0p1 1 = ( 0 + 1 )
11 10 oveq1i ( 1 ... ( 𝑁 − 1 ) ) = ( ( 0 + 1 ) ... ( 𝑁 − 1 ) )
12 11 sumeq1i Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘
13 12 oveq2i ( 0 + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 ) = ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 )
14 fzfid ( 𝑁 ∈ ℕ → ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin )
15 elfznn ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ )
16 15 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ )
17 16 nncnd ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
18 14 17 fsumcl ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 ∈ ℂ )
19 18 addid2d ( 𝑁 ∈ ℕ → ( 0 + Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 )
20 13 19 eqtr3id ( 𝑁 ∈ ℕ → ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 )
21 arisum ( ( 𝑁 − 1 ) ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) / 2 ) )
22 2 21 syl ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) / 2 ) )
23 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
24 23 2timesd ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
25 24 oveq2d ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) = ( ( 𝑁 ↑ 2 ) − ( 𝑁 + 𝑁 ) ) )
26 23 sqcld ( 𝑁 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℂ )
27 26 23 23 subsub4d ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) = ( ( 𝑁 ↑ 2 ) − ( 𝑁 + 𝑁 ) ) )
28 25 27 eqtr4d ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) )
29 28 oveq1d ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) + 1 ) )
30 binom2sub1 ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) )
31 23 30 syl ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − ( 2 · 𝑁 ) ) + 1 ) )
32 26 23 subcld ( 𝑁 ∈ ℕ → ( ( 𝑁 ↑ 2 ) − 𝑁 ) ∈ ℂ )
33 1cnd ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
34 32 23 33 subsubd ( 𝑁 ∈ ℕ → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − 𝑁 ) + 1 ) )
35 29 31 34 3eqtr4d ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ↑ 2 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) )
36 35 oveq1d ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) = ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) )
37 ax-1cn 1 ∈ ℂ
38 subcl ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℂ )
39 23 37 38 sylancl ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
40 32 39 npcand ( 𝑁 ∈ ℕ → ( ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) − ( 𝑁 − 1 ) ) + ( 𝑁 − 1 ) ) = ( ( 𝑁 ↑ 2 ) − 𝑁 ) )
41 36 40 eqtrd ( 𝑁 ∈ ℕ → ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) = ( ( 𝑁 ↑ 2 ) − 𝑁 ) )
42 41 oveq1d ( 𝑁 ∈ ℕ → ( ( ( ( 𝑁 − 1 ) ↑ 2 ) + ( 𝑁 − 1 ) ) / 2 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
43 22 42 eqtrd ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
44 20 43 eqtrd ( 𝑁 ∈ ℕ → ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 𝑘 ) = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
45 9 44 eqtrd ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
46 oveq1 ( 𝑁 = 0 → ( 𝑁 − 1 ) = ( 0 − 1 ) )
47 46 oveq2d ( 𝑁 = 0 → ( 0 ... ( 𝑁 − 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 ( 𝑁 = 0 → ( 0 ... ( 𝑁 − 1 ) ) = ∅ )
58 57 sumeq1d ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = Σ 𝑘 ∈ ∅ 𝑘 )
59 sum0 Σ 𝑘 ∈ ∅ 𝑘 = 0
60 58 59 eqtrdi ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = 0 )
61 sq0i ( 𝑁 = 0 → ( 𝑁 ↑ 2 ) = 0 )
62 id ( 𝑁 = 0 → 𝑁 = 0 )
63 61 62 oveq12d ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) − 𝑁 ) = ( 0 − 0 ) )
64 0m0e0 ( 0 − 0 ) = 0
65 63 64 eqtrdi ( 𝑁 = 0 → ( ( 𝑁 ↑ 2 ) − 𝑁 ) = 0 )
66 65 oveq1d ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) = ( 0 / 2 ) )
67 2cn 2 ∈ ℂ
68 2ne0 2 ≠ 0
69 67 68 div0i ( 0 / 2 ) = 0
70 66 69 eqtrdi ( 𝑁 = 0 → ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) = 0 )
71 60 70 eqtr4d ( 𝑁 = 0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
72 45 71 jaoi ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )
73 1 72 sylbi ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( ( ( 𝑁 ↑ 2 ) − 𝑁 ) / 2 ) )