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	$$⊢\phi \to M\in \mathbb{Z}$$
	climxlim.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climxlim.f	$$⊢\phi \to F:Z⟶ℝ$$
	climxlim.c	$$⊢\phi \to F⇝A$$
Assertion	climxlim	$$⊢\phi \to F\underset{*}{⇝}A$$

Proof

Step	Hyp	Ref	Expression
1		climxlim.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		climxlim.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		climxlim.f	$$⊢\phi \to F:Z⟶ℝ$$
4		climxlim.c	$$⊢\phi \to F⇝A$$
5	3	ffvelcdmda	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
6	2 1 4 5	climrecl	$$⊢\phi \to A\in ℝ$$
7	1 2 3 6	xlimclim	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$
8	4 7	mpbird	$$⊢\phi \to F\underset{*}{⇝}A$$