Theorem climresd

Description: A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	climresd.1	$$⊢\phi \to M\in \mathbb{Z}$$
	climresd.2	$$⊢\phi \to F\in V$$
Assertion	climresd	$$⊢\phi \to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝A\leftrightarrow F⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climresd.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		climresd.2	$$⊢\phi \to F\in V$$
3		climres	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝A\leftrightarrow F⇝A\right)$$
4	1 2 3	syl2anc	$$⊢\phi \to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝A\leftrightarrow F⇝A\right)$$