Metamath Proof Explorer

Theorem climshft

Description: A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion climshft 
|- ( ( M e. ZZ /\ F e. V ) -> ( ( F shift M ) ~~> A <-> F ~~> A ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( f = F -> ( f shift M ) = ( F shift M ) )
2 1 breq1d 
 |-  ( f = F -> ( ( f shift M ) ~~> A <-> ( F shift M ) ~~> A ) )
3 breq1 
 |-  ( f = F -> ( f ~~> A <-> F ~~> A ) )
4 2 3 bibi12d 
 |-  ( f = F -> ( ( ( f shift M ) ~~> A <-> f ~~> A ) <-> ( ( F shift M ) ~~> A <-> F ~~> A ) ) )
5 4 imbi2d 
 |-  ( f = F -> ( ( M e. ZZ -> ( ( f shift M ) ~~> A <-> f ~~> A ) ) <-> ( M e. ZZ -> ( ( F shift M ) ~~> A <-> F ~~> A ) ) ) )
6 znegcl 
 |-  ( M e. ZZ -> -u M e. ZZ )
7 ovex 
 |-  ( f shift M ) e. _V
8 7 climshftlem 
 |-  ( -u M e. ZZ -> ( ( f shift M ) ~~> A -> ( ( f shift M ) shift -u M ) ~~> A ) )
9 6 8 syl 
 |-  ( M e. ZZ -> ( ( f shift M ) ~~> A -> ( ( f shift M ) shift -u M ) ~~> A ) )
10 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
11 ovexd 
 |-  ( M e. ZZ -> ( ( f shift M ) shift -u M ) e. _V )
12 vex 
 |-  f e. _V
13 12 a1i 
 |-  ( M e. ZZ -> f e. _V )
14 id 
 |-  ( M e. ZZ -> M e. ZZ )
15 zcn 
 |-  ( M e. ZZ -> M e. CC )
16 eluzelcn 
 |-  ( k e. ( ZZ>= ` M ) -> k e. CC )
17 12 shftcan1 
 |-  ( ( M e. CC /\ k e. CC ) -> ( ( ( f shift M ) shift -u M ) ` k ) = ( f ` k ) )
18 15 16 17 syl2an 
 |-  ( ( M e. ZZ /\ k e. ( ZZ>= ` M ) ) -> ( ( ( f shift M ) shift -u M ) ` k ) = ( f ` k ) )
19 10 11 13 14 18 climeq 
 |-  ( M e. ZZ -> ( ( ( f shift M ) shift -u M ) ~~> A <-> f ~~> A ) )
20 9 19 sylibd 
 |-  ( M e. ZZ -> ( ( f shift M ) ~~> A -> f ~~> A ) )
21 12 climshftlem 
 |-  ( M e. ZZ -> ( f ~~> A -> ( f shift M ) ~~> A ) )
22 20 21 impbid 
 |-  ( M e. ZZ -> ( ( f shift M ) ~~> A <-> f ~~> A ) )
23 5 22 vtoclg 
 |-  ( F e. V -> ( M e. ZZ -> ( ( F shift M ) ~~> A <-> F ~~> A ) ) )
24 23 impcom 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( ( F shift M ) ~~> A <-> F ~~> A ) )