Metamath Proof Explorer

Theorem climmpt

Description: Exhibit a function G with the same convergence properties as the not-quite-function F . (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses 2clim.1 
|- Z = ( ZZ>= ` M )
climmpt.2 
|- G = ( k e. Z |-> ( F ` k ) )
Assertion climmpt 
|- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )

Proof

Step Hyp Ref Expression
1 2clim.1 
 |-  Z = ( ZZ>= ` M )
2 climmpt.2 
 |-  G = ( k e. Z |-> ( F ` k ) )
3 simpr 
 |-  ( ( M e. ZZ /\ F e. V ) -> F e. V )
4 fvex 
 |-  ( ZZ>= ` M ) e. _V
5 1 4 eqeltri 
 |-  Z e. _V
6 5 mptex 
 |-  ( k e. Z |-> ( F ` k ) ) e. _V
7 2 6 eqeltri 
 |-  G e. _V
8 7 a1i 
 |-  ( ( M e. ZZ /\ F e. V ) -> G e. _V )
9 simpl 
 |-  ( ( M e. ZZ /\ F e. V ) -> M e. ZZ )
10 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
11 fvex 
 |-  ( F ` m ) e. _V
12 10 2 11 fvmpt 
 |-  ( m e. Z -> ( G ` m ) = ( F ` m ) )
13 12 eqcomd 
 |-  ( m e. Z -> ( F ` m ) = ( G ` m ) )
14 13 adantl 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ m e. Z ) -> ( F ` m ) = ( G ` m ) )
15 1 3 8 9 14 climeq 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )