Metamath Proof Explorer

Theorem gsummulsubdishift1

Description: Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummulsubdishift.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
gsummulsubdishift.p ⊢ + = ( +g ‘ 𝑅 )
gsummulsubdishift.m ⊢ − = ( -g ‘ 𝑅 )
gsummulsubdishift.t ⊢ · = ( .r ‘ 𝑅 )
gsummulsubdishift.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
gsummulsubdishift.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
gsummulsubdishift.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
gsummulsubdishift.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
gsummulsubdishift.d ⊢ ( 𝜑 → 𝐷 : ( 0 ... 𝑁 ) ⟶ 𝐵 )
gsummulsubdishift1.e ⊢ ( 𝜑 → 𝐸 = ( ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) − ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) )
gsummulsubdishift1.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 = ( ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) )
Assertion gsummulsubdishift1 ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )

Proof

Step Hyp Ref Expression
1 gsummulsubdishift.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 gsummulsubdishift.p ⊢ + = ( +g ‘ 𝑅 )
3 gsummulsubdishift.m ⊢ − = ( -g ‘ 𝑅 )
4 gsummulsubdishift.t ⊢ · = ( .r ‘ 𝑅 )
5 gsummulsubdishift.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 gsummulsubdishift.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 gsummulsubdishift.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
8 gsummulsubdishift.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 gsummulsubdishift.d ⊢ ( 𝜑 → 𝐷 : ( 0 ... 𝑁 ) ⟶ 𝐵 )
10 gsummulsubdishift1.e ⊢ ( 𝜑 → 𝐸 = ( ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) − ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) )
11 gsummulsubdishift1.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 = ( ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) )
12 5 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
13 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
14 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ 𝐵 )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐷 ‘ 𝑘 ) ∈ 𝐵 )
16 1 12 13 15 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) ∈ 𝐵 )
17 1 4 3 5 16 6 7 ringsubdi ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · ( 𝐴 − 𝐶 ) ) = ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐴 ) − ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐶 ) ) )
18 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
19 8 18 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
20 fzisfzounsn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 𝑁 ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
21 19 20 syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
22 21 mpteq1d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) = ( 𝑘 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) )
23 22 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) )
24 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
25 eqid ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) )
26 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
27 25 13 14 26 fsuppmptdm ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) finSupp ( 0g ‘ 𝑅 ) )
28 1 24 4 5 13 6 14 27 gsummulc1 ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐴 ) )
29 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
30 29 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
31 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ Ring )
32 fzossfz ⊢ ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 )
33 32 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
34 33 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
35 34 14 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ 𝐵 )
36 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ 𝐵 )
37 1 4 31 35 36 ringcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ∈ 𝐵 )
38 fzonel ⊢ ¬ 𝑁 ∈ ( 0 ..^ 𝑁 )
39 38 a1i ⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 0 ..^ 𝑁 ) )
40 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
41 8 40 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
42 9 41 ffvelcdmd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ 𝐵 )
43 1 4 5 42 6 ringcld ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) ∈ 𝐵 )
44 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐷 ‘ 𝑘 ) = ( 𝐷 ‘ 𝑁 ) )
45 44 oveq1d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) = ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) )
46 1 2 12 30 37 8 39 43 45 gsumunsn ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) + ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) ) )
47 23 28 46 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐴 ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) + ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) ) )
48 1 24 4 5 13 7 14 27 gsummulc1 ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐶 ) )
49 fz0sn0fz1 ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
50 8 49 syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( { 0 } ∪ ( 1 ... 𝑁 ) ) )
51 uncom ⊢ ( ( 1 ... 𝑁 ) ∪ { 0 } ) = ( { 0 } ∪ ( 1 ... 𝑁 ) )
52 50 51 eqtr4di ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 1 ... 𝑁 ) ∪ { 0 } ) )
53 52 mpteq1d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) = ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∪ { 0 } ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) )
54 53 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∪ { 0 } ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) )
55 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
56 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑅 ∈ Ring )
57 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
58 57 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
59 58 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
60 59 14 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ 𝐵 )
61 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ 𝐵 )
62 1 4 56 60 61 ringcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ∈ 𝐵 )
63 c0ex ⊢ 0 ∈ V
64 63 a1i ⊢ ( 𝜑 → 0 ∈ V )
65 0nnn ⊢ ¬ 0 ∈ ℕ
66 elfznn ⊢ ( 0 ∈ ( 1 ... 𝑁 ) → 0 ∈ ℕ )
67 65 66 mto ⊢ ¬ 0 ∈ ( 1 ... 𝑁 )
68 67 a1i ⊢ ( 𝜑 → ¬ 0 ∈ ( 1 ... 𝑁 ) )
69 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
70 8 69 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
71 9 70 ffvelcdmd ⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) ∈ 𝐵 )
72 1 4 5 71 7 ringcld ⊢ ( 𝜑 → ( ( 𝐷 ‘ 0 ) · 𝐶 ) ∈ 𝐵 )
73 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐷 ‘ 𝑘 ) = ( 𝐷 ‘ 0 ) )
74 73 oveq1d ⊢ ( 𝑘 = 0 → ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) = ( ( 𝐷 ‘ 0 ) · 𝐶 ) )
75 1 2 12 55 62 64 68 72 74 gsumunsn ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∪ { 0 } ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) )
76 nfcv ⊢ Ⅎ 𝑘 ( ( 𝐷 ‘ ( 𝑙 + 1 ) ) · 𝐶 )
77 fveq2 ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( 𝐷 ‘ 𝑘 ) = ( 𝐷 ‘ ( 𝑙 + 1 ) ) )
78 77 oveq1d ⊢ ( 𝑘 = ( 𝑙 + 1 ) → ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) = ( ( 𝐷 ‘ ( 𝑙 + 1 ) ) · 𝐶 ) )
79 ssidd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
80 8 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
81 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
82 80 81 syl ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
83 82 eleq2d ⊢ ( 𝜑 → ( 𝑙 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
84 83 biimpar ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑙 ∈ ( 0 ..^ 𝑁 ) )
85 fz0add1fz1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑙 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) )
86 8 84 85 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑙 + 1 ) ∈ ( 1 ... 𝑁 ) )
87 59 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
88 80 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
89 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ( 1 ... 𝑁 ) )
90 elfzm1b ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑘 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
91 90 biimpa ⊢ ( ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
92 87 88 89 91 syl21anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
93 eqcom ⊢ ( ( 𝑙 + 1 ) = 𝑘 ↔ 𝑘 = ( 𝑙 + 1 ) )
94 elfznn0 ⊢ ( 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑙 ∈ ℕ0 )
95 94 nn0cnd ⊢ ( 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑙 ∈ ℂ )
96 95 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑙 ∈ ℂ )
97 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
98 87 zcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
99 98 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
100 96 97 99 addlsub ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑙 + 1 ) = 𝑘 ↔ 𝑙 = ( 𝑘 − 1 ) ) )
101 93 100 bitr3id ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 = ( 𝑙 + 1 ) ↔ 𝑙 = ( 𝑘 − 1 ) ) )
102 92 101 reu6dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ∃! 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑘 = ( 𝑙 + 1 ) )
103 76 1 24 78 12 55 79 62 86 102 gsummptf1o ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝐷 ‘ ( 𝑙 + 1 ) ) · 𝐶 ) ) ) )
104 fvoveq1 ⊢ ( 𝑙 = 𝑘 → ( 𝐷 ‘ ( 𝑙 + 1 ) ) = ( 𝐷 ‘ ( 𝑘 + 1 ) ) )
105 104 oveq1d ⊢ ( 𝑙 = 𝑘 → ( ( 𝐷 ‘ ( 𝑙 + 1 ) ) · 𝐶 ) = ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) )
106 105 cbvmptv ⊢ ( 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝐷 ‘ ( 𝑙 + 1 ) ) · 𝐶 ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) )
107 82 mpteq1d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) = ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) )
108 106 107 eqtr4id ⊢ ( 𝜑 → ( 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝐷 ‘ ( 𝑙 + 1 ) ) · 𝐶 ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) )
109 108 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ( ( 𝐷 ‘ ( 𝑙 + 1 ) ) · 𝐶 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) )
110 103 109 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) )
111 110 oveq1d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) )
112 54 75 111 3eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) )
113 48 112 eqtr3d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐶 ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) )
114 47 113 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐴 ) − ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · 𝐶 ) ) = ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) + ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) ) − ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) ) )
115 5 ringabld ⊢ ( 𝜑 → 𝑅 ∈ Abel )
116 37 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ∈ 𝐵 )
117 1 12 30 116 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) ∈ 𝐵 )
118 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 : ( 0 ... 𝑁 ) ⟶ 𝐵 )
119 fz0add1fz1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝑁 ) )
120 8 119 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 1 ... 𝑁 ) )
121 57 120 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
122 118 121 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑘 + 1 ) ) ∈ 𝐵 )
123 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ 𝐵 )
124 1 4 31 122 123 ringcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ∈ 𝐵 )
125 124 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ∈ 𝐵 )
126 1 12 30 125 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ∈ 𝐵 )
127 1 2 3 ablsub4 ⊢ ( ( 𝑅 ∈ Abel ∧ ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) ∈ 𝐵 ) ∧ ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 0 ) · 𝐶 ) ∈ 𝐵 ) ) → ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) + ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) ) − ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) ) = ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) − ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) + ( ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) − ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) ) )
128 115 117 43 126 72 127 syl122anc ⊢ ( 𝜑 → ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) + ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) ) − ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) + ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) ) = ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) − ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) + ( ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) − ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) ) )
129 17 114 128 3eqtrd ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · ( 𝐴 − 𝐶 ) ) = ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) − ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) + ( ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) − ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) ) )
130 9 feqmptd ⊢ ( 𝜑 → 𝐷 = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) )
131 130 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg 𝐷 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) )
132 131 oveq1d ⊢ ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝐷 ‘ 𝑘 ) ) ) · ( 𝐴 − 𝐶 ) ) )
133 11 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) )
134 133 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) )
135 eqid ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) )
136 eqid ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) )
137 1 3 115 30 37 124 135 136 gsummptfidmsub ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) − ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) )
138 134 137 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) − ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) )
139 138 10 oveq12d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) = ( ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ 𝑘 ) · 𝐴 ) ) ) − ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐶 ) ) ) ) + ( ( ( 𝐷 ‘ 𝑁 ) · 𝐴 ) − ( ( 𝐷 ‘ 0 ) · 𝐶 ) ) ) )
140 129 132 139 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )