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	bilani	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to F\underset{*}{⇝}\underset{*}{⇝}\left(F\right)$$
6	1	adantr	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
7	2	adantr	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to M\in \mathbb{Z}$$
8	6 7	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)$$
9	5 8	mpbid	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\underset{*}{⇝}\underset{*}{⇝}\left(F\right)$$
10		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{*}{⇝}$$
11	3 9 10	sylancr	$$⊢\left(\phi \wedge F\in \mathrm{dom}\underset{*}{⇝}\right)\to {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}$$
12		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)$$
13	12	bilani	$$⊢\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)$$
14	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)$$
15	14	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)$$
16	13 15	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)$$
17		releldm	$$⊢\left(\mathrm{Rel}\underset{*}{⇝}\wedge F\underset{*}{⇝}\underset{*}{⇝}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\right)\right)\to F\in \mathrm{dom}\underset{*}{⇝}$$
18	3 16 17	sylancr	$$⊢\left(\phi \wedge {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\right)\to F\in \mathrm{dom}\underset{*}{⇝}$$
19	11 18	impbida	$$⊢\phi \to \left(F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow {F\upharpoonright }_{{\mathbb{Z}}_{\ge M}}\in \mathrm{dom}\underset{*}{⇝}\right)$$