telgsumfzs

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

	Ref	Expression
Hypotheses	telgsumfzs.b	$⊢ B = {Base}_{G}$
	telgsumfzs.g	$⊢ φ \to G \in Abel$
	telgsumfzs.m	$⊢ \underset{˙}{-} = -_{G}$
	telgsumfzs.n	$⊢ φ \to N \in ℤ_{\geq M}$
	telgsumfzs.f	$⊢ φ \to \forall k \in (M \dots N + 1) C \in B$
Assertion	telgsumfzs	$⊢ φ \to {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C$

Proof

Step	Hyp	Ref	Expression
1		telgsumfzs.b	$⊢ B = {Base}_{G}$
2		telgsumfzs.g	$⊢ φ \to G \in Abel$
3		telgsumfzs.m	$⊢ \underset{˙}{-} = -_{G}$
4		telgsumfzs.n	$⊢ φ \to N \in ℤ_{\geq M}$
5		telgsumfzs.f	$⊢ φ \to \forall k \in (M \dots N + 1) C \in B$
6		oveq1	$⊢ x = M \to x + 1 = M + 1$
7	6	oveq2d	$⊢ x = M \to (M \dots x + 1) = (M \dots M + 1)$
8	7	raleqdv	$⊢ x = M \to (\forall k \in (M \dots x + 1) C \in B \leftrightarrow \forall k \in (M \dots M + 1) C \in B)$
9	8	anbi2d	$⊢ x = M \to ((φ \land \forall k \in (M \dots x + 1) C \in B) \leftrightarrow (φ \land \forall k \in (M \dots M + 1) C \in B))$
10		oveq2	$⊢ x = M \to (M \dots x) = (M \dots M)$
11	10	mpteq1d	$⊢ x = M \to (i \in (M \dots x) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = (i \in (M \dots M) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
12	11	oveq2d	$⊢ x = M \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = {\sum_{G}}_{i = M}^{M} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
13	6	csbeq1d	$⊢ x = M \to ⦋ (x + 1) / k ⦌ C = ⦋ (M + 1) / k ⦌ C$
14	13	oveq2d	$⊢ x = M \to ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C$
15	12 14	eqeq12d	$⊢ x = M \to ({\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C \leftrightarrow {\sum_{G}}_{i = M}^{M} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C)$
16	9 15	imbi12d	$⊢ x = M \to (((φ \land \forall k \in (M \dots x + 1) C \in B) \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C) \leftrightarrow ((φ \land \forall k \in (M \dots M + 1) C \in B) \to {\sum_{G}}_{i = M}^{M} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C))$
17		oveq1	$⊢ x = y \to x + 1 = y + 1$
18	17	oveq2d	$⊢ x = y \to (M \dots x + 1) = (M \dots y + 1)$
19	18	raleqdv	$⊢ x = y \to (\forall k \in (M \dots x + 1) C \in B \leftrightarrow \forall k \in (M \dots y + 1) C \in B)$
20	19	anbi2d	$⊢ x = y \to ((φ \land \forall k \in (M \dots x + 1) C \in B) \leftrightarrow (φ \land \forall k \in (M \dots y + 1) C \in B))$
21		oveq2	$⊢ x = y \to (M \dots x) = (M \dots y)$
22	21	mpteq1d	$⊢ x = y \to (i \in (M \dots x) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = (i \in (M \dots y) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
23	22	oveq2d	$⊢ x = y \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = {\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
24	17	csbeq1d	$⊢ x = y \to ⦋ (x + 1) / k ⦌ C = ⦋ (y + 1) / k ⦌ C$
25	24	oveq2d	$⊢ x = y \to ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C$
26	23 25	eqeq12d	$⊢ x = y \to ({\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C \leftrightarrow {\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C)$
27	20 26	imbi12d	$⊢ x = y \to (((φ \land \forall k \in (M \dots x + 1) C \in B) \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C) \leftrightarrow ((φ \land \forall k \in (M \dots y + 1) C \in B) \to {\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C))$
28		oveq1	$⊢ x = y + 1 \to x + 1 = y + 1 + 1$
29	28	oveq2d	$⊢ x = y + 1 \to (M \dots x + 1) = (M \dots y + 1 + 1)$
30	29	raleqdv	$⊢ x = y + 1 \to (\forall k \in (M \dots x + 1) C \in B \leftrightarrow \forall k \in (M \dots y + 1 + 1) C \in B)$
31	30	anbi2d	$⊢ x = y + 1 \to ((φ \land \forall k \in (M \dots x + 1) C \in B) \leftrightarrow (φ \land \forall k \in (M \dots y + 1 + 1) C \in B))$
32		oveq2	$⊢ x = y + 1 \to (M \dots x) = (M \dots y + 1)$
33	32	mpteq1d	$⊢ x = y + 1 \to (i \in (M \dots x) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = (i \in (M \dots y + 1) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
34	33	oveq2d	$⊢ x = y + 1 \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = {\sum_{G}}_{i = M}^{y + 1} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
35	28	csbeq1d	$⊢ x = y + 1 \to ⦋ (x + 1) / k ⦌ C = ⦋ (y + 1 + 1) / k ⦌ C$
36	35	oveq2d	$⊢ x = y + 1 \to ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
37	34 36	eqeq12d	$⊢ x = y + 1 \to ({\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C \leftrightarrow {\sum_{G}}_{i = M}^{y + 1} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C)$
38	31 37	imbi12d	$⊢ x = y + 1 \to (((φ \land \forall k \in (M \dots x + 1) C \in B) \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C) \leftrightarrow ((φ \land \forall k \in (M \dots y + 1 + 1) C \in B) \to {\sum_{G}}_{i = M}^{y + 1} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C))$
39		oveq1	$⊢ x = N \to x + 1 = N + 1$
40	39	oveq2d	$⊢ x = N \to (M \dots x + 1) = (M \dots N + 1)$
41	40	raleqdv	$⊢ x = N \to (\forall k \in (M \dots x + 1) C \in B \leftrightarrow \forall k \in (M \dots N + 1) C \in B)$
42	41	anbi2d	$⊢ x = N \to ((φ \land \forall k \in (M \dots x + 1) C \in B) \leftrightarrow (φ \land \forall k \in (M \dots N + 1) C \in B))$
43		oveq2	$⊢ x = N \to (M \dots x) = (M \dots N)$
44	43	mpteq1d	$⊢ x = N \to (i \in (M \dots x) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = (i \in (M \dots N) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
45	44	oveq2d	$⊢ x = N \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
46	39	csbeq1d	$⊢ x = N \to ⦋ (x + 1) / k ⦌ C = ⦋ (N + 1) / k ⦌ C$
47	46	oveq2d	$⊢ x = N \to ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C$
48	45 47	eqeq12d	$⊢ x = N \to ({\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C \leftrightarrow {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C)$
49	42 48	imbi12d	$⊢ x = N \to (((φ \land \forall k \in (M \dots x + 1) C \in B) \to {\sum_{G}}_{i = M}^{x} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (x + 1) / k ⦌ C) \leftrightarrow ((φ \land \forall k \in (M \dots N + 1) C \in B) \to {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C))$
50		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
51	4 50	syl	$⊢ φ \to M \in ℤ$
52	51	adantr	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M \in ℤ$
53		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
54	52 53	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to (M \dots M) = \{M\}$
55	54	mpteq1d	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to (i \in (M \dots M) ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = (i \in \{M\} ⟼ ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
56	55	oveq2d	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to {\sum_{G}}_{i = M}^{M} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = \underset{i \in \{M\}}{\sum_{G}} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)$
57		ablgrp	$⊢ G \in Abel \to G \in Grp$
58	2 57	syl	$⊢ φ \to G \in Grp$
59	58	grpmndd	$⊢ φ \to G \in Mnd$
60	59	adantr	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to G \in Mnd$
61	58	adantr	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to G \in Grp$
62		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
63	52 62	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M \in ℤ_{\geq M}$
64		peano2uz	$⊢ M \in ℤ_{\geq M} \to M + 1 \in ℤ_{\geq M}$
65	63 64	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M + 1 \in ℤ_{\geq M}$
66		eluzfz1	$⊢ M + 1 \in ℤ_{\geq M} \to M \in (M \dots M + 1)$
67	65 66	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M \in (M \dots M + 1)$
68		rspcsbela	$⊢ (M \in (M \dots M + 1) \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ M / k ⦌ C \in B$
69	67 68	sylancom	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ M / k ⦌ C \in B$
70		eluzfz2	$⊢ M + 1 \in ℤ_{\geq M} \to M + 1 \in (M \dots M + 1)$
71	65 70	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M + 1 \in (M \dots M + 1)$
72		rspcsbela	$⊢ (M + 1 \in (M \dots M + 1) \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ (M + 1) / k ⦌ C \in B$
73	71 72	sylancom	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ (M + 1) / k ⦌ C \in B$
74	1 3	grpsubcl	$⊢ (G \in Grp \land ⦋ M / k ⦌ C \in B \land ⦋ (M + 1) / k ⦌ C \in B) \to ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C \in B$
75	61 69 73 74	syl3anc	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C \in B$
76		csbeq1	$⊢ i = M \to ⦋ i / k ⦌ C = ⦋ M / k ⦌ C$
77		oveq1	$⊢ i = M \to i + 1 = M + 1$
78	77	csbeq1d	$⊢ i = M \to ⦋ (i + 1) / k ⦌ C = ⦋ (M + 1) / k ⦌ C$
79	76 78	oveq12d	$⊢ i = M \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C$
80	79	adantl	$⊢ ((φ \land \forall k \in (M \dots M + 1) C \in B) \land i = M) \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C$
81	1 60 52 75 80	gsumsnd	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to \underset{i \in \{M\}}{\sum_{G}} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C$
82	56 81	eqtrd	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to {\sum_{G}}_{i = M}^{M} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C$
83	1 2 3	telgsumfzslem	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to ({\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C \to {\sum_{G}}_{i = M}^{y + 1} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C)$
84	83	ex	$⊢ y \in ℤ_{\geq M} \to ((φ \land \forall k \in (M \dots y + 1 + 1) C \in B) \to ({\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C \to {\sum_{G}}_{i = M}^{y + 1} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C))$
85		eluzelz	$⊢ y \in ℤ_{\geq M} \to y \in ℤ$
86	85	peano2zd	$⊢ y \in ℤ_{\geq M} \to y + 1 \in ℤ$
87	86	peano2zd	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ$
88		peano2z	$⊢ y \in ℤ \to y + 1 \in ℤ$
89	88	zred	$⊢ y \in ℤ \to y + 1 \in ℝ$
90	85 89	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 \in ℝ$
91	90	lep1d	$⊢ y \in ℤ_{\geq M} \to y + 1 \leq y + 1 + 1$
92		eluz2	$⊢ y + 1 + 1 \in ℤ_{\geq (y + 1)} \leftrightarrow (y + 1 \in ℤ \land y + 1 + 1 \in ℤ \land y + 1 \leq y + 1 + 1)$
93	86 87 91 92	syl3anbrc	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ_{\geq (y + 1)}$
94		fzss2	$⊢ y + 1 + 1 \in ℤ_{\geq (y + 1)} \to (M \dots y + 1) \subseteq (M \dots y + 1 + 1)$
95	93 94	syl	$⊢ y \in ℤ_{\geq M} \to (M \dots y + 1) \subseteq (M \dots y + 1 + 1)$
96		ssralv	$⊢ (M \dots y + 1) \subseteq (M \dots y + 1 + 1) \to (\forall k \in (M \dots y + 1 + 1) C \in B \to \forall k \in (M \dots y + 1) C \in B)$
97	95 96	syl	$⊢ y \in ℤ_{\geq M} \to (\forall k \in (M \dots y + 1 + 1) C \in B \to \forall k \in (M \dots y + 1) C \in B)$
98	97	adantld	$⊢ y \in ℤ_{\geq M} \to ((φ \land \forall k \in (M \dots y + 1 + 1) C \in B) \to \forall k \in (M \dots y + 1) C \in B)$
99	84 98	a2and	$⊢ y \in ℤ_{\geq M} \to (((φ \land \forall k \in (M \dots y + 1) C \in B) \to {\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C) \to ((φ \land \forall k \in (M \dots y + 1 + 1) C \in B) \to {\sum_{G}}_{i = M}^{y + 1} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C))$
100	16 27 38 49 82 99	uzind4i	$⊢ N \in ℤ_{\geq M} \to ((φ \land \forall k \in (M \dots N + 1) C \in B) \to {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C)$
101	100	expd	$⊢ N \in ℤ_{\geq M} \to (φ \to (\forall k \in (M \dots N + 1) C \in B \to {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C))$
102	4 101	mpcom	$⊢ φ \to (\forall k \in (M \dots N + 1) C \in B \to {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C)$
103	5 102	mpd	$⊢ φ \to {\sum_{G}}_{i = M}^{N} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (N + 1) / k ⦌ C$

Metamath Proof Explorer

Theorem telgsumfzs

Proof