Metamath Proof Explorer

Theorem serclim0

Description: The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008) (Proof shortened by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion serclim0 
|- ( M e. ZZ -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
2 1 ser0f 
 |-  ( M e. ZZ -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) = ( ( ZZ>= ` M ) X. { 0 } ) )
3 0cn 
 |-  0 e. CC
4 ssid 
 |-  ( ZZ>= ` M ) C_ ( ZZ>= ` M )
5 fvex 
 |-  ( ZZ>= ` M ) e. _V
6 4 5 climconst2 
 |-  ( ( 0 e. CC /\ M e. ZZ ) -> ( ( ZZ>= ` M ) X. { 0 } ) ~~> 0 )
7 3 6 mpan 
 |-  ( M e. ZZ -> ( ( ZZ>= ` M ) X. { 0 } ) ~~> 0 )
8 2 7 eqbrtrd 
 |-  ( M e. ZZ -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )