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 ⊢ Z = ℤ ≥ M
isumneg.2 ⊢ φ → M ∈ ℤ
isumneg.3 ⊢ φ → ∑ k ∈ Z A ∈ ℂ
isumneg.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
isumneg.5 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
isumneg.6 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
Assertion isumneg ⊢ φ → ∑ k ∈ Z − A = − ∑ k ∈ Z A

Proof

Step Hyp Ref Expression
1 isumneg.1 ⊢ Z = ℤ ≥ M
2 isumneg.2 ⊢ φ → M ∈ ℤ
3 isumneg.3 ⊢ φ → ∑ k ∈ Z A ∈ ℂ
4 isumneg.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
5 isumneg.5 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
6 isumneg.6 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
7 5 mulm1d ⊢ φ ∧ k ∈ Z → -1 ⁢ A = − A
8 7 eqcomd ⊢ φ ∧ k ∈ Z → − A = -1 ⁢ A
9 8 sumeq2dv ⊢ φ → ∑ k ∈ Z − A = ∑ k ∈ Z -1 ⁢ A
10 1cnd ⊢ φ → 1 ∈ ℂ
11 10 negcld ⊢ φ → − 1 ∈ ℂ
12 1 2 4 5 6 11 isummulc2 ⊢ φ → -1 ⁢ ∑ k ∈ Z A = ∑ k ∈ Z -1 ⁢ A
13 3 mulm1d ⊢ φ → -1 ⁢ ∑ k ∈ Z A = − ∑ k ∈ Z A
14 9 12 13 3eqtr2d ⊢ φ → ∑ k ∈ Z − A = − ∑ k ∈ Z A