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	11	grpmndd	$⊢ φ \to G \in Mnd$
32	31	ad2antrl	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to G \in Mnd$
33		ovexd	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to y + 1 \in V$
34		peano2uz	$⊢ y \in ℤ_{\geq M} \to y + 1 \in ℤ_{\geq M}$
35		eluzfz2	$⊢ y + 1 \in ℤ_{\geq M} \to y + 1 \in (M \dots y + 1)$
36	34 35	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 \in (M \dots y + 1)$
37		fzelp1	$⊢ y + 1 \in (M \dots y + 1) \to y + 1 \in (M \dots y + 1 + 1)$
38	36 37	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 \in (M \dots y + 1 + 1)$
39		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$
40	38 15 39	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$
41		peano2uz	$⊢ y + 1 \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ_{\geq M}$
42	34 41	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in ℤ_{\geq M}$
43		eluzfz2	$⊢ y + 1 + 1 \in ℤ_{\geq M} \to y + 1 + 1 \in (M \dots y + 1 + 1)$
44	42 43	syl	$⊢ y \in ℤ_{\geq M} \to y + 1 + 1 \in (M \dots y + 1 + 1)$
45		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$
46	44 15 45	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$
47	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$
48	12 40 46 47	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$
49		csbeq1	$⊢ i = y + 1 \to ⦋ i / k ⦌ C = ⦋ (y + 1) / k ⦌ C$
50		oveq1	$⊢ i = y + 1 \to i + 1 = y + 1 + 1$
51	50	csbeq1d	$⊢ i = y + 1 \to ⦋ (i + 1) / k ⦌ C = ⦋ (y + 1 + 1) / k ⦌ C$
52	49 51	oveq12d	$⊢ i = y + 1 \to ⦋ i / k ⦌ C \underset{˙}{-} ⦋ (i + 1) / k ⦌ C = ⦋ (y + 1) / k ⦌ C \underset{˙}{-} ⦋ (y + 1 + 1) / k ⦌ C$
53	52	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$
54	1 32 33 48 53	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$
55	54	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$
56	30 55	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)$
57		eluzfz1	$⊢ y + 1 + 1 \in ℤ_{\geq M} \to M \in (M \dots y + 1 + 1)$
58	42 57	syl	$⊢ y \in ℤ_{\geq M} \to M \in (M \dots y + 1 + 1)$
59		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$
60	58 15 59	syl2an	$⊢ (y \in ℤ_{\geq M} \land (φ \land \forall k \in (M \dots y + 1 + 1) C \in B)) \to ⦋ M / k ⦌ C \in B$
61	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$
62	12 60 40 46 61	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$
63	62	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$
64	29 56 63	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$
65	64	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