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 ) ) |