This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 → 𝑆 ∈ ℕ₀ )
		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	⊢ ( 𝜑 → 𝑆 ∈ ℕ₀ )
5		telgsumfz0s.f	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑆 + 1 ) ) 𝐶 ∈ 𝐵 )
6		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
7	4 6	eleqtrdi	⊢ ( 𝜑 → 𝑆 ∈ ( ℤ_≥ ‘ 0 ) )
8	1 2 3 7 5	telgsumfzs	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑖 ∈ ( 0 ... 𝑆 ) ↦ ( ⦋ 𝑖 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑖 + 1 ) / 𝑘 ⦌ 𝐶 ) ) ) = ( ⦋ 0 / 𝑘 ⦌ 𝐶 − ⦋ ( 𝑆 + 1 ) / 𝑘 ⦌ 𝐶 ) )