Theorem isumclim

Description: An infinite sum equals the value its series converges to. (Contributed by NM, 25-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		isumclim.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumclim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumclim.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumclim.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		isumclim.6	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐵 )
6	1 2 3 4	isum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
7		fclim	⊢ ⇝ : dom ⇝ ⟶ ℂ
8		ffun	⊢ ( ⇝ : dom ⇝ ⟶ ℂ → Fun ⇝ )
9	7 8	ax-mp	⊢ Fun ⇝
10		funbrfv	⊢ ( Fun ⇝ → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐵 → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) = 𝐵 ) )
11	9 5 10	mpsyl	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) = 𝐵 )
12	6 11	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = 𝐵 )