Metamath Proof Explorer


Theorem telgsumfzslem

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

Ref Expression
Hypotheses telgsumfzs.b B = Base G
telgsumfzs.g φ G Abel
telgsumfzs.m - ˙ = - G
Assertion telgsumfzslem y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C G i = M y + 1 i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 + 1 / k C

Proof

Step Hyp Ref Expression
1 telgsumfzs.b B = Base G
2 telgsumfzs.g φ G Abel
3 telgsumfzs.m - ˙ = - G
4 eqid + G = + G
5 2 adantr φ k M y + 1 + 1 C B G Abel
6 ablcmn G Abel G CMnd
7 5 6 syl φ k M y + 1 + 1 C B G CMnd
8 7 adantl y M φ k M y + 1 + 1 C B G CMnd
9 fzfid y M φ k M y + 1 + 1 C B M y + 1 Fin
10 ablgrp G Abel G Grp
11 2 10 syl φ G Grp
12 11 ad2antrl y M φ k M y + 1 + 1 C B G Grp
13 12 adantr y M φ k M y + 1 + 1 C B i M y + 1 G Grp
14 fzelp1 i M y + 1 i M y + 1 + 1
15 simpr φ k M y + 1 + 1 C B k M y + 1 + 1 C B
16 15 adantl y M φ k M y + 1 + 1 C B k M y + 1 + 1 C B
17 rspcsbela i M y + 1 + 1 k M y + 1 + 1 C B i / k C B
18 14 16 17 syl2anr y M φ k M y + 1 + 1 C B i M y + 1 i / k C B
19 fzp1elp1 i M y + 1 i + 1 M y + 1 + 1
20 rspcsbela i + 1 M y + 1 + 1 k M y + 1 + 1 C B i + 1 / k C B
21 19 16 20 syl2anr y M φ k M y + 1 + 1 C B i M y + 1 i + 1 / k C B
22 1 3 grpsubcl G Grp i / k C B i + 1 / k C B i / k C - ˙ i + 1 / k C B
23 13 18 21 22 syl3anc y M φ k M y + 1 + 1 C B i M y + 1 i / k C - ˙ i + 1 / k C B
24 fzp1disj M y y + 1 =
25 24 a1i y M φ k M y + 1 + 1 C B M y y + 1 =
26 fzsuc y M M y + 1 = M y y + 1
27 26 adantr y M φ k M y + 1 + 1 C B M y + 1 = M y y + 1
28 1 4 8 9 23 25 27 gsummptfidmsplit y M φ k M y + 1 + 1 C B G i = M y + 1 i / k C - ˙ i + 1 / k C = G i = M y i / k C - ˙ i + 1 / k C + G G i y + 1 i / k C - ˙ i + 1 / k C
29 28 adantr y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C G i = M y + 1 i / k C - ˙ i + 1 / k C = G i = M y i / k C - ˙ i + 1 / k C + G G i y + 1 i / k C - ˙ i + 1 / k C
30 simpr y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C
31 11 grpmndd φ G Mnd
32 31 ad2antrl y M φ k M y + 1 + 1 C B G Mnd
33 ovexd y M φ k M y + 1 + 1 C B y + 1 V
34 peano2uz y M y + 1 M
35 eluzfz2 y + 1 M y + 1 M y + 1
36 34 35 syl y M y + 1 M y + 1
37 fzelp1 y + 1 M y + 1 y + 1 M y + 1 + 1
38 36 37 syl y M y + 1 M y + 1 + 1
39 rspcsbela y + 1 M y + 1 + 1 k M y + 1 + 1 C B y + 1 / k C B
40 38 15 39 syl2an y M φ k M y + 1 + 1 C B y + 1 / k C B
41 peano2uz y + 1 M y + 1 + 1 M
42 34 41 syl y M y + 1 + 1 M
43 eluzfz2 y + 1 + 1 M y + 1 + 1 M y + 1 + 1
44 42 43 syl y M y + 1 + 1 M y + 1 + 1
45 rspcsbela y + 1 + 1 M y + 1 + 1 k M y + 1 + 1 C B y + 1 + 1 / k C B
46 44 15 45 syl2an y M φ k M y + 1 + 1 C B y + 1 + 1 / k C B
47 1 3 grpsubcl G Grp y + 1 / k C B y + 1 + 1 / k C B y + 1 / k C - ˙ y + 1 + 1 / k C B
48 12 40 46 47 syl3anc y M φ k M y + 1 + 1 C B y + 1 / k C - ˙ y + 1 + 1 / k C B
49 csbeq1 i = y + 1 i / k C = y + 1 / k C
50 oveq1 i = y + 1 i + 1 = y + 1 + 1
51 50 csbeq1d i = y + 1 i + 1 / k C = y + 1 + 1 / k C
52 49 51 oveq12d i = y + 1 i / k C - ˙ i + 1 / k C = y + 1 / k C - ˙ y + 1 + 1 / k C
53 52 adantl y M φ k M y + 1 + 1 C B i = y + 1 i / k C - ˙ i + 1 / k C = y + 1 / k C - ˙ y + 1 + 1 / k C
54 1 32 33 48 53 gsumsnd y M φ k M y + 1 + 1 C B G i y + 1 i / k C - ˙ i + 1 / k C = y + 1 / k C - ˙ y + 1 + 1 / k C
55 54 adantr y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C G i y + 1 i / k C - ˙ i + 1 / k C = y + 1 / k C - ˙ y + 1 + 1 / k C
56 30 55 oveq12d y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C G i = M y i / k C - ˙ i + 1 / k C + G G i y + 1 i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C + G y + 1 / k C - ˙ y + 1 + 1 / k C
57 eluzfz1 y + 1 + 1 M M M y + 1 + 1
58 42 57 syl y M M M y + 1 + 1
59 rspcsbela M M y + 1 + 1 k M y + 1 + 1 C B M / k C B
60 58 15 59 syl2an y M φ k M y + 1 + 1 C B M / k C B
61 1 4 3 grpnpncan G Grp M / k C B y + 1 / k C B y + 1 + 1 / k C B M / k C - ˙ y + 1 / k C + G y + 1 / k C - ˙ y + 1 + 1 / k C = M / k C - ˙ y + 1 + 1 / k C
62 12 60 40 46 61 syl13anc y M φ k M y + 1 + 1 C B M / k C - ˙ y + 1 / k C + G y + 1 / k C - ˙ y + 1 + 1 / k C = M / k C - ˙ y + 1 + 1 / k C
63 62 adantr y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C M / k C - ˙ y + 1 / k C + G y + 1 / k C - ˙ y + 1 + 1 / k C = M / k C - ˙ y + 1 + 1 / k C
64 29 56 63 3eqtrd y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C G i = M y + 1 i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 + 1 / k C
65 64 ex y M φ k M y + 1 + 1 C B G i = M y i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 / k C G i = M y + 1 i / k C - ˙ i + 1 / k C = M / k C - ˙ y + 1 + 1 / k C