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 
|- Z = ( ZZ>= ` M )
isumclim.2 
|- ( ph -> M e. ZZ )
isumclim.3 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
isumclim.4 
|- ( ( ph /\ k e. Z ) -> A e. CC )
isumclim.6 
|- ( ph -> seq M ( + , F ) ~~> B )
Assertion isumclim 
|- ( ph -> sum_ k e. Z A = B )

Proof

Step Hyp Ref Expression
1 isumclim.1 
 |-  Z = ( ZZ>= ` M )
2 isumclim.2 
 |-  ( ph -> M e. ZZ )
3 isumclim.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4 isumclim.4 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
5 isumclim.6 
 |-  ( ph -> seq M ( + , F ) ~~> B )
6 1 2 3 4 isum 
 |-  ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
7 fclim 
 |-  ~~> : dom ~~> --> CC
8 ffun 
 |-  ( ~~> : dom ~~> --> CC -> Fun ~~> )
9 7 8 ax-mp 
 |-  Fun ~~>
10 funbrfv 
 |-  ( Fun ~~> -> ( seq M ( + , F ) ~~> B -> ( ~~> ` seq M ( + , F ) ) = B ) )
11 9 5 10 mpsyl 
 |-  ( ph -> ( ~~> ` seq M ( + , F ) ) = B )
12 6 11 eqtrd 
 |-  ( ph -> sum_ k e. Z A = B )