Theorem climres

Description: A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
2		resexg	$$⊢F\in V\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{V}$$
3	2	adantl	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{V}$$
4		simpr	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to F\in V$$
5		simpl	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to M\in \mathbb{Z}$$
6		fvres	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\left(k\right)=F\left(k\right)$$
7	6	adantl	$$⊢\left(\left(M\in \mathbb{Z}\wedge F\in V\right)\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\left(k\right)=F\left(k\right)$$
8	1 3 4 5 7	climeq	$$⊢\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)$$