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