Metamath Proof Explorer

Theorem telgsumfz

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

Ref Expression
Hypotheses telgsumfz.b ⊢ B = Base G
telgsumfz.g ⊢ φ → G ∈ Abel
telgsumfz.m ⊢ - ˙ = - G
telgsumfz.n ⊢ φ → N ∈ ℤ ≥ M
telgsumfz.f ⊢ φ → ∀ k ∈ M … N + 1 A ∈ B
telgsumfz.l ⊢ k = i → A = L
telgsumfz.c ⊢ k = i + 1 → A = C
telgsumfz.d ⊢ k = M → A = D
telgsumfz.e ⊢ k = N + 1 → A = E
Assertion telgsumfz ⊢ φ → ∑ G i = M N L - ˙ C = D - ˙ E

Proof

Step Hyp Ref Expression
1 telgsumfz.b ⊢ B = Base G
2 telgsumfz.g ⊢ φ → G ∈ Abel
3 telgsumfz.m ⊢ - ˙ = - G
4 telgsumfz.n ⊢ φ → N ∈ ℤ ≥ M
5 telgsumfz.f ⊢ φ → ∀ k ∈ M … N + 1 A ∈ B
6 telgsumfz.l ⊢ k = i → A = L
7 telgsumfz.c ⊢ k = i + 1 → A = C
8 telgsumfz.d ⊢ k = M → A = D
9 telgsumfz.e ⊢ k = N + 1 → A = E
10 simpr ⊢ φ ∧ i ∈ M … N → i ∈ M … N
11 6 adantl ⊢ φ ∧ i ∈ M … N ∧ k = i → A = L
12 10 11 csbied ⊢ φ ∧ i ∈ M … N → ⦋ i / k⦌ A = L
13 12 eqcomd ⊢ φ ∧ i ∈ M … N → L = ⦋ i / k⦌ A
14 ovexd ⊢ φ ∧ i ∈ M … N → i + 1 ∈ V
15 7 adantl ⊢ φ ∧ i ∈ M … N ∧ k = i + 1 → A = C
16 14 15 csbied ⊢ φ ∧ i ∈ M … N → ⦋ i + 1 / k⦌ A = C
17 16 eqcomd ⊢ φ ∧ i ∈ M … N → C = ⦋ i + 1 / k⦌ A
18 13 17 oveq12d ⊢ φ ∧ i ∈ M … N → L - ˙ C = ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A
19 18 mpteq2dva ⊢ φ → i ∈ M … N ⟼ L - ˙ C = i ∈ M … N ⟼ ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A
20 19 oveq2d ⊢ φ → ∑ G i = M N L - ˙ C = ∑ G i = M N ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A
21 1 2 3 4 5 telgsumfzs ⊢ φ → ∑ G i = M N ⦋ i / k⦌ A - ˙ ⦋ i + 1 / k⦌ A = ⦋ M / k⦌ A - ˙ ⦋ N + 1 / k⦌ A
22 4 elfvexd ⊢ φ → M ∈ V
23 8 adantl ⊢ φ ∧ k = M → A = D
24 22 23 csbied ⊢ φ → ⦋ M / k⦌ A = D
25 ovexd ⊢ φ → N + 1 ∈ V
26 9 adantl ⊢ φ ∧ k = N + 1 → A = E
27 25 26 csbied ⊢ φ → ⦋ N + 1 / k⦌ A = E
28 24 27 oveq12d ⊢ φ → ⦋ M / k⦌ A - ˙ ⦋ N + 1 / k⦌ A = D - ˙ E
29 20 21 28 3eqtrd ⊢ φ → ∑ G i = M N L - ˙ C = D - ˙ E