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\in \mathbb{Z}\to seqM\left(+,\left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\right)⇝0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
2	1	ser0f	$$⊢M\in \mathbb{Z}\to seqM\left(+,\left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\right)={\mathbb{Z}}_{\ge M}\times \left\{0\right\}$$
3		0cn	$$⊢0\in ℂ$$
4		ssid	$$⊢{\mathbb{Z}}_{\ge M}\subseteq {\mathbb{Z}}_{\ge M}$$
5		fvex	$$⊢{\mathbb{Z}}_{\ge M}\in \mathrm{V}$$
6	4 5	climconst2	$$⊢\left(0\in ℂ\wedge M\in \mathbb{Z}\right)\to \left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)⇝0$$
7	3 6	mpan	$$⊢M\in \mathbb{Z}\to \left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)⇝0$$
8	2 7	eqbrtrd	$$⊢M\in \mathbb{Z}\to seqM\left(+,\left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\right)⇝0$$