Metamath Proof Explorer

Theorem 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=BaseG
telgsumfzs.g ⊢φ→G∈Abel
telgsumfzs.m ⊢-˙=-G
telgsumfzs.n ⊢φ→N∈ℤ≥M
telgsumfzs.f ⊢φ→∀k∈M…N+1C∈B
Assertion telgsumfzs ⊢φ→∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C

Proof

Step Hyp Ref Expression
1 telgsumfzs.b ⊢B=BaseG
2 telgsumfzs.g ⊢φ→G∈Abel
3 telgsumfzs.m ⊢-˙=-G
4 telgsumfzs.n ⊢φ→N∈ℤ≥M
5 telgsumfzs.f ⊢φ→∀k∈M…N+1C∈B
6 oveq1 ⊢x=M→x+1=M+1
7 6 oveq2d ⊢x=M→M…x+1=M…M+1
8 7 raleqdv ⊢x=M→∀k∈M…x+1C∈B↔∀k∈M…M+1C∈B
9 8 anbi2d ⊢x=M→φ∧∀k∈M…x+1C∈B↔φ∧∀k∈M…M+1C∈B
10 oveq2 ⊢x=M→M…x=M…M
11 10 mpteq1d ⊢x=M→i∈M…x⟼⦋i/k⦌C-˙⦋i+1/k⦌C=i∈M…M⟼⦋i/k⦌C-˙⦋i+1/k⦌C
12 11 oveq2d ⊢x=M→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=∑Gi=MM⦋i/k⦌C-˙⦋i+1/k⦌C
13 6 csbeq1d ⊢x=M→⦋x+1/k⦌C=⦋M+1/k⦌C
14 13 oveq2d ⊢x=M→⦋M/k⦌C-˙⦋x+1/k⦌C=⦋M/k⦌C-˙⦋M+1/k⦌C
15 12 14 eqeq12d ⊢x=M→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔∑Gi=MM⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋M+1/k⦌C
16 9 15 imbi12d ⊢x=M→φ∧∀k∈M…x+1C∈B→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔φ∧∀k∈M…M+1C∈B→∑Gi=MM⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋M+1/k⦌C
17 oveq1 ⊢x=y→x+1=y+1
18 17 oveq2d ⊢x=y→M…x+1=M…y+1
19 18 raleqdv ⊢x=y→∀k∈M…x+1C∈B↔∀k∈M…y+1C∈B
20 19 anbi2d ⊢x=y→φ∧∀k∈M…x+1C∈B↔φ∧∀k∈M…y+1C∈B
21 oveq2 ⊢x=y→M…x=M…y
22 21 mpteq1d ⊢x=y→i∈M…x⟼⦋i/k⦌C-˙⦋i+1/k⦌C=i∈M…y⟼⦋i/k⦌C-˙⦋i+1/k⦌C
23 22 oveq2d ⊢x=y→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=∑Gi=My⦋i/k⦌C-˙⦋i+1/k⦌C
24 17 csbeq1d ⊢x=y→⦋x+1/k⦌C=⦋y+1/k⦌C
25 24 oveq2d ⊢x=y→⦋M/k⦌C-˙⦋x+1/k⦌C=⦋M/k⦌C-˙⦋y+1/k⦌C
26 23 25 eqeq12d ⊢x=y→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔∑Gi=My⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1/k⦌C
27 20 26 imbi12d ⊢x=y→φ∧∀k∈M…x+1C∈B→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔φ∧∀k∈M…y+1C∈B→∑Gi=My⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1/k⦌C
28 oveq1 ⊢x=y+1→x+1=y+1+1
29 28 oveq2d ⊢x=y+1→M…x+1=M…y+1+1
30 29 raleqdv ⊢x=y+1→∀k∈M…x+1C∈B↔∀k∈M…y+1+1C∈B
31 30 anbi2d ⊢x=y+1→φ∧∀k∈M…x+1C∈B↔φ∧∀k∈M…y+1+1C∈B
32 oveq2 ⊢x=y+1→M…x=M…y+1
33 32 mpteq1d ⊢x=y+1→i∈M…x⟼⦋i/k⦌C-˙⦋i+1/k⦌C=i∈M…y+1⟼⦋i/k⦌C-˙⦋i+1/k⦌C
34 33 oveq2d ⊢x=y+1→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=∑Gi=My+1⦋i/k⦌C-˙⦋i+1/k⦌C
35 28 csbeq1d ⊢x=y+1→⦋x+1/k⦌C=⦋y+1+1/k⦌C
36 35 oveq2d ⊢x=y+1→⦋M/k⦌C-˙⦋x+1/k⦌C=⦋M/k⦌C-˙⦋y+1+1/k⦌C
37 34 36 eqeq12d ⊢x=y+1→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔∑Gi=My+1⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1+1/k⦌C
38 31 37 imbi12d ⊢x=y+1→φ∧∀k∈M…x+1C∈B→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔φ∧∀k∈M…y+1+1C∈B→∑Gi=My+1⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1+1/k⦌C
39 oveq1 ⊢x=N→x+1=N+1
40 39 oveq2d ⊢x=N→M…x+1=M…N+1
41 40 raleqdv ⊢x=N→∀k∈M…x+1C∈B↔∀k∈M…N+1C∈B
42 41 anbi2d ⊢x=N→φ∧∀k∈M…x+1C∈B↔φ∧∀k∈M…N+1C∈B
43 oveq2 ⊢x=N→M…x=M…N
44 43 mpteq1d ⊢x=N→i∈M…x⟼⦋i/k⦌C-˙⦋i+1/k⦌C=i∈M…N⟼⦋i/k⦌C-˙⦋i+1/k⦌C
45 44 oveq2d ⊢x=N→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C
46 39 csbeq1d ⊢x=N→⦋x+1/k⦌C=⦋N+1/k⦌C
47 46 oveq2d ⊢x=N→⦋M/k⦌C-˙⦋x+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C
48 45 47 eqeq12d ⊢x=N→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C
49 42 48 imbi12d ⊢x=N→φ∧∀k∈M…x+1C∈B→∑Gi=Mx⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋x+1/k⦌C↔φ∧∀k∈M…N+1C∈B→∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C
50 eluzel2 ⊢N∈ℤ≥M→M∈ℤ
51 4 50 syl ⊢φ→M∈ℤ
52 51 adantr ⊢φ∧∀k∈M…M+1C∈B→M∈ℤ
53 fzsn ⊢M∈ℤ→M…M=M
54 52 53 syl ⊢φ∧∀k∈M…M+1C∈B→M…M=M
55 54 mpteq1d ⊢φ∧∀k∈M…M+1C∈B→i∈M…M⟼⦋i/k⦌C-˙⦋i+1/k⦌C=i∈M⟼⦋i/k⦌C-˙⦋i+1/k⦌C
56 55 oveq2d ⊢φ∧∀k∈M…M+1C∈B→∑Gi=MM⦋i/k⦌C-˙⦋i+1/k⦌C=∑Gi∈M⦋i/k⦌C-˙⦋i+1/k⦌C
57 ablgrp ⊢G∈Abel→G∈Grp
58 2 57 syl ⊢φ→G∈Grp
59 58 grpmndd ⊢φ→G∈Mnd
60 59 adantr ⊢φ∧∀k∈M…M+1C∈B→G∈Mnd
61 58 adantr ⊢φ∧∀k∈M…M+1C∈B→G∈Grp
62 uzid ⊢M∈ℤ→M∈ℤ≥M
63 52 62 syl ⊢φ∧∀k∈M…M+1C∈B→M∈ℤ≥M
64 peano2uz ⊢M∈ℤ≥M→M+1∈ℤ≥M
65 63 64 syl ⊢φ∧∀k∈M…M+1C∈B→M+1∈ℤ≥M
66 eluzfz1 ⊢M+1∈ℤ≥M→M∈M…M+1
67 65 66 syl ⊢φ∧∀k∈M…M+1C∈B→M∈M…M+1
68 rspcsbela ⊢M∈M…M+1∧∀k∈M…M+1C∈B→⦋M/k⦌C∈B
69 67 68 sylancom ⊢φ∧∀k∈M…M+1C∈B→⦋M/k⦌C∈B
70 eluzfz2 ⊢M+1∈ℤ≥M→M+1∈M…M+1
71 65 70 syl ⊢φ∧∀k∈M…M+1C∈B→M+1∈M…M+1
72 rspcsbela ⊢M+1∈M…M+1∧∀k∈M…M+1C∈B→⦋M+1/k⦌C∈B
73 71 72 sylancom ⊢φ∧∀k∈M…M+1C∈B→⦋M+1/k⦌C∈B
74 1 3 grpsubcl ⊢G∈Grp∧⦋M/k⦌C∈B∧⦋M+1/k⦌C∈B→⦋M/k⦌C-˙⦋M+1/k⦌C∈B
75 61 69 73 74 syl3anc ⊢φ∧∀k∈M…M+1C∈B→⦋M/k⦌C-˙⦋M+1/k⦌C∈B
76 csbeq1 ⊢i=M→⦋i/k⦌C=⦋M/k⦌C
77 oveq1 ⊢i=M→i+1=M+1
78 77 csbeq1d ⊢i=M→⦋i+1/k⦌C=⦋M+1/k⦌C
79 76 78 oveq12d ⊢i=M→⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋M+1/k⦌C
80 79 adantl ⊢φ∧∀k∈M…M+1C∈B∧i=M→⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋M+1/k⦌C
81 1 60 52 75 80 gsumsnd ⊢φ∧∀k∈M…M+1C∈B→∑Gi∈M⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋M+1/k⦌C
82 56 81 eqtrd ⊢φ∧∀k∈M…M+1C∈B→∑Gi=MM⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋M+1/k⦌C
83 1 2 3 telgsumfzslem ⊢y∈ℤ≥M∧φ∧∀k∈M…y+1+1C∈B→∑Gi=My⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1/k⦌C→∑Gi=My+1⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1+1/k⦌C
84 83 ex ⊢y∈ℤ≥M→φ∧∀k∈M…y+1+1C∈B→∑Gi=My⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1/k⦌C→∑Gi=My+1⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1+1/k⦌C
85 eluzelz ⊢y∈ℤ≥M→y∈ℤ
86 85 peano2zd ⊢y∈ℤ≥M→y+1∈ℤ
87 86 peano2zd ⊢y∈ℤ≥M→y+1+1∈ℤ
88 peano2z ⊢y∈ℤ→y+1∈ℤ
89 88 zred ⊢y∈ℤ→y+1∈ℝ
90 85 89 syl ⊢y∈ℤ≥M→y+1∈ℝ
91 90 lep1d ⊢y∈ℤ≥M→y+1≤y+1+1
92 eluz2 ⊢y+1+1∈ℤ≥y+1↔y+1∈ℤ∧y+1+1∈ℤ∧y+1≤y+1+1
93 86 87 91 92 syl3anbrc ⊢y∈ℤ≥M→y+1+1∈ℤ≥y+1
94 fzss2 ⊢y+1+1∈ℤ≥y+1→M…y+1⊆M…y+1+1
95 93 94 syl ⊢y∈ℤ≥M→M…y+1⊆M…y+1+1
96 ssralv ⊢M…y+1⊆M…y+1+1→∀k∈M…y+1+1C∈B→∀k∈M…y+1C∈B
97 95 96 syl ⊢y∈ℤ≥M→∀k∈M…y+1+1C∈B→∀k∈M…y+1C∈B
98 97 adantld ⊢y∈ℤ≥M→φ∧∀k∈M…y+1+1C∈B→∀k∈M…y+1C∈B
99 84 98 a2and ⊢y∈ℤ≥M→φ∧∀k∈M…y+1C∈B→∑Gi=My⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1/k⦌C→φ∧∀k∈M…y+1+1C∈B→∑Gi=My+1⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋y+1+1/k⦌C
100 16 27 38 49 82 99 uzind4i ⊢N∈ℤ≥M→φ∧∀k∈M…N+1C∈B→∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C
101 100 expd ⊢N∈ℤ≥M→φ→∀k∈M…N+1C∈B→∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C
102 4 101 mpcom ⊢φ→∀k∈M…N+1C∈B→∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C
103 5 102 mpd ⊢φ→∑Gi=MN⦋i/k⦌C-˙⦋i+1/k⦌C=⦋M/k⦌C-˙⦋N+1/k⦌C