Theorem climresd

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

	Ref	Expression
Hypotheses	climresd.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climresd.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion	climresd	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climresd.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		climresd.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		climres	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )