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

Metamath Proof Explorer

Theorem isumcl

Description: The sum of a converging infinite series is a complex number. (Contributed by NM, 13-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses isumcl.1 ⊢ Z = ℤ ≥ M
isumcl.2 ⊢ φ → M ∈ ℤ
isumcl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
isumcl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
isumcl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
Assertion isumcl ⊢ φ → ∑ k ∈ Z A ∈ ℂ

Proof

Step Hyp Ref Expression
1 isumcl.1 ⊢ Z = ℤ ≥ M
2 isumcl.2 ⊢ φ → M ∈ ℤ
3 isumcl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
4 isumcl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
5 isumcl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
6 1 2 3 4 isum ⊢ φ → ∑ k ∈ Z A = ⇝ ⁡ seq M + F
7 fclim ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ
8 ffvelcdm ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ ∧ seq M + F ∈ dom ⁡ ⇝ → ⇝ ⁡ seq M + F ∈ ℂ
9 7 5 8 sylancr ⊢ φ → ⇝ ⁡ seq M + F ∈ ℂ
10 6 9 eqeltrd ⊢ φ → ∑ k ∈ Z A ∈ ℂ