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 e. ZZ /\ F e. V ) -> ( ( F |` ( ZZ>= ` M ) ) ~~> A <-> F ~~> A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
2 resexg 
 |-  ( F e. V -> ( F |` ( ZZ>= ` M ) ) e. _V )
3 2 adantl 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( F |` ( ZZ>= ` M ) ) e. _V )
4 simpr 
 |-  ( ( M e. ZZ /\ F e. V ) -> F e. V )
5 simpl 
 |-  ( ( M e. ZZ /\ F e. V ) -> M e. ZZ )
6 fvres 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( F |` ( ZZ>= ` M ) ) ` k ) = ( F ` k ) )
7 6 adantl 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F |` ( ZZ>= ` M ) ) ` k ) = ( F ` k ) )
8 1 3 4 5 7 climeq 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( ( F |` ( ZZ>= ` M ) ) ~~> A <-> F ~~> A ) )