Theorem xlimconst2

Description: A sequence that eventually becomes constant, converges to its constant value (w.r.t. the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimconst2.p	$$⊢Ⅎk\phi$$
	xlimconst2.k	$$⊢\underset{\_}{Ⅎ}kF$$
	xlimconst2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimconst2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
	xlimconst2.n	$$⊢\phi \to N\in Z$$
	xlimconst2.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	xlimconst2.e	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to F\left(k\right)=A$$
Assertion	xlimconst2	$$⊢\phi \to F\underset{*}{⇝}A$$

Proof

Step	Hyp	Ref	Expression
1		xlimconst2.p	$$⊢Ⅎk\phi$$
2		xlimconst2.k	$$⊢\underset{\_}{Ⅎ}kF$$
3		xlimconst2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		xlimconst2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5		xlimconst2.n	$$⊢\phi \to N\in Z$$
6		xlimconst2.a	$$⊢\phi \to A\in {ℝ}^{*}$$
7		xlimconst2.e	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to F\left(k\right)=A$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}k{\mathbb{Z}}_{\ge N}$$
9	2 8	nfres	$$⊢\underset{\_}{Ⅎ}k\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)$$
10	3 5	eluzelz2d	$$⊢\phi \to N\in \mathbb{Z}$$
11		eqid	$$⊢{\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge N}$$
12	4	ffnd	$$⊢\phi \to FFnZ$$
13	3 5	uzssd2	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq Z$$
14	12 13	fnssresd	$$⊢\phi \to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)Fn{\mathbb{Z}}_{\ge N}$$
15		fvres	$$⊢k\in {\mathbb{Z}}_{\ge N}\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)\left(k\right)=F\left(k\right)$$
16	15	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)\left(k\right)=F\left(k\right)$$
17	16 7	eqtrd	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)\left(k\right)=A$$
18	1 9 10 11 14 6 17	xlimconst	$$⊢\phi \to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)\underset{*}{⇝}A$$
19	3 4	fuzxrpmcn	$$⊢\phi \to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
20	19 10	xlimres	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)\underset{*}{⇝}A\right)$$
21	18 20	mpbird	$$⊢\phi \to F\underset{*}{⇝}A$$