Theorem climres

Description: A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Assertion	climres	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
2		resexg	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ V )
3	2	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ V )
4		simpr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝐹 ∈ 𝑉 )
5		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝑀 ∈ ℤ )
6		fvres	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
7	6	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
8	1 3 4 5 7	climeq	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )