Theorem climxlim

Description: A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		climxlim.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		climxlim.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		climxlim.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4		climxlim.c	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
5	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
6	2 1 4 5	climrecl	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7	1 2 3 6	xlimclim	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
8	4 7	mpbird	⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )