Metamath Proof Explorer

Theorem climshftlem

Description: A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013)

Ref Expression
Hypothesis climshft.1 
|- F e. _V
Assertion climshftlem 
|- ( M e. ZZ -> ( F ~~> A -> ( F shift M ) ~~> A ) )

Proof

Step Hyp Ref Expression
1 climshft.1 
 |-  F e. _V
2 zaddcl 
 |-  ( ( k e. ZZ /\ M e. ZZ ) -> ( k + M ) e. ZZ )
3 2 ancoms 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( k + M ) e. ZZ )
4 eluzsub 
 |-  ( ( k e. ZZ /\ M e. ZZ /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( n - M ) e. ( ZZ>= ` k ) )
5 4 3com12 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( n - M ) e. ( ZZ>= ` k ) )
6 5 3expa 
 |-  ( ( ( M e. ZZ /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( n - M ) e. ( ZZ>= ` k ) )
7 fveq2 
 |-  ( m = ( n - M ) -> ( F ` m ) = ( F ` ( n - M ) ) )
8 7 eleq1d 
 |-  ( m = ( n - M ) -> ( ( F ` m ) e. CC <-> ( F ` ( n - M ) ) e. CC ) )
9 7 fvoveq1d 
 |-  ( m = ( n - M ) -> ( abs ` ( ( F ` m ) - A ) ) = ( abs ` ( ( F ` ( n - M ) ) - A ) ) )
10 9 breq1d 
 |-  ( m = ( n - M ) -> ( ( abs ` ( ( F ` m ) - A ) ) < x <-> ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) )
11 8 10 anbi12d 
 |-  ( m = ( n - M ) -> ( ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
12 11 rspcv 
 |-  ( ( n - M ) e. ( ZZ>= ` k ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
13 6 12 syl 
 |-  ( ( ( M e. ZZ /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
14 zcn 
 |-  ( M e. ZZ -> M e. CC )
15 eluzelcn 
 |-  ( n e. ( ZZ>= ` ( k + M ) ) -> n e. CC )
16 1 shftval 
 |-  ( ( M e. CC /\ n e. CC ) -> ( ( F shift M ) ` n ) = ( F ` ( n - M ) ) )
17 16 eleq1d 
 |-  ( ( M e. CC /\ n e. CC ) -> ( ( ( F shift M ) ` n ) e. CC <-> ( F ` ( n - M ) ) e. CC ) )
18 16 fvoveq1d 
 |-  ( ( M e. CC /\ n e. CC ) -> ( abs ` ( ( ( F shift M ) ` n ) - A ) ) = ( abs ` ( ( F ` ( n - M ) ) - A ) ) )
19 18 breq1d 
 |-  ( ( M e. CC /\ n e. CC ) -> ( ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x <-> ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) )
20 17 19 anbi12d 
 |-  ( ( M e. CC /\ n e. CC ) -> ( ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
21 14 15 20 syl2an 
 |-  ( ( M e. ZZ /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
22 21 adantlr 
 |-  ( ( ( M e. ZZ /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
23 13 22 sylibrd 
 |-  ( ( ( M e. ZZ /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
24 23 ralrimdva 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> A. n e. ( ZZ>= ` ( k + M ) ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
25 fveq2 
 |-  ( m = ( k + M ) -> ( ZZ>= ` m ) = ( ZZ>= ` ( k + M ) ) )
26 25 raleqdv 
 |-  ( m = ( k + M ) -> ( A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> A. n e. ( ZZ>= ` ( k + M ) ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
27 26 rspcev 
 |-  ( ( ( k + M ) e. ZZ /\ A. n e. ( ZZ>= ` ( k + M ) ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) -> E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) )
28 3 24 27 syl6an 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
29 28 rexlimdva 
 |-  ( M e. ZZ -> ( E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
30 29 ralimdv 
 |-  ( M e. ZZ -> ( A. x e. RR+ E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> A. x e. RR+ E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
31 30 anim2d 
 |-  ( M e. ZZ -> ( ( A e. CC /\ A. x e. RR+ E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) ) -> ( A e. CC /\ A. x e. RR+ E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) ) )
32 1 a1i 
 |-  ( M e. ZZ -> F e. _V )
33 eqidd 
 |-  ( ( M e. ZZ /\ m e. ZZ ) -> ( F ` m ) = ( F ` m ) )
34 32 33 clim 
 |-  ( M e. ZZ -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) ) ) )
35 ovexd 
 |-  ( M e. ZZ -> ( F shift M ) e. _V )
36 eqidd 
 |-  ( ( M e. ZZ /\ n e. ZZ ) -> ( ( F shift M ) ` n ) = ( ( F shift M ) ` n ) )
37 35 36 clim 
 |-  ( M e. ZZ -> ( ( F shift M ) ~~> A <-> ( A e. CC /\ A. x e. RR+ E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) ) )
38 31 34 37 3imtr4d 
 |-  ( M e. ZZ -> ( F ~~> A -> ( F shift M ) ~~> A ) )