Theorem climresdm

Description: A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023)

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

Proof

Step	Hyp	Ref	Expression
1		climresdm.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		climresdm.2	$$⊢\phi \to F\in V$$
3		resexg	$$⊢F\in \mathrm{dom}⇝\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{V}$$
4	3	adantl	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{V}$$
5		fvexd	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to ⇝\left(F\right)\in \mathrm{V}$$
6		climdm	$$⊢F\in \mathrm{dom}⇝\leftrightarrow F⇝⇝\left(F\right)$$
7	6	biimpi	$$⊢F\in \mathrm{dom}⇝\to F⇝⇝\left(F\right)$$
8	7	adantl	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to F⇝⇝\left(F\right)$$
9	1	adantr	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to M\in \mathbb{Z}$$
10		simpr	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to F\in \mathrm{dom}⇝$$
11	9 10	climresd	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝⇝\left(F\right)\leftrightarrow F⇝⇝\left(F\right)\right)$$
12	8 11	mpbird	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝⇝\left(F\right)$$
13	4 5 12	breldmd	$$⊢\left(\phi \wedge F\in \mathrm{dom}⇝\right)\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝$$
14	2	adantr	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)\to F\in V$$
15		fvexd	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)\to ⇝\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\in \mathrm{V}$$
16		climdm	$$⊢{F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝⇝\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
17	16	biimpi	$$⊢{F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝⇝\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
18	17	adantl	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝⇝\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
19	1	adantr	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)\to M\in \mathbb{Z}$$
20	19 14	climresd	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)⇝⇝\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\leftrightarrow F⇝⇝\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\right)$$
21	18 20	mpbid	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)\to F⇝⇝\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
22	14 15 21	breldmd	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)\to F\in \mathrm{dom}⇝$$
23	13 22	impbida	$$⊢\phi \to \left(F\in \mathrm{dom}⇝\leftrightarrow {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}⇝\right)$$