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 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
lmres.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
lmres.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion lmres ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) )

Proof

Step Hyp Ref Expression
1 lmres.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 lmres.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
3 lmres.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
5 1 4 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
6 cnex ⊢ ℂ ∈ V
7 ssid ⊢ 𝑋 ⊆ 𝑋
8 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
9 zsscn ⊢ ℤ ⊆ ℂ
10 8 9 sstri ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ
11 pmss12g ⊢ ( ( ( 𝑋 ⊆ 𝑋 ∧ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ ) ∧ ( 𝑋 ∈ 𝐽 ∧ ℂ ∈ V ) ) → ( 𝑋 ↑pm ( ℤ≥ ‘ 𝑀 ) ) ⊆ ( 𝑋 ↑pm ℂ ) )
12 7 10 11 mpanl12 ⊢ ( ( 𝑋 ∈ 𝐽 ∧ ℂ ∈ V ) → ( 𝑋 ↑pm ( ℤ≥ ‘ 𝑀 ) ) ⊆ ( 𝑋 ↑pm ℂ ) )
13 5 6 12 sylancl ⊢ ( 𝜑 → ( 𝑋 ↑pm ( ℤ≥ ‘ 𝑀 ) ) ⊆ ( 𝑋 ↑pm ℂ ) )
14 fvex ⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
15 pmresg ⊢ ( ( ( ℤ≥ ‘ 𝑀 ) ∈ V ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ ( 𝑋 ↑pm ( ℤ≥ ‘ 𝑀 ) ) )
16 14 2 15 sylancr ⊢ ( 𝜑 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ ( 𝑋 ↑pm ( ℤ≥ ‘ 𝑀 ) ) )
17 13 16 sseldd ⊢ ( 𝜑 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ ( 𝑋 ↑pm ℂ ) )
18 17 2 2thd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ ( 𝑋 ↑pm ℂ ) ↔ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) )
19 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
20 19 uztrn2 ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
21 dmres ⊢ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ dom 𝐹 )
22 21 elin2 ⊢ ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ dom 𝐹 ) )
23 22 baib ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ↔ 𝑘 ∈ dom 𝐹 ) )
24 fvres ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
25 24 eleq1d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
26 23 25 anbi12d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
27 20 26 syl ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
28 27 ralbidva ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
29 28 rexbiia ⊢ ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
30 29 imbi2i ⊢ ( ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ) ↔ ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
31 30 ralbii ⊢ ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
32 31 a1i ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
33 18 32 3anbi13d ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
34 1 19 3 lmbr2 ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
35 1 19 3 lmbr2 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
36 33 34 35 3bitr4rd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) )