Theorem climconst2

Description: A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climconst2.1	$$⊢{\mathbb{Z}}_{\ge M}\subseteq Z$$
	climconst2.2	$$⊢Z\in \mathrm{V}$$
Assertion	climconst2	$$⊢\left(A\in ℂ\wedge M\in \mathbb{Z}\right)\to \left(Z\times \left\{A\right\}\right)⇝A$$

Proof

Step	Hyp	Ref	Expression
1		climconst2.1	$$⊢{\mathbb{Z}}_{\ge M}\subseteq Z$$
2		climconst2.2	$$⊢Z\in \mathrm{V}$$
3		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
4		simpr	$$⊢\left(A\in ℂ\wedge M\in \mathbb{Z}\right)\to M\in \mathbb{Z}$$
5		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
6	2 5	xpex	$$⊢Z\times \left\{A\right\}\in \mathrm{V}$$
7	6	a1i	$$⊢\left(A\in ℂ\wedge M\in \mathbb{Z}\right)\to Z\times \left\{A\right\}\in \mathrm{V}$$
8		simpl	$$⊢\left(A\in ℂ\wedge M\in \mathbb{Z}\right)\to A\in ℂ$$
9	1	sseli	$$⊢k\in {\mathbb{Z}}_{\ge M}\to k\in Z$$
10		fvconst2g	$$⊢\left(A\in ℂ\wedge k\in Z\right)\to \left(Z\times \left\{A\right\}\right)\left(k\right)=A$$
11	8 9 10	syl2an	$$⊢\left(\left(A\in ℂ\wedge M\in \mathbb{Z}\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to \left(Z\times \left\{A\right\}\right)\left(k\right)=A$$
12	3 4 7 8 11	climconst	$$⊢\left(A\in ℂ\wedge M\in \mathbb{Z}\right)\to \left(Z\times \left\{A\right\}\right)⇝A$$