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	⊢ Ⅎ 𝑘 𝜑
	xlimconst2.k	⊢ Ⅎ 𝑘 𝐹
	xlimconst2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	xlimconst2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
	xlimconst2.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
	xlimconst2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xlimconst2.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
Assertion	xlimconst2	⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		xlimconst2.p	⊢ Ⅎ 𝑘 𝜑
2		xlimconst2.k	⊢ Ⅎ 𝑘 𝐹
3		xlimconst2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		xlimconst2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5		xlimconst2.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
6		xlimconst2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
7		xlimconst2.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
8		nfcv	⊢ Ⅎ 𝑘 ( ℤ≥ ‘ 𝑁 )
9	2 8	nfres	⊢ Ⅎ 𝑘 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) )
10	3 5	eluzelz2d	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11		eqid	⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
12	4	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
13	3 5	uzssd2	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
14	12 13	fnssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) Fn ( ℤ≥ ‘ 𝑁 ) )
15		fvres	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
17	16 7	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ‘ 𝑘 ) = 𝐴 )
18	1 9 10 11 14 6 17	xlimconst	⊢ ( 𝜑 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ~~>* 𝐴 )
19	3 4	fuzxrpmcn	⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
20	19 10	xlimres	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑁 ) ) ~~>* 𝐴 ) )
21	18 20	mpbird	⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )