Step |
Hyp |
Ref |
Expression |
1 |
|
isumneg.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
isumneg.2 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
3 |
|
isumneg.3 |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ ) |
4 |
|
isumneg.4 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 ) |
5 |
|
isumneg.5 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ ) |
6 |
|
isumneg.6 |
⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) |
7 |
5
|
mulm1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( - 1 · 𝐴 ) = - 𝐴 ) |
8 |
7
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - 𝐴 = ( - 1 · 𝐴 ) ) |
9 |
8
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 - 𝐴 = Σ 𝑘 ∈ 𝑍 ( - 1 · 𝐴 ) ) |
10 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
11 |
10
|
negcld |
⊢ ( 𝜑 → - 1 ∈ ℂ ) |
12 |
1 2 4 5 6 11
|
isummulc2 |
⊢ ( 𝜑 → ( - 1 · Σ 𝑘 ∈ 𝑍 𝐴 ) = Σ 𝑘 ∈ 𝑍 ( - 1 · 𝐴 ) ) |
13 |
3
|
mulm1d |
⊢ ( 𝜑 → ( - 1 · Σ 𝑘 ∈ 𝑍 𝐴 ) = - Σ 𝑘 ∈ 𝑍 𝐴 ) |
14 |
9 12 13
|
3eqtr2d |
⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 - 𝐴 = - Σ 𝑘 ∈ 𝑍 𝐴 ) |