Metamath Proof Explorer

Theorem telgsumfz0

Description: Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum . (Contributed by AV, 23-Nov-2019)

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

Proof

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