Step |
Hyp |
Ref |
Expression |
1 |
|
telfsumo.1 |
⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 ) |
2 |
|
telfsumo.2 |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 ) |
3 |
|
telfsumo.3 |
⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 ) |
4 |
|
telfsumo.4 |
⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐸 ) |
5 |
|
telfsumo.5 |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
6 |
|
telfsumo.6 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ ) |
7 |
1
|
negeqd |
⊢ ( 𝑘 = 𝑗 → - 𝐴 = - 𝐵 ) |
8 |
2
|
negeqd |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → - 𝐴 = - 𝐶 ) |
9 |
3
|
negeqd |
⊢ ( 𝑘 = 𝑀 → - 𝐴 = - 𝐷 ) |
10 |
4
|
negeqd |
⊢ ( 𝑘 = 𝑁 → - 𝐴 = - 𝐸 ) |
11 |
6
|
negcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → - 𝐴 ∈ ℂ ) |
12 |
7 8 9 10 5 11
|
telfsumo |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( - 𝐵 − - 𝐶 ) = ( - 𝐷 − - 𝐸 ) ) |
13 |
6
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ ) |
14 |
|
elfzofz |
⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) |
15 |
1
|
eleq1d |
⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ ) ) |
16 |
15
|
rspccva |
⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐵 ∈ ℂ ) |
17 |
13 14 16
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ ) |
18 |
|
fzofzp1 |
⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) |
19 |
2
|
eleq1d |
⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 ∈ ℂ ↔ 𝐶 ∈ ℂ ) ) |
20 |
19
|
rspccva |
⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ ∧ ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐶 ∈ ℂ ) |
21 |
13 18 20
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐶 ∈ ℂ ) |
22 |
17 21
|
neg2subd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( - 𝐵 − - 𝐶 ) = ( 𝐶 − 𝐵 ) ) |
23 |
22
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( - 𝐵 − - 𝐶 ) = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 − 𝐵 ) ) |
24 |
3
|
eleq1d |
⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∈ ℂ ↔ 𝐷 ∈ ℂ ) ) |
25 |
|
eluzfz1 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) |
26 |
5 25
|
syl |
⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) |
27 |
24 13 26
|
rspcdva |
⊢ ( 𝜑 → 𝐷 ∈ ℂ ) |
28 |
4
|
eleq1d |
⊢ ( 𝑘 = 𝑁 → ( 𝐴 ∈ ℂ ↔ 𝐸 ∈ ℂ ) ) |
29 |
|
eluzfz2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) |
30 |
5 29
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) |
31 |
28 13 30
|
rspcdva |
⊢ ( 𝜑 → 𝐸 ∈ ℂ ) |
32 |
27 31
|
neg2subd |
⊢ ( 𝜑 → ( - 𝐷 − - 𝐸 ) = ( 𝐸 − 𝐷 ) ) |
33 |
12 23 32
|
3eqtr3d |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 − 𝐵 ) = ( 𝐸 − 𝐷 ) ) |