telgsumfzslem

Description: Lemma for telgsumfzs (induction step). (Contributed by AV, 23-Nov-2019)

	Ref	Expression
Hypotheses	telgsumfzs.b	$⊢ B = {Base}_{G}$
	telgsumfzs.g	$⊢ φ \to G \in Abel$
	telgsumfzs.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		telgsumfzs.b	$⊢ B = {Base}_{G}$
2		telgsumfzs.g	$⊢ φ \to G \in Abel$
3		telgsumfzs.m	$⊢ \underset{˙}{-} = -_{G}$
4		eqid	$⊢ +_{G} = +_{G}$
5	2	adantr	$⊢ (φ \land \forall k \in (M \dots y + 1 + 1) C \in B) \to G \in Abel$
6		ablcmn	$⊢ G \in Abel \to G \in CMnd$
7	5 6	syl	$⊢ (φ \land \forall k \in (M \dots y + 1 + 1) C \in B) \to G \in CMnd$
8	7	adantl	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to G \in CMnd$
9		fzfid	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to (M \dots y + 1) \in Fin$
10		ablgrp	$⊢ G \in Abel \to G \in Grp$
11	2 10	syl	$⊢ φ \to G \in Grp$
12	11	ad2antrl	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to G \in Grp$
13	12	adantr	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land i \in (M \dots y + 1)) \to G \in Grp$
14		fzelp1	$⊢ i \in (M \dots y + 1) \to i \in (M \dots y + 1 + 1)$
15		simpr	$⊢ (φ \land \forall k \in (M \dots y + 1 + 1) C \in B) \to \forall k \in (M \dots y + 1 + 1) C \in B$
16	15	adantl	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to \forall k \in (M \dots y + 1 + 1) C \in B$
17		rspcsbela	$⊢ (i \in (M \dots y + 1 + 1) \land \forall k \in (M \dots y + 1 + 1) C \in B) \to ⦋ i / k ⦌ C \in B$
18	14 16 17	syl2anr	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land i \in (M \dots y + 1)) \to ⦋ i / k ⦌ C \in B$
19		fzp1elp1	$⊢ i \in (M \dots y + 1) \to i + 1 \in (M \dots y + 1 + 1)$
20		rspcsbela	$⊢ (i + 1 \in (M \dots y + 1 + 1) \land \forall k \in (M \dots y + 1 + 1) C \in B) \to ⦋ (i + 1) / k ⦌ C \in B$
21	19 16 20	syl2anr	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land i \in (M \dots y + 1)) \to ⦋ (i + 1) / k ⦌ C \in B$
22	1 3	grpsubcl	$⊢ (G \in Grp \land ⦋ i / k ⦌ C \in B \land ⦋ (i + 1) / k ⦌ C \in B) \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C \in B$
23	13 18 21 22	syl3anc	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land i \in (M \dots y + 1)) \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C \in B$
24		fzp1disj	$⊢ (M \dots y) \cap \{y + 1\} = \emptyset$
25	24	a1i	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to (M \dots y) \cap \{y + 1\} = \emptyset$
26		fzsuc	$⊢ y \in ℤ_{\geq M} \to (M \dots y + 1) = (M \dots y) \cup \{y + 1\}$
27	26	adantr	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to (M \dots y + 1) = (M \dots y) \cup \{y + 1\}$
28	1 4 8 9 23 25 27	gsummptfidmsplit	$⊢ (y \in ℤ_{\geq M} \land (φ \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) = ({\sum_{G}}_{i = M}^{y}, (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)) +_{G} (\underset{i \in \{y + 1\}}{\sum_{G}}, (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C))$
29	28	adantr	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land {\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) = ({\sum_{G}}_{i = M}^{y}, (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)) +_{G} (\underset{i \in \{y + 1\}}{\sum_{G}}, (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C))$
30		simpr	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land {\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} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C$
31		grpmnd	$⊢ G \in Grp \to G \in Mnd$
32	11 31	syl	$⊢ φ \to G \in Mnd$
33	32	ad2antrl	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to G \in Mnd$
34		ovexd	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to y + 1 \in V$
35		peano2uz	$⊢ y \in ℤ_{\geq M} \to y + 1 \in ℤ_{\geq M}$
36		eluzfz2	$⊢ y + 1 \in ℤ_{\geq M} \to y + 1 \in (M \dots y + 1)$
37	35 36	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 \in (M \dots y + 1)$
38		fzelp1	$⊢ y + 1 \in (M \dots y + 1) \to y + 1 \in (M \dots y + 1 + 1)$
39	37 38	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 \in (M \dots y + 1 + 1)$
40		rspcsbela	$⊢ (y + 1 \in (M \dots y + 1 + 1) \land \forall k \in (M \dots y + 1 + 1) C \in B) \to ⦋ (y + 1) / k ⦌ C \in B$
41	39 15 40	syl2an	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to ⦋ (y + 1) / k ⦌ C \in B$
42		peano2uz	$⊢ y + 1 \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ_{\geq M}$
43	35 42	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ_{\geq M}$
44		eluzfz2	$⊢ y + 1 + 1 \in ℤ_{\geq M} \to y + 1 + 1 \in (M \dots y + 1 + 1)$
45	43 44	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in (M \dots y + 1 + 1)$
46		rspcsbela	$⊢ (y + 1 + 1 \in (M \dots y + 1 + 1) \land \forall k \in (M \dots y + 1 + 1) C \in B) \to ⦋ (y + 1 + 1) / k ⦌ C \in B$
47	45 15 46	syl2an	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to ⦋ (y + 1 + 1) / k ⦌ C \in B$
48	1 3	grpsubcl	$⊢ (G \in Grp \land ⦋ (y + 1) / k ⦌ C \in B \land ⦋ (y + 1 + 1) / k ⦌ C \in B) \to ⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C \in B$
49	12 41 47 48	syl3anc	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to ⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C \in B$
50		csbeq1	$⊢ i = y + 1 \to ⦋ i / k ⦌ C = ⦋ (y + 1) / k ⦌ C$
51		oveq1	$⊢ i = y + 1 \to i + 1 = y + 1 + 1$
52	51	csbeq1d	$⊢ i = y + 1 \to ⦋ (i + 1) / k ⦌ C = ⦋ (y + 1 + 1) / k ⦌ C$
53	50 52	oveq12d	$⊢ i = y + 1 \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C = ⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
54	53	adantl	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land i = y + 1) \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C = ⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
55	1 33 34 49 54	gsumsnd	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to \underset{i \in \{y + 1\}}{\sum_{G}} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
56	55	adantr	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land {\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C) \to \underset{i \in \{y + 1\}}{\sum_{G}} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
57	30 56	oveq12d	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land {\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}, (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)) +_{G} (\underset{i \in \{y + 1\}}{\sum_{G}}, (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C)) = (⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C) +_{G} (⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C)$
58		eluzfz1	$⊢ y + 1 + 1 \in ℤ_{\geq M} \to M \in (M \dots y + 1 + 1)$
59	43 58	syl	$⊢ y \in ℤ_{\geq M} \to M \in (M \dots y + 1 + 1)$
60		rspcsbela	$⊢ (M \in (M \dots y + 1 + 1) \land \forall k \in (M \dots y + 1 + 1) C \in B) \to ⦋ M / k ⦌ C \in B$
61	59 15 60	syl2an	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to ⦋ M / k ⦌ C \in B$
62	1 4 3	grpnpncan	$⊢ (G \in Grp \land (⦋ M / k ⦌ C \in B \land ⦋ (y + 1) / k ⦌ C \in B \land ⦋ (y + 1 + 1) / k ⦌ C \in B)) \to (⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C) +_{G} (⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
63	12 61 41 47 62	syl13anc	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to (⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C) +_{G} (⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
64	63	adantr	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land {\sum_{G}}_{i = M}^{y} (⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C) \to (⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1) / k ⦌ C) +_{G} (⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C) = ⦋ M / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
65	29 57 64	3eqtrd	$⊢ ((y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \land {\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$
66	65	ex	$⊢ (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)$

Metamath Proof Explorer

Theorem telgsumfzslem

Proof