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

Metamath Proof Explorer

Theorem telgsum

Description: Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019)

Ref Expression
Hypotheses telgsum.b ⊢ B = Base G
telgsum.g ⊢ φ → G ∈ Abel
telgsum.m ⊢ - ˙ = - G
telgsum.0 ⊢ 0 ˙ = 0 G
telgsum.f ⊢ φ → ∀ k ∈ ℕ 0 A ∈ B
telgsum.s ⊢ φ → S ∈ ℕ 0
telgsum.u ⊢ φ → ∀ k ∈ ℕ 0 S < k → A = 0 ˙
telgsum.c ⊢ k = i → A = C
telgsum.d ⊢ k = i + 1 → A = D
telgsum.e ⊢ k = 0 → A = E
Assertion telgsum ⊢ φ → ∑ G i ∈ ℕ 0 C - ˙ D = E

Proof

Step Hyp Ref Expression
1 telgsum.b ⊢ B = Base G
2 telgsum.g ⊢ φ → G ∈ Abel
3 telgsum.m ⊢ - ˙ = - G
4 telgsum.0 ⊢ 0 ˙ = 0 G
5 telgsum.f ⊢ φ → ∀ k ∈ ℕ 0 A ∈ B
6 telgsum.s ⊢ φ → S ∈ ℕ 0
7 telgsum.u ⊢ φ → ∀ k ∈ ℕ 0 S < k → A = 0 ˙
8 telgsum.c ⊢ k = i → A = C
9 telgsum.d ⊢ k = i + 1 → A = D
10 telgsum.e ⊢ k = 0 → A = E
11 simpr ⊢ φ ∧ i ∈ ℕ 0 → i ∈ ℕ 0
12 8 adantl ⊢ φ ∧ i ∈ ℕ 0 ∧ k = i → A = C
13 11 12 csbied ⊢ φ ∧ i ∈ ℕ 0 → ⦋ i / k⦌ A = C
14 13 eqcomd ⊢ φ ∧ i ∈ ℕ 0 → C = ⦋ i / k⦌ A
15 peano2nn0 ⊢ i ∈ ℕ 0 → i + 1 ∈ ℕ 0
16 15 adantl ⊢ φ ∧ i ∈ ℕ 0 → i + 1 ∈ ℕ 0
17 9 adantl ⊢ φ ∧ i ∈ ℕ 0 ∧ k = i + 1 → A = D
18 16 17 csbied ⊢ φ ∧ i ∈ ℕ 0 → ⦋ i + 1 / k⦌ A = D
19 18 eqcomd ⊢ φ ∧ i ∈ ℕ 0 → D = ⦋ i + 1 / k⦌ A
20 14 19 oveq12d ⊢ φ ∧ i ∈ ℕ 0 → C - ˙ D = ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A
21 20 mpteq2dva ⊢ φ → i ∈ ℕ 0 ⟼ C - ˙ D = i ∈ ℕ 0 ⟼ ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A
22 21 oveq2d ⊢ φ → ∑ G i ∈ ℕ 0 C - ˙ D = ∑ G i ∈ ℕ 0 ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A
23 1 2 3 4 5 6 7 telgsums ⊢ φ → ∑ G i ∈ ℕ 0 ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A = ⦋ 0 / k⦌ A
24 c0ex ⊢ 0 ∈ V
25 24 a1i ⊢ φ → 0 ∈ V
26 10 adantl ⊢ φ ∧ k = 0 → A = E
27 25 26 csbied ⊢ φ → ⦋ 0 / k⦌ A = E
28 22 23 27 3eqtrd ⊢ φ → ∑ G i ∈ ℕ 0 C - ˙ D = E