Theorem xlimclim2

Description: Given a sequence of extended reals, it converges to a real number A w.r.t. the standard topology on the reals (see climreeq ), if and only if it converges to A w.r.t. to the standard topology on the extended reals. In order for the first part of the statement to even make sense, the sequence will of course eventually become (and stay) real: showing this, is the key step of the proof. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		xlimclim2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		xlimclim2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		xlimclim2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4		xlimclim2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → 𝐹 ~~>* 𝐴 )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → 𝐹 : 𝑍 ⟶ ℝ* )
7	4	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → 𝐴 ∈ ℝ )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → 𝑀 ∈ ℤ )
9	8 2 6 7 5	xlimxrre	⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
10	2 6 7 9	xlimclim2lem	⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
11	5 10	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → 𝐹 ⇝ 𝐴 )
12		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ⇝ 𝐴 )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 : 𝑍 ⟶ ℝ* )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐴 ∈ ℝ )
15	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝑀 ∈ ℤ )
16	15 2 13 14 12	climxrre	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
17	2 13 14 16	xlimclim2lem	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
18	12 17	mpbird	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ~~>* 𝐴 )
19	11 18	impbida	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )