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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	isumcl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion	isumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		isumcl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6	1 2 3 4	isum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
7		fclim	⊢ ⇝ : dom ⇝ ⟶ ℂ
8		ffvelrn	⊢ ( ( ⇝ : dom ⇝ ⟶ ℂ ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ∈ ℂ )
9	7 5 8	sylancr	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ∈ ℂ )
10	6 9	eqeltrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ )