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	⊢ ( ℤ × { 0 } ) ⇝ 0

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		0z	⊢ 0 ∈ ℤ
3		uzssz	⊢ ( ℤ≥ ‘ 0 ) ⊆ ℤ
4		zex	⊢ ℤ ∈ V
5	3 4	climconst2	⊢ ( ( 0 ∈ ℂ ∧ 0 ∈ ℤ ) → ( ℤ × { 0 } ) ⇝ 0 )
6	1 2 5	mp2an	⊢ ( ℤ × { 0 } ) ⇝ 0