This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem telfsumo

Description: Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses telfsumo.1 ⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
telfsumo.2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
telfsumo.3 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
telfsumo.4 ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐸 )
telfsumo.5 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
telfsumo.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
Assertion telfsumo ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐸 ) )

Proof

Step Hyp Ref Expression
1 telfsumo.1 ⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
2 telfsumo.2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
3 telfsumo.3 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
4 telfsumo.4 ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐸 )
5 telfsumo.5 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 telfsumo.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
7 sum0 ⊢ Σ 𝑗 ∈ ∅ ( 𝐵 − 𝐶 ) = 0
8 3 eleq1d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∈ ℂ ↔ 𝐷 ∈ ℂ ) )
9 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
10 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
11 5 10 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
12 8 9 11 rspcdva ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → 𝐷 ∈ ℂ )
14 13 subidd ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( 𝐷 − 𝐷 ) = 0 )
15 7 14 eqtr4id ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → Σ 𝑗 ∈ ∅ ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐷 ) )
16 oveq2 ⊢ ( 𝑁 = 𝑀 → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ..^ 𝑀 ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ..^ 𝑀 ) )
18 fzo0 ⊢ ( 𝑀 ..^ 𝑀 ) = ∅
19 17 18 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( 𝑀 ..^ 𝑁 ) = ∅ )
20 19 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 − 𝐶 ) = Σ 𝑗 ∈ ∅ ( 𝐵 − 𝐶 ) )
21 eqeq1 ⊢ ( 𝑘 = 𝑁 → ( 𝑘 = 𝑀 ↔ 𝑁 = 𝑀 ) )
22 4 eqeq1d ⊢ ( 𝑘 = 𝑁 → ( 𝐴 = 𝐷 ↔ 𝐸 = 𝐷 ) )
23 21 22 imbi12d ⊢ ( 𝑘 = 𝑁 → ( ( 𝑘 = 𝑀 → 𝐴 = 𝐷 ) ↔ ( 𝑁 = 𝑀 → 𝐸 = 𝐷 ) ) )
24 23 3 vtoclg ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 → 𝐸 = 𝐷 ) )
25 24 imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → 𝐸 = 𝐷 )
26 5 25 sylan ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → 𝐸 = 𝐷 )
27 26 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( 𝐷 − 𝐸 ) = ( 𝐷 − 𝐷 ) )
28 15 20 27 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐸 ) )
29 fzofi ⊢ ( 𝑀 ..^ 𝑁 ) ∈ Fin
30 29 a1i ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ∈ Fin )
31 1 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
32 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
33 elfzofz ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
34 33 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
35 31 32 34 rspcdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ )
36 2 eleq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
37 fzofzp1 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
39 36 32 38 rspcdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐶 ∈ ℂ )
40 30 35 39 fsumsub ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 − 𝐶 ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐵 − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐶 ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 − 𝐶 ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐵 − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐶 ) )
42 1 cbvsumv ⊢ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐵
43 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
44 5 43 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
45 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
46 44 45 sylan ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
47 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
48 5 47 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 ∈ ℤ )
50 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
51 49 50 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
52 fzossfz ⊢ ( 𝑀 ..^ 𝑁 ) ⊆ ( 𝑀 ... 𝑁 )
53 51 52 eqsstrrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 ... ( 𝑁 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
54 53 sselda ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
55 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
56 54 55 syldan ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
57 46 56 3 fsum1p ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 = ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 ) )
58 51 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 )
59 fzoval ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ..^ 𝑁 ) = ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) )
60 49 59 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) ..^ 𝑁 ) = ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) )
61 60 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 )
62 61 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) = ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 ) )
63 57 58 62 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) )
64 42 63 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐵 = ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) )
65 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
66 fzp1ss ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
67 44 66 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
68 67 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
69 68 6 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝐴 ∈ ℂ )
70 69 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝐴 ∈ ℂ )
71 65 70 4 fsumm1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 + 𝐸 ) )
72 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
73 44 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
74 72 73 48 69 2 fsumshftm ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 = Σ 𝑗 ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) 𝐶 )
75 44 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
76 ax-1cn ⊢ 1 ∈ ℂ
77 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
78 75 76 77 sylancl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
79 78 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
80 48 50 syl ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
81 79 80 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) = ( 𝑀 ..^ 𝑁 ) )
82 81 sumeq1d ⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) 𝐶 = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐶 )
83 74 82 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐶 )
84 83 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐶 )
85 48 59 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ..^ 𝑁 ) = ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) )
86 85 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 )
87 86 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 + 𝐸 ) = ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 + 𝐸 ) )
88 fzofi ⊢ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∈ Fin
89 88 a1i ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∈ Fin )
90 elfzofz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
91 90 69 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
92 89 91 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ∈ ℂ )
93 4 eleq1d ⊢ ( 𝑘 = 𝑁 → ( 𝐴 ∈ ℂ ↔ 𝐸 ∈ ℂ ) )
94 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
95 5 94 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
96 93 9 95 rspcdva ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
97 92 96 addcomd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 + 𝐸 ) = ( 𝐸 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) )
98 87 97 eqtr3d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 + 𝐸 ) = ( 𝐸 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) 𝐴 + 𝐸 ) = ( 𝐸 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) )
100 71 84 99 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐶 = ( 𝐸 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) )
101 64 100 oveq12d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐵 − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) 𝐶 ) = ( ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) − ( 𝐸 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) ) )
102 12 96 92 pnpcan2d ⊢ ( 𝜑 → ( ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) − ( 𝐸 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) ) = ( 𝐷 − 𝐸 ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐷 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) − ( 𝐸 + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) 𝐴 ) ) = ( 𝐷 − 𝐸 ) )
104 41 101 103 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐸 ) )
105 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
106 5 105 syl ⊢ ( 𝜑 → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
107 28 104 106 mpjaodan ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐸 ) )