Theorem telgsums

Description: Telescoping finitely supported group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019)

	Ref	Expression
Hypotheses	telgsums.b	$$⊢B={\mathrm{Base}}_G$$
	telgsums.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	telgsums.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	telgsums.0	$$⊢\underset{\dot{}}{0}=0_G$$
	telgsums.f	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}C\in B$$
	telgsums.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	telgsums.u	$$⊢\phi \to \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)$$
Assertion	telgsums	$$⊢\phi \to \underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\right)=⦋0/k⦌C$$

Proof

Step	Hyp	Ref	Expression
1		telgsums.b	$$⊢B={\mathrm{Base}}_G$$
2		telgsums.g	$$⊢\phi \to G\in \mathrm{Abel}$$
3		telgsums.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		telgsums.0	$$⊢\underset{\dot{}}{0}=0_G$$
5		telgsums.f	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}C\in B$$
6		telgsums.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
7		telgsums.u	$$⊢\phi \to \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)$$
8		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
9	2 8	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
10		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
11	2 10	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
12	11	adantr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to G\in \mathrm{Grp}$$
13		simpr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to i\in {\mathbb{N}}_0$$
14	5	adantr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \forall k\in {\mathbb{N}}_{0}C\in B$$
15		rspcsbela	$$⊢\left(i\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}C\in B\right)\to ⦋i/k⦌C\in B$$
16	13 14 15	syl2anc	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to ⦋i/k⦌C\in B$$
17		peano2nn0	$$⊢i\in {\mathbb{N}}_0\to i+1\in {\mathbb{N}}_0$$
18		rspcsbela	$$⊢\left(i+1\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}C\in B\right)\to ⦋\left(i+1\right)/k⦌C\in B$$
19	17 5 18	syl2anr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to ⦋\left(i+1\right)/k⦌C\in B$$
20	1 3	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge ⦋i/k⦌C\in B\wedge ⦋\left(i+1\right)/k⦌C\in B\right)\to ⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\in B$$
21	12 16 19 20	syl3anc	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to ⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\in B$$
22	21	ralrimiva	$$⊢\phi \to \forall i\in {\mathbb{N}}_0⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\in B$$
23		rspsbca	$$⊢\left(i\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{[}i/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)$$
24		sbcimg	$$⊢i\in \mathrm{V}\to \left(\underset{\dot{}}{[}i/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(\underset{\dot{}}{[}i/k\underset{\dot{}}{]}S<k\to \underset{\dot{}}{[}i/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\right)\right)$$
25		sbcbr2g	$$⊢i\in \mathrm{V}\to \left(\underset{\dot{}}{[}i/k\underset{\dot{}}{]}S<k\leftrightarrow S<⦋i/k⦌k\right)$$
26		csbvarg	$$⊢i\in \mathrm{V}\to ⦋i/k⦌k=i$$
27	26	breq2d	$$⊢i\in \mathrm{V}\to \left(S<⦋i/k⦌k\leftrightarrow S<i\right)$$
28	25 27	bitrd	$$⊢i\in \mathrm{V}\to \left(\underset{\dot{}}{[}i/k\underset{\dot{}}{]}S<k\leftrightarrow S<i\right)$$
29		sbceq1g	$$⊢i\in \mathrm{V}\to \left(\underset{\dot{}}{[}i/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\leftrightarrow ⦋i/k⦌C=\underset{\dot{}}{0}\right)$$
30	28 29	imbi12d	$$⊢i\in \mathrm{V}\to \left(\left(\underset{\dot{}}{[}i/k\underset{\dot{}}{]}S<k\to \underset{\dot{}}{[}i/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<i\to ⦋i/k⦌C=\underset{\dot{}}{0}\right)\right)$$
31	24 30	bitrd	$$⊢i\in \mathrm{V}\to \left(\underset{\dot{}}{[}i/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<i\to ⦋i/k⦌C=\underset{\dot{}}{0}\right)\right)$$
32	31	elv	$$⊢\underset{\dot{}}{[}i/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<i\to ⦋i/k⦌C=\underset{\dot{}}{0}\right)$$
33	23 32	sylib	$$⊢\left(i\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\right)\to \left(S<i\to ⦋i/k⦌C=\underset{\dot{}}{0}\right)$$
34	33	expcom	$$⊢\forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\to \left(i\in {\mathbb{N}}_0\to \left(S<i\to ⦋i/k⦌C=\underset{\dot{}}{0}\right)\right)$$
35	7 34	syl	$$⊢\phi \to \left(i\in {\mathbb{N}}_0\to \left(S<i\to ⦋i/k⦌C=\underset{\dot{}}{0}\right)\right)$$
36	35	imp31	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to ⦋i/k⦌C=\underset{\dot{}}{0}$$
37	6	nn0red	$$⊢\phi \to S\in ℝ$$
38	37	adantr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to S\in ℝ$$
39	38	adantr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to S\in ℝ$$
40		nn0re	$$⊢i\in {\mathbb{N}}_0\to i\in ℝ$$
41	40	ad2antlr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to i\in ℝ$$
42	17	ad2antlr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to i+1\in {\mathbb{N}}_0$$
43	42	nn0red	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to i+1\in ℝ$$
44		simpr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to S<i$$
45	41	ltp1d	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to i<i+1$$
46	39 41 43 44 45	lttrd	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to S<i+1$$
47	46	ex	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \left(S<i\to S<i+1\right)$$
48		rspsbca	$$⊢\left(i+1\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)$$
49		ovex	$$⊢i+1\in \mathrm{V}$$
50		sbcimg	$$⊢i+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}S<k\to \underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\right)\right)$$
51		sbcbr2g	$$⊢i+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}S<k\leftrightarrow S<⦋\left(i+1\right)/k⦌k\right)$$
52		csbvarg	$$⊢i+1\in \mathrm{V}\to ⦋\left(i+1\right)/k⦌k=i+1$$
53	52	breq2d	$$⊢i+1\in \mathrm{V}\to \left(S<⦋\left(i+1\right)/k⦌k\leftrightarrow S<i+1\right)$$
54	51 53	bitrd	$$⊢i+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}S<k\leftrightarrow S<i+1\right)$$
55		sbceq1g	$$⊢i+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\leftrightarrow ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
56	54 55	imbi12d	$$⊢i+1\in \mathrm{V}\to \left(\left(\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}S<k\to \underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<i+1\to ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)\right)$$
57	50 56	bitrd	$$⊢i+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<i+1\to ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)\right)$$
58	49 57	ax-mp	$$⊢\underset{\dot{}}{[}\left(i+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<i+1\to ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
59	48 58	sylib	$$⊢\left(i+1\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\right)\to \left(S<i+1\to ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
60	17 7 59	syl2anr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \left(S<i+1\to ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
61	47 60	syld	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \left(S<i\to ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
62	61	imp	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to ⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}$$
63	36 62	oveq12d	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to ⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\underset{\dot{}}{-}\underset{\dot{}}{0}$$
64	12	adantr	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to G\in \mathrm{Grp}$$
65	1 4	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
66	1 4 3	grpsubid	$$⊢\left(G\in \mathrm{Grp}\wedge \underset{\dot{}}{0}\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{-}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
67	64 65 66	syl2anc2	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to \underset{\dot{}}{0}\underset{\dot{}}{-}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
68	63 67	eqtrd	$$⊢\left(\left(\phi \wedge i\in {\mathbb{N}}_0\right)\wedge S<i\right)\to ⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}$$
69	68	ex	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \left(S<i\to ⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
70	69	ralrimiva	$$⊢\phi \to \forall i\in {\mathbb{N}}_0\left(S<i\to ⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
71	1 4 9 22 6 70	gsummptnn0fz	$$⊢\phi \to \underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\right)=\underset{i=0}{\overset{S}{{\sum }_G}}\left(⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\right)$$
72		fzssuz	$$⊢\left(0\dots S+1\right)\subseteq {\mathbb{Z}}_{\ge 0}$$
73	72	a1i	$$⊢\phi \to \left(0\dots S+1\right)\subseteq {\mathbb{Z}}_{\ge 0}$$
74		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
75	73 74	sseqtrrdi	$$⊢\phi \to \left(0\dots S+1\right)\subseteq {\mathbb{N}}_0$$
76		ssralv	$$⊢\left(0\dots S+1\right)\subseteq {\mathbb{N}}_0\to \left(\forall k\in {\mathbb{N}}_{0}C\in B\to \forall k\in \left(0\dots S+1\right)C\in B\right)$$
77	75 5 76	sylc	$$⊢\phi \to \forall k\in \left(0\dots S+1\right)C\in B$$
78	1 2 3 6 77	telgsumfz0s	$$⊢\phi \to \underset{i=0}{\overset{S}{{\sum }_G}}\left(⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\right)=⦋0/k⦌C\underset{\dot{}}{-}⦋\left(S+1\right)/k⦌C$$
79		peano2nn0	$$⊢S\in {\mathbb{N}}_0\to S+1\in {\mathbb{N}}_0$$
80	6 79	syl	$$⊢\phi \to S+1\in {\mathbb{N}}_0$$
81	37	ltp1d	$$⊢\phi \to S<S+1$$
82		rspsbca	$$⊢\left(S+1\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)$$
83		ovex	$$⊢S+1\in \mathrm{V}$$
84		sbcimg	$$⊢S+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}S<k\to \underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\right)\right)$$
85		sbcbr2g	$$⊢S+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}S<k\leftrightarrow S<⦋\left(S+1\right)/k⦌k\right)$$
86		csbvarg	$$⊢S+1\in \mathrm{V}\to ⦋\left(S+1\right)/k⦌k=S+1$$
87	86	breq2d	$$⊢S+1\in \mathrm{V}\to \left(S<⦋\left(S+1\right)/k⦌k\leftrightarrow S<S+1\right)$$
88	85 87	bitrd	$$⊢S+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}S<k\leftrightarrow S<S+1\right)$$
89		sbceq1g	$$⊢S+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\leftrightarrow ⦋\left(S+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
90	88 89	imbi12d	$$⊢S+1\in \mathrm{V}\to \left(\left(\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}S<k\to \underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<S+1\to ⦋\left(S+1\right)/k⦌C=\underset{\dot{}}{0}\right)\right)$$
91	84 90	bitrd	$$⊢S+1\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<S+1\to ⦋\left(S+1\right)/k⦌C=\underset{\dot{}}{0}\right)\right)$$
92	83 91	ax-mp	$$⊢\underset{\dot{}}{[}\left(S+1\right)/k\underset{\dot{}}{]}\left(S<k\to C=\underset{\dot{}}{0}\right)\leftrightarrow \left(S<S+1\to ⦋\left(S+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
93	82 92	sylib	$$⊢\left(S+1\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\right)\to \left(S<S+1\to ⦋\left(S+1\right)/k⦌C=\underset{\dot{}}{0}\right)$$
94	93	ex	$$⊢S+1\in {\mathbb{N}}_0\to \left(\forall k\in {\mathbb{N}}_0\left(S<k\to C=\underset{\dot{}}{0}\right)\to \left(S<S+1\to ⦋\left(S+1\right)/k⦌C=\underset{\dot{}}{0}\right)\right)$$
95	80 7 81 94	syl3c	$$⊢\phi \to ⦋\left(S+1\right)/k⦌C=\underset{\dot{}}{0}$$
96	95	oveq2d	$$⊢\phi \to ⦋0/k⦌C\underset{\dot{}}{-}⦋\left(S+1\right)/k⦌C=⦋0/k⦌C\underset{\dot{}}{-}\underset{\dot{}}{0}$$
97		0nn0	$$⊢0\in {\mathbb{N}}_0$$
98	97	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
99		rspcsbela	$$⊢\left(0\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}C\in B\right)\to ⦋0/k⦌C\in B$$
100	98 5 99	syl2anc	$$⊢\phi \to ⦋0/k⦌C\in B$$
101	1 4 3	grpsubid1	$$⊢\left(G\in \mathrm{Grp}\wedge ⦋0/k⦌C\in B\right)\to ⦋0/k⦌C\underset{\dot{}}{-}\underset{\dot{}}{0}=⦋0/k⦌C$$
102	11 100 101	syl2anc	$$⊢\phi \to ⦋0/k⦌C\underset{\dot{}}{-}\underset{\dot{}}{0}=⦋0/k⦌C$$
103	96 102	eqtrd	$$⊢\phi \to ⦋0/k⦌C\underset{\dot{}}{-}⦋\left(S+1\right)/k⦌C=⦋0/k⦌C$$
104	71 78 103	3eqtrd	$$⊢\phi \to \underset{i\in {\mathbb{N}}_0}{{\sum }_G}\left(⦋i/k⦌C\underset{\dot{}}{-}⦋\left(i+1\right)/k⦌C\right)=⦋0/k⦌C$$