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		grpmnd	$⊢ G \in Grp \to G \in Mnd$
60	58 59	syl	$⊢ φ \to G \in Mnd$
61	60	adantr	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to G \in Mnd$
62	58	adantr	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to G \in Grp$
63		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
64	52 63	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M \in ℤ_{\geq M}$
65		peano2uz	$⊢ M \in ℤ_{\geq M} \to M + 1 \in ℤ_{\geq M}$
66	64 65	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M + 1 \in ℤ_{\geq M}$
67		eluzfz1	$⊢ M + 1 \in ℤ_{\geq M} \to M \in (M \dots M + 1)$
68	66 67	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M \in (M \dots M + 1)$
69		rspcsbela	$⊢ (M \in (M \dots M + 1) \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ M / k ⦌ C \in B$
70	68 69	sylancom	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ M / k ⦌ C \in B$
71		eluzfz2	$⊢ M + 1 \in ℤ_{\geq M} \to M + 1 \in (M \dots M + 1)$
72	66 71	syl	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to M + 1 \in (M \dots M + 1)$
73		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$
74	72 73	sylancom	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ (M + 1) / k ⦌ C \in B$
75	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$
76	62 70 74 75	syl3anc	$⊢ (φ \land \forall k \in (M \dots M + 1) C \in B) \to ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C \in B$
77		csbeq1	$⊢ i = M \to ⦋ i / k ⦌ C = ⦋ M / k ⦌ C$
78		oveq1	$⊢ i = M \to i + 1 = M + 1$
79	78	csbeq1d	$⊢ i = M \to ⦋ (i + 1) / k ⦌ C = ⦋ (M + 1) / k ⦌ C$
80	77 79	oveq12d	$⊢ i = M \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (M + 1) / k ⦌ C$
81	80	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$
82	1 61 52 76 81	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$
83	56 82	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$
84	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)$
85	84	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))$
86		eluzelz	$⊢ y \in ℤ_{\geq M} \to y \in ℤ$
87	86	peano2zd	$⊢ y \in ℤ_{\geq M} \to y + 1 \in ℤ$
88	87	peano2zd	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ$
89		peano2z	$⊢ y \in ℤ \to y + 1 \in ℤ$
90	89	zred	$⊢ y \in ℤ \to y + 1 \in ℝ$
91	86 90	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 \in ℝ$
92	91	lep1d	$⊢ y \in ℤ_{\geq M} \to y + 1 \leq y + 1 + 1$
93		eluz2	$⊢ y + 1 + 1 \in ℤ_{\geq (y + 1)} \leftrightarrow (y + 1 \in ℤ \land y + 1 + 1 \in ℤ \land y + 1 \leq y + 1 + 1)$
94	87 88 92 93	syl3anbrc	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ_{\geq (y + 1)}$
95		fzss2	$⊢ y + 1 + 1 \in ℤ_{\geq (y + 1)} \to (M \dots y + 1) \subseteq (M \dots y + 1 + 1)$
96	94 95	syl	$⊢ y \in ℤ_{\geq M} \to (M \dots y + 1) \subseteq (M \dots y + 1 + 1)$
97		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)$
98	96 97	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)$
99	98	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)$
100	85 99	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))$
101	16 27 38 49 83 100	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)$
102	101	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))$
103	4 102	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)$
104	5 103	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