Theorem xlimresdm

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

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

Proof

Step	Hyp	Ref	Expression
1		xlimresdm.1	$$⊢\phi \to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
2		xlimresdm.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		xlimrel	$$⊢\mathrm{Rel}\underset{*}{⇝}$$
4		xlimdm	$$⊢F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)$$
5	4	a1i	$$⊢\phi \to \left(F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)\right)$$
6	5	biimpa	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)$$
7	1	adantr	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
8	2	adantr	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to M\in \mathbb{Z}$$
9	7 8	xlimres	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to \left(F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left(F\right)\right)$$
10	6 9	mpbid	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left(F\right)$$
11		releldm	$$⊢\left(\mathrm{Rel}\underset{*}{⇝}\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left(F\right)\right)\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}$$
12	3 10 11	sylancr	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}$$
13		xlimdm	$$⊢{F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
14	13	biimpi	$$⊢{F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
15	14	adantl	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
16	1 2	xlimres	$$⊢\phi \to \left(F\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\right)$$
17	16	adantr	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\right)\to \left(F\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\right)$$
18	15 17	mpbird	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\right)\to F\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)$$
19		releldm	$$⊢\left(\mathrm{Rel}\underset{*}{⇝}\wedge F\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\right)\to F\in \mathrm{dom}\underset{*}{⇝}$$
20	3 18 19	sylancr	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\right)\to F\in \mathrm{dom}\underset{*}{⇝}$$
21	12 20	impbida	$$⊢\phi \to \left(F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\right)$$