Theorem xlimclim

Description: Given a sequence of reals, it converges to a real number A w.r.t. the standard topology on the reals, if and only if it converges to A w.r.t. to the standard topology on the extended reals (see climreeq ). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimclim.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	xlimclim.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	xlimclim.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
	xlimclim.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion	xlimclim	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xlimclim.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		xlimclim.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		xlimclim.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4		xlimclim.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		df-xlim	⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )
6	5	breqi	⊢ ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 )
7	6	a1i	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 ) )
8		xrtgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
9		reex	⊢ ℝ ∈ V
10	9	a1i	⊢ ( 𝜑 → ℝ ∈ V )
11		letop	⊢ ( ordTop ‘ ≤ ) ∈ Top
12	11	a1i	⊢ ( 𝜑 → ( ordTop ‘ ≤ ) ∈ Top )
13	8 2 10 12 4 1 3	lmss	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
14		eqid	⊢ ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
15	14 2 1 3	climreeq	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
16	7 13 15	3bitrd	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )