Theorem xlimres

Description: A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimres.1	$$⊢\phi \to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
	xlimres.2	$$⊢\phi \to M\in \mathbb{Z}$$
Assertion	xlimres	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimres.1	$$⊢\phi \to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
2		xlimres.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		letopon	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
4	3	a1i	$$⊢\phi \to \mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
5	4 1 2	lmres	$$⊢\phi \to \left(F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A\right)$$
6		df-xlim	$$⊢\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
7	6	breqi	$$⊢F\underset{*}{⇝}A\leftrightarrow F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
8	6	breqi	$$⊢\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
9	5 7 8	3bitr4g	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}A\right)$$