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