Theorem xlimconst

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

	Ref	Expression
Hypotheses	xlimconst.p	⊢ Ⅎ 𝑘 𝜑
	xlimconst.k	⊢ Ⅎ 𝑘 𝐹
	xlimconst.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	xlimconst.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	xlimconst.f	⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
	xlimconst.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xlimconst.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
Assertion	xlimconst	⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		xlimconst.p	⊢ Ⅎ 𝑘 𝜑
2		xlimconst.k	⊢ Ⅎ 𝑘 𝐹
3		xlimconst.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		xlimconst.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		xlimconst.f	⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
6		xlimconst.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
7		xlimconst.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
8	1 2 5 6 7	fconst7	⊢ ( 𝜑 → 𝐹 = ( 𝑍 × { 𝐴 } ) )
9		letopon	⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
10	4	lmconst	⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ 𝐴 ∈ ℝ* ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝐴 } ) ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 )
11	9 6 3 10	mp3an2i	⊢ ( 𝜑 → ( 𝑍 × { 𝐴 } ) ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 )
12	8 11	eqbrtrd	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 )
13		df-xlim	⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )
14	13	breqi	⊢ ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 )
15	12 14	sylibr	⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )