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

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