Metamath Proof Explorer

Theorem climz

Description: The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion climz 
|- ( ZZ X. { 0 } ) ~~> 0

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 0z 
 |-  0 e. ZZ
3 uzssz 
 |-  ( ZZ>= ` 0 ) C_ ZZ
4 zex 
 |-  ZZ e. _V
5 3 4 climconst2 
 |-  ( ( 0 e. CC /\ 0 e. ZZ ) -> ( ZZ X. { 0 } ) ~~> 0 )
6 1 2 5 mp2an 
 |-  ( ZZ X. { 0 } ) ~~> 0