Theorem climresmpt

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

	Ref	Expression
Hypotheses	climresmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climresmpt.f	$$⊢F=\left(x\in Z⟼A\right)$$
	climresmpt.n	$$⊢\phi \to N\in Z$$
	climresmpt.g	$$⊢G=\left(x\in {\mathbb{Z}}_{\ge N}⟼A\right)$$
Assertion	climresmpt	$$⊢\phi \to \left(G⇝B\leftrightarrow F⇝B\right)$$

Proof

Step	Hyp	Ref	Expression
1		climresmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climresmpt.f	$$⊢F=\left(x\in Z⟼A\right)$$
3		climresmpt.n	$$⊢\phi \to N\in Z$$
4		climresmpt.g	$$⊢G=\left(x\in {\mathbb{Z}}_{\ge N}⟼A\right)$$
5	2	reseq1i	$$⊢{F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}={\left(x\in Z⟼A\right)\upharpoonright }_{{\mathbb{Z}}_{\ge N}}$$
6	5	a1i	$$⊢\phi \to {F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}={\left(x\in Z⟼A\right)\upharpoonright }_{{\mathbb{Z}}_{\ge N}}$$
7	3 1	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
8		uzss	$$⊢N\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
9	7 8	syl	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
10	9 1	sseqtrrdi	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq Z$$
11		resmpt	$$⊢{\mathbb{Z}}_{\ge N}\subseteq Z\to {\left(x\in Z⟼A\right)\upharpoonright }_{{\mathbb{Z}}_{\ge N}}=\left(x\in {\mathbb{Z}}_{\ge N}⟼A\right)$$
12	10 11	syl	$$⊢\phi \to {\left(x\in Z⟼A\right)\upharpoonright }_{{\mathbb{Z}}_{\ge N}}=\left(x\in {\mathbb{Z}}_{\ge N}⟼A\right)$$
13	4	eqcomi	$$⊢\left(x\in {\mathbb{Z}}_{\ge N}⟼A\right)=G$$
14	13	a1i	$$⊢\phi \to \left(x\in {\mathbb{Z}}_{\ge N}⟼A\right)=G$$
15	6 12 14	3eqtrrd	$$⊢\phi \to G={F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}$$
16	15	breq1d	$$⊢\phi \to \left(G⇝B\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)⇝B\right)$$
17		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
18	7 17	syl	$$⊢\phi \to N\in \mathbb{Z}$$
19	1	fvexi	$$⊢Z\in \mathrm{V}$$
20	19	mptex	$$⊢\left(x\in Z⟼A\right)\in \mathrm{V}$$
21	20	a1i	$$⊢\phi \to \left(x\in Z⟼A\right)\in \mathrm{V}$$
22	2 21	eqeltrid	$$⊢\phi \to F\in \mathrm{V}$$
23		climres	$$⊢\left(N\in \mathbb{Z}\wedge F\in \mathrm{V}\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)⇝B\leftrightarrow F⇝B\right)$$
24	18 22 23	syl2anc	$$⊢\phi \to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge N}}\right)⇝B\leftrightarrow F⇝B\right)$$
25	16 24	bitrd	$$⊢\phi \to \left(G⇝B\leftrightarrow F⇝B\right)$$