Metamath Proof Explorer

Theorem climshft2

Description: A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007) (Revised by Mario Carneiro, 6-Feb-2014)

Ref Expression
Hypotheses climshft2.1 
|- Z = ( ZZ>= ` M )
climshft2.2 
|- ( ph -> M e. ZZ )
climshft2.3 
|- ( ph -> K e. ZZ )
climshft2.5 
|- ( ph -> F e. W )
climshft2.6 
|- ( ph -> G e. X )
climshft2.7 
|- ( ( ph /\ k e. Z ) -> ( G ` ( k + K ) ) = ( F ` k ) )
Assertion climshft2 
|- ( ph -> ( F ~~> A <-> G ~~> A ) )

Proof

Step Hyp Ref Expression
1 climshft2.1 
 |-  Z = ( ZZ>= ` M )
2 climshft2.2 
 |-  ( ph -> M e. ZZ )
3 climshft2.3 
 |-  ( ph -> K e. ZZ )
4 climshft2.5 
 |-  ( ph -> F e. W )
5 climshft2.6 
 |-  ( ph -> G e. X )
6 climshft2.7 
 |-  ( ( ph /\ k e. Z ) -> ( G ` ( k + K ) ) = ( F ` k ) )
7 ovexd 
 |-  ( ph -> ( G shift -u K ) e. _V )
8 3 zcnd 
 |-  ( ph -> K e. CC )
9 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
10 9 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
11 10 zcnd 
 |-  ( k e. Z -> k e. CC )
12 fvex 
 |-  ( _I ` G ) e. _V
13 12 shftval4 
 |-  ( ( K e. CC /\ k e. CC ) -> ( ( ( _I ` G ) shift -u K ) ` k ) = ( ( _I ` G ) ` ( K + k ) ) )
14 8 11 13 syl2an 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( _I ` G ) shift -u K ) ` k ) = ( ( _I ` G ) ` ( K + k ) ) )
15 fvi 
 |-  ( G e. X -> ( _I ` G ) = G )
16 5 15 syl 
 |-  ( ph -> ( _I ` G ) = G )
17 16 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( _I ` G ) = G )
18 17 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( _I ` G ) shift -u K ) = ( G shift -u K ) )
19 18 fveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( _I ` G ) shift -u K ) ` k ) = ( ( G shift -u K ) ` k ) )
20 addcom 
 |-  ( ( K e. CC /\ k e. CC ) -> ( K + k ) = ( k + K ) )
21 8 11 20 syl2an 
 |-  ( ( ph /\ k e. Z ) -> ( K + k ) = ( k + K ) )
22 17 21 fveq12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( _I ` G ) ` ( K + k ) ) = ( G ` ( k + K ) ) )
23 14 19 22 3eqtr3d 
 |-  ( ( ph /\ k e. Z ) -> ( ( G shift -u K ) ` k ) = ( G ` ( k + K ) ) )
24 23 6 eqtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( G shift -u K ) ` k ) = ( F ` k ) )
25 1 7 4 2 24 climeq 
 |-  ( ph -> ( ( G shift -u K ) ~~> A <-> F ~~> A ) )
26 3 znegcld 
 |-  ( ph -> -u K e. ZZ )
27 climshft 
 |-  ( ( -u K e. ZZ /\ G e. X ) -> ( ( G shift -u K ) ~~> A <-> G ~~> A ) )
28 26 5 27 syl2anc 
 |-  ( ph -> ( ( G shift -u K ) ~~> A <-> G ~~> A ) )
29 25 28 bitr3d 
 |-  ( ph -> ( F ~~> A <-> G ~~> A ) )