Theorem telgsumfz0s

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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	telgsumfz0s.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	telgsumfz0s.m	⊢ − = ( -g ‘ 𝐺 )
	telgsumfz0s.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	telgsumfz0s.f	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐶 ∈ 𝐵 )
Assertion	telgsumfz0s	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 0 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		telgsumfz0s.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		telgsumfz0s.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
3		telgsumfz0s.m	⊢ − = ( -g ‘ 𝐺 )
4		telgsumfz0s.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
5		telgsumfz0s.f	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐶 ∈ 𝐵 )
6		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
7	4 6	eleqtrdi	⊢ ( 𝜑 → 𝑆 ∈ ( ℤ≥ ‘ 0 ) )
8	1 2 3 7 5	telgsumfzs	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 0 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 ) )