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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = 𝐵 )