Theorem isumclim2

Description: A converging series converges to its infinite sum. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	isumclim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumclim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumclim.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumclim.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	isumclim2.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion	isumclim2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		isumclim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumclim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumclim.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumclim.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		isumclim2.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6		climdm	⊢ ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
7	5 6	sylib	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
8	1 2 3 4	isum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
9	7 8	breqtrrd	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )