Metamath Proof Explorer


Theorem ulmres

Description: A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ulmres.z
|- Z = ( ZZ>= ` M )
ulmres.w
|- W = ( ZZ>= ` N )
ulmres.m
|- ( ph -> N e. Z )
ulmres.f
|- ( ph -> F : Z --> ( CC ^m S ) )
Assertion ulmres
|- ( ph -> ( F ( ~~>u ` S ) G <-> ( F |` W ) ( ~~>u ` S ) G ) )

Proof

Step Hyp Ref Expression
1 ulmres.z
 |-  Z = ( ZZ>= ` M )
2 ulmres.w
 |-  W = ( ZZ>= ` N )
3 ulmres.m
 |-  ( ph -> N e. Z )
4 ulmres.f
 |-  ( ph -> F : Z --> ( CC ^m S ) )
5 ulmscl
 |-  ( F ( ~~>u ` S ) G -> S e. _V )
6 ulmcl
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
7 5 6 jca
 |-  ( F ( ~~>u ` S ) G -> ( S e. _V /\ G : S --> CC ) )
8 7 a1i
 |-  ( ph -> ( F ( ~~>u ` S ) G -> ( S e. _V /\ G : S --> CC ) ) )
9 ulmscl
 |-  ( ( F |` W ) ( ~~>u ` S ) G -> S e. _V )
10 ulmcl
 |-  ( ( F |` W ) ( ~~>u ` S ) G -> G : S --> CC )
11 9 10 jca
 |-  ( ( F |` W ) ( ~~>u ` S ) G -> ( S e. _V /\ G : S --> CC ) )
12 11 a1i
 |-  ( ph -> ( ( F |` W ) ( ~~>u ` S ) G -> ( S e. _V /\ G : S --> CC ) ) )
13 3 1 eleqtrdi
 |-  ( ph -> N e. ( ZZ>= ` M ) )
14 13 adantr
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> N e. ( ZZ>= ` M ) )
15 eluzel2
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
16 14 15 syl
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> M e. ZZ )
17 1 rexuz3
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
18 16 17 syl
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
19 eluzelz
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
20 14 19 syl
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> N e. ZZ )
21 2 rexuz3
 |-  ( N e. ZZ -> ( E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
22 20 21 syl
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
23 18 22 bitr4d
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r <-> E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
24 23 ralbidv
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r <-> A. r e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
25 4 adantr
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> F : Z --> ( CC ^m S ) )
26 eqidd
 |-  ( ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` z ) )
27 eqidd
 |-  ( ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
28 simprr
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> G : S --> CC )
29 simprl
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> S e. _V )
30 1 16 25 26 27 28 29 ulm2
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( F ( ~~>u ` S ) G <-> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
31 uzss
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
32 14 31 syl
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
33 32 2 1 3sstr4g
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> W C_ Z )
34 25 33 fssresd
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( F |` W ) : W --> ( CC ^m S ) )
35 fvres
 |-  ( k e. W -> ( ( F |` W ) ` k ) = ( F ` k ) )
36 35 ad2antrl
 |-  ( ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) /\ ( k e. W /\ z e. S ) ) -> ( ( F |` W ) ` k ) = ( F ` k ) )
37 36 fveq1d
 |-  ( ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) /\ ( k e. W /\ z e. S ) ) -> ( ( ( F |` W ) ` k ) ` z ) = ( ( F ` k ) ` z ) )
38 2 20 34 37 27 28 29 ulm2
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( ( F |` W ) ( ~~>u ` S ) G <-> A. r e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < r ) )
39 24 30 38 3bitr4d
 |-  ( ( ph /\ ( S e. _V /\ G : S --> CC ) ) -> ( F ( ~~>u ` S ) G <-> ( F |` W ) ( ~~>u ` S ) G ) )
40 39 ex
 |-  ( ph -> ( ( S e. _V /\ G : S --> CC ) -> ( F ( ~~>u ` S ) G <-> ( F |` W ) ( ~~>u ` S ) G ) ) )
41 8 12 40 pm5.21ndd
 |-  ( ph -> ( F ( ~~>u ` S ) G <-> ( F |` W ) ( ~~>u ` S ) G ) )