Metamath Proof Explorer


Theorem climresmpt

Description: A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses climresmpt.z 𝑍 = ( ℤ𝑀 )
climresmpt.f 𝐹 = ( 𝑥𝑍𝐴 )
climresmpt.n ( 𝜑𝑁𝑍 )
climresmpt.g 𝐺 = ( 𝑥 ∈ ( ℤ𝑁 ) ↦ 𝐴 )
Assertion climresmpt ( 𝜑 → ( 𝐺𝐵𝐹𝐵 ) )

Proof

Step Hyp Ref Expression
1 climresmpt.z 𝑍 = ( ℤ𝑀 )
2 climresmpt.f 𝐹 = ( 𝑥𝑍𝐴 )
3 climresmpt.n ( 𝜑𝑁𝑍 )
4 climresmpt.g 𝐺 = ( 𝑥 ∈ ( ℤ𝑁 ) ↦ 𝐴 )
5 2 reseq1i ( 𝐹 ↾ ( ℤ𝑁 ) ) = ( ( 𝑥𝑍𝐴 ) ↾ ( ℤ𝑁 ) )
6 5 a1i ( 𝜑 → ( 𝐹 ↾ ( ℤ𝑁 ) ) = ( ( 𝑥𝑍𝐴 ) ↾ ( ℤ𝑁 ) ) )
7 3 1 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
8 uzss ( 𝑁 ∈ ( ℤ𝑀 ) → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )
9 7 8 syl ( 𝜑 → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )
10 9 1 sseqtrrdi ( 𝜑 → ( ℤ𝑁 ) ⊆ 𝑍 )
11 resmpt ( ( ℤ𝑁 ) ⊆ 𝑍 → ( ( 𝑥𝑍𝐴 ) ↾ ( ℤ𝑁 ) ) = ( 𝑥 ∈ ( ℤ𝑁 ) ↦ 𝐴 ) )
12 10 11 syl ( 𝜑 → ( ( 𝑥𝑍𝐴 ) ↾ ( ℤ𝑁 ) ) = ( 𝑥 ∈ ( ℤ𝑁 ) ↦ 𝐴 ) )
13 4 eqcomi ( 𝑥 ∈ ( ℤ𝑁 ) ↦ 𝐴 ) = 𝐺
14 13 a1i ( 𝜑 → ( 𝑥 ∈ ( ℤ𝑁 ) ↦ 𝐴 ) = 𝐺 )
15 6 12 14 3eqtrrd ( 𝜑𝐺 = ( 𝐹 ↾ ( ℤ𝑁 ) ) )
16 15 breq1d ( 𝜑 → ( 𝐺𝐵 ↔ ( 𝐹 ↾ ( ℤ𝑁 ) ) ⇝ 𝐵 ) )
17 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
18 7 17 syl ( 𝜑𝑁 ∈ ℤ )
19 1 fvexi 𝑍 ∈ V
20 19 mptex ( 𝑥𝑍𝐴 ) ∈ V
21 20 a1i ( 𝜑 → ( 𝑥𝑍𝐴 ) ∈ V )
22 2 21 eqeltrid ( 𝜑𝐹 ∈ V )
23 climres ( ( 𝑁 ∈ ℤ ∧ 𝐹 ∈ V ) → ( ( 𝐹 ↾ ( ℤ𝑁 ) ) ⇝ 𝐵𝐹𝐵 ) )
24 18 22 23 syl2anc ( 𝜑 → ( ( 𝐹 ↾ ( ℤ𝑁 ) ) ⇝ 𝐵𝐹𝐵 ) )
25 16 24 bitrd ( 𝜑 → ( 𝐺𝐵𝐹𝐵 ) )