Database
BASIC ALGEBRAIC STRUCTURES
Groups
Abelian groups
Group sums over (ranges of) integers
telgsumfz0s
Metamath Proof Explorer
Description: Telescoping finite group sum ranging over nonnegative integers, using
explicit substitution. (Contributed by AV , 24-Oct-2019) (Proof
shortened by AV , 25-Nov-2019)
Ref
Expression
Hypotheses
telgsumfz0s.b
⊢ B = Base G
telgsumfz0s.g
⊢ φ → G ∈ Abel
telgsumfz0s.m
⊢ - ˙ = - G
telgsumfz0s.s
⊢ φ → S ∈ ℕ 0
telgsumfz0s.f
⊢ φ → ∀ k ∈ 0 … S + 1 C ∈ B
Assertion
telgsumfz0s
⊢ φ → ∑ G i = 0 S ⦋ i / k ⦌ C - ˙ ⦋ i + 1 / k ⦌ C = ⦋ 0 / k ⦌ C - ˙ ⦋ S + 1 / k ⦌ C
Proof
Step
Hyp
Ref
Expression
1
telgsumfz0s.b
⊢ B = Base G
2
telgsumfz0s.g
⊢ φ → G ∈ Abel
3
telgsumfz0s.m
⊢ - ˙ = - G
4
telgsumfz0s.s
⊢ φ → S ∈ ℕ 0
5
telgsumfz0s.f
⊢ φ → ∀ k ∈ 0 … S + 1 C ∈ B
6
nn0uz
⊢ ℕ 0 = ℤ ≥ 0
7
4 6
eleqtrdi
⊢ φ → S ∈ ℤ ≥ 0
8
1 2 3 7 5
telgsumfzs
⊢ φ → ∑ G i = 0 S ⦋ i / k ⦌ C - ˙ ⦋ i + 1 / k ⦌ C = ⦋ 0 / k ⦌ C - ˙ ⦋ S + 1 / k ⦌ C