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

Metamath Proof Explorer

Theorem climmptf

Description: Exhibit a function G with the same convergence properties as the not-quite-function F . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climmptf.k 
|- F/_ k F
climmptf.m 
|- ( ph -> M e. ZZ )
climmptf.f 
|- ( ph -> F e. V )
climmptf.z 
|- Z = ( ZZ>= ` M )
climmptf.g 
|- G = ( k e. Z |-> ( F ` k ) )
Assertion climmptf 
|- ( ph -> ( F ~~> A <-> G ~~> A ) )

Proof

Step Hyp Ref Expression
1 climmptf.k 
 |-  F/_ k F
2 climmptf.m 
 |-  ( ph -> M e. ZZ )
3 climmptf.f 
 |-  ( ph -> F e. V )
4 climmptf.z 
 |-  Z = ( ZZ>= ` M )
5 climmptf.g 
 |-  G = ( k e. Z |-> ( F ` k ) )
6 nfcv 
 |-  F/_ j ( F ` k )
7 nfcv 
 |-  F/_ k j
8 1 7 nffv 
 |-  F/_ k ( F ` j )
9 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
10 6 8 9 cbvmpt 
 |-  ( k e. Z |-> ( F ` k ) ) = ( j e. Z |-> ( F ` j ) )
11 5 10 eqtri 
 |-  G = ( j e. Z |-> ( F ` j ) )
12 4 11 climmpt 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )
13 2 3 12 syl2anc 
 |-  ( ph -> ( F ~~> A <-> G ~~> A ) )