# Metamath Proof Explorer

## Theorem lmres

Description: A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses lmres.2 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
lmres.4 ${⊢}{\phi }\to {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
lmres.5 ${⊢}{\phi }\to {M}\in ℤ$
Assertion lmres

### Proof

Step Hyp Ref Expression
1 lmres.2 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
2 lmres.4 ${⊢}{\phi }\to {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
3 lmres.5 ${⊢}{\phi }\to {M}\in ℤ$
4 toponmax ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {J}$
5 1 4 syl ${⊢}{\phi }\to {X}\in {J}$
6 cnex ${⊢}ℂ\in \mathrm{V}$
7 ssid ${⊢}{X}\subseteq {X}$
8 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
9 zsscn ${⊢}ℤ\subseteq ℂ$
10 8 9 sstri ${⊢}{ℤ}_{\ge {M}}\subseteq ℂ$
11 pmss12g ${⊢}\left(\left({X}\subseteq {X}\wedge {ℤ}_{\ge {M}}\subseteq ℂ\right)\wedge \left({X}\in {J}\wedge ℂ\in \mathrm{V}\right)\right)\to {X}{↑}_{𝑝𝑚}{ℤ}_{\ge {M}}\subseteq {X}{↑}_{𝑝𝑚}ℂ$
12 7 10 11 mpanl12 ${⊢}\left({X}\in {J}\wedge ℂ\in \mathrm{V}\right)\to {X}{↑}_{𝑝𝑚}{ℤ}_{\ge {M}}\subseteq {X}{↑}_{𝑝𝑚}ℂ$
13 5 6 12 sylancl ${⊢}{\phi }\to {X}{↑}_{𝑝𝑚}{ℤ}_{\ge {M}}\subseteq {X}{↑}_{𝑝𝑚}ℂ$
14 fvex ${⊢}{ℤ}_{\ge {M}}\in \mathrm{V}$
15 pmresg ${⊢}\left({ℤ}_{\ge {M}}\in \mathrm{V}\wedge {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)\to {{F}↾}_{{ℤ}_{\ge {M}}}\in \left({X}{↑}_{𝑝𝑚}{ℤ}_{\ge {M}}\right)$
16 14 2 15 sylancr ${⊢}{\phi }\to {{F}↾}_{{ℤ}_{\ge {M}}}\in \left({X}{↑}_{𝑝𝑚}{ℤ}_{\ge {M}}\right)$
17 13 16 sseldd ${⊢}{\phi }\to {{F}↾}_{{ℤ}_{\ge {M}}}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
18 17 2 2thd ${⊢}{\phi }\to \left({{F}↾}_{{ℤ}_{\ge {M}}}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)↔{F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\right)$
19 eqid ${⊢}{ℤ}_{\ge {M}}={ℤ}_{\ge {M}}$
20 19 uztrn2 ${⊢}\left({j}\in {ℤ}_{\ge {M}}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {ℤ}_{\ge {M}}$
21 dmres ${⊢}\mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)={ℤ}_{\ge {M}}\cap \mathrm{dom}{F}$
22 21 elin2 ${⊢}{k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)↔\left({k}\in {ℤ}_{\ge {M}}\wedge {k}\in \mathrm{dom}{F}\right)$
23 22 baib ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)↔{k}\in \mathrm{dom}{F}\right)$
24 fvres ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)={F}\left({k}\right)$
25 24 eleq1d ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left(\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}↔{F}\left({k}\right)\in {u}\right)$
26 23 25 anbi12d ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left(\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)$
27 20 26 syl ${⊢}\left({j}\in {ℤ}_{\ge {M}}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left(\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)$
28 27 ralbidva ${⊢}{j}\in {ℤ}_{\ge {M}}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)$
29 28 rexbiia ${⊢}\exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)↔\exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)$
30 29 imbi2i ${⊢}\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)\right)↔\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)$
31 30 ralbii ${⊢}\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)\right)↔\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)$
32 31 a1i ${⊢}{\phi }\to \left(\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)\right)↔\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)\right)$
33 18 32 3anbi13d ${⊢}{\phi }\to \left(\left({{F}↾}_{{ℤ}_{\ge {M}}}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}\left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\wedge \left({{F}↾}_{{ℤ}_{\ge {M}}}\right)\left({k}\right)\in {u}\right)\right)\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\right)\right)\right)$
34 1 19 3 lmbr2
35 1 19 3 lmbr2
36 33 34 35 3bitr4rd