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	⊢ ( 𝜑 → ( 𝐺 ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵 ) )

Metamath Proof Explorer

Theorem climresmpt

Proof