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	$$⊢\left(\mathbb{Z}\times \left\{0\right\}\right)⇝0$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		0z	$$⊢0\in \mathbb{Z}$$
3		uzssz	$$⊢{\mathbb{Z}}_{\ge 0}\subseteq \mathbb{Z}$$
4		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
5	3 4	climconst2	$$⊢\left(0\in ℂ\wedge 0\in \mathbb{Z}\right)\to \left(\mathbb{Z}\times \left\{0\right\}\right)⇝0$$
6	1 2 5	mp2an	$$⊢\left(\mathbb{Z}\times \left\{0\right\}\right)⇝0$$