Metamath Proof Explorer


Theorem isumneg

Description: Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses isumneg.1 𝑍 = ( ℤ𝑀 )
isumneg.2 ( 𝜑𝑀 ∈ ℤ )
isumneg.3 ( 𝜑 → Σ 𝑘𝑍 𝐴 ∈ ℂ )
isumneg.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = 𝐴 )
isumneg.5 ( ( 𝜑𝑘𝑍 ) → 𝐴 ∈ ℂ )
isumneg.6 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion isumneg ( 𝜑 → Σ 𝑘𝑍 - 𝐴 = - Σ 𝑘𝑍 𝐴 )

Proof

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 ( 𝜑 → Σ 𝑘𝑍 - 𝐴 = - Σ 𝑘𝑍 𝐴 )