Theorem climconst

Description: An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climconst.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climconst.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climconst.3	$$⊢\phi \to F\in V$$
	climconst.4	$$⊢\phi \to A\in ℂ$$
	climconst.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
Assertion	climconst	$$⊢\phi \to F⇝A$$

Proof

Step	Hyp	Ref	Expression
1		climconst.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climconst.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climconst.3	$$⊢\phi \to F\in V$$
4		climconst.4	$$⊢\phi \to A\in ℂ$$
5		climconst.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
6		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
7	2 6	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
8	7 1	eleqtrrdi	$$⊢\phi \to M\in Z$$
9	4	subidd	$$⊢\phi \to A-A=0$$
10	9	fveq2d	$$⊢\phi \to \left|A-A\right|=\left|0\right|$$
11		abs0	$$⊢\left|0\right|=0$$
12	10 11	eqtrdi	$$⊢\phi \to \left|A-A\right|=0$$
13	12	adantr	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left|A-A\right|=0$$
14		rpgt0	$$⊢x\in {ℝ}^{+}\to 0<x$$
15	14	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to 0<x$$
16	13 15	eqbrtrd	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left|A-A\right|<x$$
17	16	ralrimivw	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \forall k\in Z\left|A-A\right|<x$$
18		fveq2	$$⊢j=M\to {\mathbb{Z}}_{\ge j}={\mathbb{Z}}_{\ge M}$$
19	18 1	eqtr4di	$$⊢j=M\to {\mathbb{Z}}_{\ge j}=Z$$
20	19	raleqdv	$$⊢j=M\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|A-A\right|<x\leftrightarrow \forall k\in Z\left|A-A\right|<x\right)$$
21	20	rspcev	$$⊢\left(M\in Z\wedge \forall k\in Z\left|A-A\right|<x\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|A-A\right|<x$$
22	8 17 21	syl2an2r	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|A-A\right|<x$$
23	22	ralrimiva	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|A-A\right|<x$$
24	4	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
25	1 2 3 5 4 24	clim2c	$$⊢\phi \to \left(F⇝A\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|A-A\right|<x\right)$$
26	23 25	mpbird	$$⊢\phi \to F⇝A$$