This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (M \in ℤ \land F \in V) \to (({F ↾}_{ℤ_{\geq M}}) ⇝ A \leftrightarrow F ⇝ A)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
2		resexg	$⊢ F \in V \to {F ↾}_{ℤ_{\geq M}} \in V$
3	2	adantl	$⊢ (M \in ℤ \land F \in V) \to {F ↾}_{ℤ_{\geq M}} \in V$
4		simpr	$⊢ (M \in ℤ \land F \in V) \to F \in V$
5		simpl	$⊢ (M \in ℤ \land F \in V) \to M \in ℤ$
6		fvres	$⊢ k \in ℤ_{\geq M} \to ({F ↾}_{ℤ_{\geq M}}) (k) = F (k)$
7	6	adantl	$⊢ ((M \in ℤ \land F \in V) \land k \in ℤ_{\geq M}) \to ({F ↾}_{ℤ_{\geq M}}) (k) = F (k)$
8	1 3 4 5 7	climeq	$⊢ (M \in ℤ \land F \in V) \to (({F ↾}_{ℤ_{\geq M}}) ⇝ A \leftrightarrow F ⇝ A)$