MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ulmcau Structured version   Unicode version

Theorem ulmcau 20311
Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 
0  <  x there is a  j such that for all  j  <_  k the functions  F ( k ) and  F
( j ) are uniformly within  x of each other on  S. This is the four-quantifier version, see ulmcau2 20312 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypotheses
Ref Expression
ulmcau.z  |-  Z  =  ( ZZ>= `  M )
ulmcau.m  |-  ( ph  ->  M  e.  ZZ )
ulmcau.s  |-  ( ph  ->  S  e.  V )
ulmcau.f  |-  ( ph  ->  F : Z --> ( CC 
^m  S ) )
Assertion
Ref Expression
ulmcau  |-  ( ph  ->  ( F  e.  dom  (
~~> u `  S )  <->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x ) )
Distinct variable groups:    j, k, x, z, F    ph, j, k, x, z    S, j, k, x, z    j, Z, k, x, z    j, M, k, z
Allowed substitution hints:    M( x)    V( x, z, j, k)

Proof of Theorem ulmcau
Dummy variables  g  m  n  p  q 
r  v  w  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldmg 5065 . . . 4  |-  ( F  e.  dom  ( ~~> u `  S )  ->  ( F  e.  dom  ( ~~> u `  S )  <->  E. g  F ( ~~> u `  S ) g ) )
21ibi 233 . . 3  |-  ( F  e.  dom  ( ~~> u `  S )  ->  E. g  F ( ~~> u `  S ) g )
3 ulmcau.z . . . . . . . 8  |-  Z  =  ( ZZ>= `  M )
4 ulmcau.m . . . . . . . . 9  |-  ( ph  ->  M  e.  ZZ )
54ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  M  e.  ZZ )
6 ulmcau.f . . . . . . . . 9  |-  ( ph  ->  F : Z --> ( CC 
^m  S ) )
76ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F : Z --> ( CC 
^m  S ) )
8 eqidd 2437 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( k  e.  Z  /\  z  e.  S ) )  -> 
( ( F `  k ) `  z
)  =  ( ( F `  k ) `
 z ) )
9 eqidd 2437 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  z  e.  S
)  ->  ( g `  z )  =  ( g `  z ) )
10 simplr 732 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F ( ~~> u `  S ) g )
11 rphalfcl 10636 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR+ )
1211adantl 453 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  -> 
( x  /  2
)  e.  RR+ )
133, 5, 7, 8, 9, 10, 12ulmi 20302 . . . . . . 7  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  E. j  e.  Z  A. k  e.  ( ZZ>=
`  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  < 
( x  /  2
) )
14 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  Z )
1514, 3syl6eleq 2526 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  ( ZZ>= `  M )
)
16 eluzelz 10496 . . . . . . . . . . 11  |-  ( j  e.  ( ZZ>= `  M
)  ->  j  e.  ZZ )
17 uzid 10500 . . . . . . . . . . 11  |-  ( j  e.  ZZ  ->  j  e.  ( ZZ>= `  j )
)
1815, 16, 173syl 19 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  ( ZZ>= `  j )
)
19 fveq2 5728 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  ( F `  k )  =  ( F `  j ) )
2019fveq1d 5730 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( F `  k
) `  z )  =  ( ( F `
 j ) `  z ) )
2120oveq1d 6096 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ( F `  k ) `  z
)  -  ( g `
 z ) )  =  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )
2221fveq2d 5732 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  =  ( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) ) )
2322breq1d 4222 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  <->  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) ) )
2423ralbidv 2725 . . . . . . . . . . 11  |-  ( k  =  j  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 )  <->  A. z  e.  S  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) ) )
2524rspcv 3048 . . . . . . . . . 10  |-  ( j  e.  ( ZZ>= `  j
)  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. z  e.  S  ( abs `  ( ( ( F `  j
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) ) )
2618, 25syl 16 . . . . . . . . 9  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. z  e.  S  ( abs `  ( ( ( F `  j
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) ) )
27 r19.26 2838 . . . . . . . . . . . . . . 15  |-  ( A. z  e.  S  (
( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  /\  ( abs `  ( ( ( F `  k
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) )  <->  ( A. z  e.  S  ( abs `  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )  < 
( x  /  2
)  /\  A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) ) )
287ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
2928adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
30 elmapi 7038 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  j )  e.  ( CC  ^m  S )  ->  ( F `  j ) : S --> CC )
3129, 30syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  j ) : S --> CC )
3231ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( F `  j
) `  z )  e.  CC )
33 ulmcl 20297 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F ( ~~> u `  S
) g  ->  g : S --> CC )
3433ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  g : S
--> CC )
3534ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
g `  z )  e.  CC )
3632, 35abssubd 12255 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  ( abs `  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )  =  ( abs `  (
( g `  z
)  -  ( ( F `  j ) `
 z ) ) ) )
3736breq1d 4222 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  <->  ( abs `  ( ( g `  z )  -  (
( F `  j
) `  z )
) )  <  (
x  /  2 ) ) )
3837biimpd 199 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  -> 
( abs `  (
( g `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  ( x  /  2 ) ) )
393uztrn2 10503 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
k  e.  Z )
40 ffvelrn 5868 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : Z --> ( CC 
^m  S )  /\  k  e.  Z )  ->  ( F `  k
)  e.  ( CC 
^m  S ) )
417, 39, 40syl2an 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( j  e.  Z  /\  k  e.  ( ZZ>= `  j )
) )  ->  ( F `  k )  e.  ( CC  ^m  S
) )
4241anassrs 630 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  k )  e.  ( CC  ^m  S ) )
43 elmapi 7038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  k )  e.  ( CC  ^m  S )  ->  ( F `  k ) : S --> CC )
4442, 43syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  k ) : S --> CC )
4544ffvelrnda 5870 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( F `  k
) `  z )  e.  CC )
46 rpre 10618 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  RR )
4746ad4antlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  x  e.  RR )
48 abs3lem 12142 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( F `
 k ) `  z )  e.  CC  /\  ( ( F `  j ) `  z
)  e.  CC )  /\  ( ( g `
 z )  e.  CC  /\  x  e.  RR ) )  -> 
( ( ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  /\  ( abs `  (
( g `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  ( x  /  2 ) )  ->  ( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x ) )
4945, 32, 35, 47, 48syl22anc 1185 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( ( abs `  (
( ( F `  k ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  /\  ( abs `  ( ( g `  z )  -  ( ( F `
 j ) `  z ) ) )  <  ( x  / 
2 ) )  -> 
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x ) )
5038, 49sylan2d 469 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( ( abs `  (
( ( F `  k ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  /\  ( abs `  ( ( ( F `  j
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) )  -> 
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x ) )
5150ancomsd 441 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( ( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  /\  ( abs `  ( ( ( F `  k
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) )  -> 
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x ) )
5251ralimdva 2784 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( A. z  e.  S  (
( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  /\  ( abs `  ( ( ( F `  k
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) )  ->  A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x ) )
5327, 52syl5bir 210 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( ( A. z  e.  S  ( abs `  ( ( ( F `  j
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 )  /\  A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  < 
( x  /  2
) )  ->  A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
) )
5453expdimp 427 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  A. z  e.  S  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) )  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  < 
( x  /  2
)  ->  A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
) )
5554an32s 780 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  A. z  e.  S  ( abs `  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )  < 
( x  /  2
) )  /\  k  e.  ( ZZ>= `  j )
)  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  < 
( x  /  2
)  ->  A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
) )
5655ralimdva 2784 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  A. z  e.  S  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) )  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. k  e.  (
ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x ) )
5756ex 424 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )  < 
( x  /  2
)  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. k  e.  (
ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x ) ) )
5857com23 74 . . . . . . . . 9  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  ( A. z  e.  S  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. k  e.  (
ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x ) ) )
5926, 58mpdd 38 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. k  e.  (
ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x ) )
6059reximdva 2818 . . . . . . 7  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  -> 
( E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 )  ->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x ) )
6113, 60mpd 15 . . . . . 6  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  E. j  e.  Z  A. k  e.  ( ZZ>=
`  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x )
6261ralrimiva 2789 . . . . 5  |-  ( (
ph  /\  F ( ~~> u `  S )
g )  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )
6362ex 424 . . . 4  |-  ( ph  ->  ( F ( ~~> u `  S ) g  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x ) )
6463exlimdv 1646 . . 3  |-  ( ph  ->  ( E. g  F ( ~~> u `  S
) g  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x ) )
652, 64syl5 30 . 2  |-  ( ph  ->  ( F  e.  dom  (
~~> u `  S )  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
) )
66 ulmrel 20294 . . . 4  |-  Rel  ( ~~> u `  S )
67 ulmcau.s . . . . . . . . . 10  |-  ( ph  ->  S  e.  V )
683, 4, 67, 6ulmcaulem 20310 . . . . . . . . 9  |-  ( ph  ->  ( A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>=
`  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x  <->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  x ) )
6968biimpa 471 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  k ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )  < 
x )
70 rphalfcl 10636 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
71 breq2 4216 . . . . . . . . . . . . 13  |-  ( x  =  ( r  / 
2 )  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
7271ralbidv 2725 . . . . . . . . . . . 12  |-  ( x  =  ( r  / 
2 )  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  x  <->  A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
73722ralbidv 2747 . . . . . . . . . . 11  |-  ( x  =  ( r  / 
2 )  ->  ( A. k  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  x  <->  A. k  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  ( r  / 
2 ) ) )
7473rexbidv 2726 . . . . . . . . . 10  |-  ( x  =  ( r  / 
2 )  ->  ( E. j  e.  Z  A. k  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  x  <->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  ( r  / 
2 ) ) )
75 ralcom 2868 . . . . . . . . . . . . . 14  |-  ( A. w  e.  S  A. m  e.  ( ZZ>= `  q ) ( abs `  ( ( ( F `
 q ) `  w )  -  (
( F `  m
) `  w )
) )  <  (
r  /  2 )  <->  A. m  e.  ( ZZ>=
`  q ) A. w  e.  S  ( abs `  ( ( ( F `  q ) `
 w )  -  ( ( F `  m ) `  w
) ) )  < 
( r  /  2
) )
76 fveq2 5728 . . . . . . . . . . . . . . 15  |-  ( q  =  k  ->  ( ZZ>=
`  q )  =  ( ZZ>= `  k )
)
77 fveq2 5728 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  q
) `  w )  =  ( ( F `
 q ) `  z ) )
78 fveq2 5728 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  m
) `  w )  =  ( ( F `
 m ) `  z ) )
7977, 78oveq12d 6099 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  z  ->  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) )  =  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )
8079fveq2d 5732 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  z  ->  ( abs `  ( ( ( F `  q ) `
 w )  -  ( ( F `  m ) `  w
) ) )  =  ( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
8180breq1d 4222 . . . . . . . . . . . . . . . . 17  |-  ( w  =  z  ->  (
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 q ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8281cbvralv 2932 . . . . . . . . . . . . . . . 16  |-  ( A. w  e.  S  ( abs `  ( ( ( F `  q ) `
 w )  -  ( ( F `  m ) `  w
) ) )  < 
( r  /  2
)  <->  A. z  e.  S  ( abs `  ( ( ( F `  q
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  ( r  / 
2 ) )
83 fveq2 5728 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  =  k  ->  ( F `  q )  =  ( F `  k ) )
8483fveq1d 5730 . . . . . . . . . . . . . . . . . . . 20  |-  ( q  =  k  ->  (
( F `  q
) `  z )  =  ( ( F `
 k ) `  z ) )
8584oveq1d 6096 . . . . . . . . . . . . . . . . . . 19  |-  ( q  =  k  ->  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) )  =  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )
8685fveq2d 5732 . . . . . . . . . . . . . . . . . 18  |-  ( q  =  k  ->  ( abs `  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
8786breq1d 4222 . . . . . . . . . . . . . . . . 17  |-  ( q  =  k  ->  (
( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8887ralbidv 2725 . . . . . . . . . . . . . . . 16  |-  ( q  =  k  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  q
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  ( r  / 
2 )  <->  A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8982, 88syl5bb 249 . . . . . . . . . . . . . . 15  |-  ( q  =  k  ->  ( A. w  e.  S  ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  <->  A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
9076, 89raleqbidv 2916 . . . . . . . . . . . . . 14  |-  ( q  =  k  ->  ( A. m  e.  ( ZZ>=
`  q ) A. w  e.  S  ( abs `  ( ( ( F `  q ) `
 w )  -  ( ( F `  m ) `  w
) ) )  < 
( r  /  2
)  <->  A. m  e.  (
ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )  < 
( r  /  2
) ) )
9175, 90syl5bb 249 . . . . . . . . . . . . 13  |-  ( q  =  k  ->  ( A. w  e.  S  A. m  e.  ( ZZ>=
`  q ) ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  <->  A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  ( r  / 
2 ) ) )
9291cbvralv 2932 . . . . . . . . . . . 12  |-  ( A. q  e.  ( ZZ>= `  p ) A. w  e.  S  A. m  e.  ( ZZ>= `  q )
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  <->  A. k  e.  ( ZZ>= `  p ) A. m  e.  ( ZZ>=
`  k ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )  < 
( r  /  2
) )
93 fveq2 5728 . . . . . . . . . . . . 13  |-  ( p  =  j  ->  ( ZZ>=
`  p )  =  ( ZZ>= `  j )
)
9493raleqdv 2910 . . . . . . . . . . . 12  |-  ( p  =  j  ->  ( A. k  e.  ( ZZ>=
`  p ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 )  <->  A. k  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
9592, 94syl5bb 249 . . . . . . . . . . 11  |-  ( p  =  j  ->  ( A. q  e.  ( ZZ>=
`  p ) A. w  e.  S  A. m  e.  ( ZZ>= `  q ) ( abs `  ( ( ( F `
 q ) `  w )  -  (
( F `  m
) `  w )
) )  <  (
r  /  2 )  <->  A. k  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
9695cbvrexv 2933 . . . . . . . . . 10  |-  ( E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) A. w  e.  S  A. m  e.  ( ZZ>= `  q )
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  <->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  k ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )  < 
( r  /  2
) )
9774, 96syl6bbr 255 . . . . . . . . 9  |-  ( x  =  ( r  / 
2 )  ->  ( E. j  e.  Z  A. k  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  x  <->  E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) A. w  e.  S  A. m  e.  ( ZZ>= `  q )
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 ) ) )
9897rspccva 3051 . . . . . . . 8  |-  ( ( A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  k ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 m ) `  z ) ) )  <  x  /\  (
r  /  2 )  e.  RR+ )  ->  E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) A. w  e.  S  A. m  e.  ( ZZ>=
`  q ) ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 ) )
9969, 70, 98syl2an 464 . . . . . . 7  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  ->  E. p  e.  Z  A. q  e.  ( ZZ>=
`  p ) A. w  e.  S  A. m  e.  ( ZZ>= `  q ) ( abs `  ( ( ( F `
 q ) `  w )  -  (
( F `  m
) `  w )
) )  <  (
r  /  2 ) )
1003uztrn2 10503 . . . . . . . . . . 11  |-  ( ( p  e.  Z  /\  q  e.  ( ZZ>= `  p ) )  -> 
q  e.  Z )
101 eqid 2436 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  q )  =  (
ZZ>= `  q )
102 eluzelz 10496 . . . . . . . . . . . . . . . 16  |-  ( q  e.  ( ZZ>= `  M
)  ->  q  e.  ZZ )
103102, 3eleq2s 2528 . . . . . . . . . . . . . . 15  |-  ( q  e.  Z  ->  q  e.  ZZ )
104103ad2antlr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  q  e.  ZZ )
10570adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  -> 
( r  /  2
)  e.  RR+ )
106105ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  (
r  /  2 )  e.  RR+ )
107 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  q  e.  Z )
1083uztrn2 10503 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Z  /\  m  e.  ( ZZ>= `  q ) )  ->  m  e.  Z )
109107, 108sylan 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  m  e.  Z )
110 fveq2 5728 . . . . . . . . . . . . . . . . 17  |-  ( n  =  m  ->  ( F `  n )  =  ( F `  m ) )
111110fveq1d 5730 . . . . . . . . . . . . . . . 16  |-  ( n  =  m  ->  (
( F `  n
) `  w )  =  ( ( F `
 m ) `  w ) )
112 eqid 2436 . . . . . . . . . . . . . . . 16  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) )
113 fvex 5742 . . . . . . . . . . . . . . . 16  |-  ( ( F `  m ) `
 w )  e. 
_V
114111, 112, 113fvmpt 5806 . . . . . . . . . . . . . . 15  |-  ( m  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  w
) ) `  m
)  =  ( ( F `  m ) `
 w ) )
115109, 114syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  ( (
n  e.  Z  |->  ( ( F `  n
) `  w )
) `  m )  =  ( ( F `
 m ) `  w ) )
1166adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  ->  F : Z --> ( CC 
^m  S ) )
117116ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  n  e.  Z )  ->  ( F `  n
)  e.  ( CC 
^m  S ) )
118 elmapi 7038 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  n )  e.  ( CC  ^m  S )  ->  ( F `  n ) : S --> CC )
119117, 118syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  n  e.  Z )  ->  ( F `  n
) : S --> CC )
120119ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  n  e.  Z )  /\  y  e.  S
)  ->  ( ( F `  n ) `  y )  e.  CC )
121120an32s 780 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  /\  n  e.  Z
)  ->  ( ( F `  n ) `  y )  e.  CC )
122 eqid 2436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  y ) )
123121, 122fmptd 5893 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  ->  ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) : Z --> CC )
124123ffvelrnda 5870 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  /\  q  e.  Z
)  ->  ( (
n  e.  Z  |->  ( ( F `  n
) `  y )
) `  q )  e.  CC )
125 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  y ) )
126 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  j
) `  z )  =  ( ( F `
 j ) `  y ) )
127125, 126oveq12d 6099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) )  =  ( ( ( F `  k ) `
 y )  -  ( ( F `  j ) `  y
) ) )
128127fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) ) )
129128breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  y  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
130129rspcv 3048 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  S  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x  ->  ( abs `  ( ( ( F `  k ) `
 y )  -  ( ( F `  j ) `  y
) ) )  < 
x ) )
131130ralimdv 2785 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  S  ->  ( A. k  e.  ( ZZ>=
`  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x  ->  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  x ) )
132131reximdv 2817 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  S  ->  ( E. j  e.  Z  A. k  e.  ( ZZ>=
`  j ) A. z  e.  S  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  < 
x  ->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  x ) )
133132ralimdv 2785 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  S  ->  ( A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  x ) )
134133impcom 420 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x  /\  y  e.  S
)  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  x )
135134adantll 695 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
)
136 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( q  =  k  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  q
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  k )
)
137136oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( q  =  k  ->  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  q )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) )  =  ( ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) ) )
138137fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( q  =  k  ->  ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  q )  -  ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 p ) ) )  =  ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 k )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  p ) ) ) )
139138breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( q  =  k  ->  (
( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  q )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) ) )  < 
r  <->  ( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) ) )  < 
r ) )
140139cbvralv 2932 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. q  e.  ( ZZ>= `  p ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 q )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  p ) ) )  <  r  <->  A. k  e.  ( ZZ>= `  p )
( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) ) )  < 
r )
141 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  =  j  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  j )
)
142141oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( p  =  j  ->  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) )  =  ( ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
) ) )
143142fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  =  j  ->  ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  k )  -  ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 p ) ) )  =  ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 k )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j ) ) ) )
144143breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  j  ->  (
( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) ) )  < 
r  <->  ( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
) ) )  < 
r ) )
14593, 144raleqbidv 2916 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  j  ->  ( A. k  e.  ( ZZ>=
`  p ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  k
)  -  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  p )
) )  <  r  <->  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 k )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j ) ) )  <  r ) )
146140, 145syl5bb 249 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  j  ->  ( A. q  e.  ( ZZ>=
`  p ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  q
)  -  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  p )
) )  <  r  <->  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 k )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j ) ) )  <  r ) )
147146cbvrexv 2933 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 q )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  p ) ) )  <  r  <->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
) ) )  < 
r )
148 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
149148fveq1d 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  (
( F `  n
) `  y )  =  ( ( F `
 k ) `  y ) )
150 fvex 5742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  k ) `
 y )  e. 
_V
151149, 122, 150fvmpt 5806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  k
)  =  ( ( F `  k ) `
 y ) )
15239, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  =  ( ( F `  k
) `  y )
)
153 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  j  ->  ( F `  n )  =  ( F `  j ) )
154153fveq1d 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  j  ->  (
( F `  n
) `  y )  =  ( ( F `
 j ) `  y ) )
155 fvex 5742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  j ) `
 y )  e. 
_V
156154, 122, 155fvmpt 5806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
)  =  ( ( F `  j ) `
 y ) )
157156adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j )  =  ( ( F `  j
) `  y )
)
158152, 157oveq12d 6099 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 k )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j ) )  =  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )
159158fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
) ) )  =  ( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) ) )
160159breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
) ) )  < 
r  <->  ( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  r ) )
161160ralbidva 2721 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  Z  ->  ( A. k  e.  ( ZZ>=
`  j ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  k
)  -  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  j )
) )  <  r  <->  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  r
) )
162161rexbiia 2738 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 k )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j ) ) )  <  r  <->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  r )
163147, 162bitri 241 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 q )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  p ) ) )  <  r  <->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  r )
164 breq2 4216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( r  =  x  ->  (
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  r  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
165164ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  =  x  ->  ( A. k  e.  ( ZZ>=
`  j ) ( abs `  ( ( ( F `  k
) `  y )  -  ( ( F `
 j ) `  y ) ) )  <  r  <->  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  x ) )
166165rexbidv 2726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( r  =  x  ->  ( E. j  e.  Z  A. k  e.  ( ZZ>=
`  j ) ( abs `  ( ( ( F `  k
) `  y )  -  ( ( F `
 j ) `  y ) ) )  <  r  <->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  x ) )
167163, 166syl5bb 249 . . . . . . . . . . . . . . . . . . . . 21  |-  ( r  =  x  ->  ( E. p  e.  Z  A. q  e.  ( ZZ>=
`  p ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  q
)  -  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  p )
) )  <  r  <->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
168167cbvralv 2932 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. r  e.  RR+  E. p  e.  Z  A. q  e.  ( ZZ>= `  p )
( abs `  (
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  q )  -  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
) ) )  < 
r  <->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
)
169135, 168sylibr 204 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  ->  A. r  e.  RR+  E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) ( abs `  ( ( ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) `
 q )  -  ( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  p ) ) )  <  r )
170 fvex 5742 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ZZ>= `  M )  e.  _V
1713, 170eqeltri 2506 . . . . . . . . . . . . . . . . . . . . 21  |-  Z  e. 
_V
172171mptex 5966 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  e.  _V
173172a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  ->  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  _V )
1743, 124, 169, 173caucvg 12472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  ->  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  )
175174ralrimiva 2789 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  ->  A. y  e.  S  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  )
176175ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  ->  A. y  e.  S  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  )
177 fveq2 5728 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  w  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  w ) )
178177mpteq2dv 4296 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  w  ->  (
n  e.  Z  |->  ( ( F `  n
) `  y )
)  =  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) )
179178eleq1d 2502 . . . . . . . . . . . . . . . . 17  |-  ( y  =  w  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  <->  (
n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  ) )
180179rspccva 3051 . . . . . . . . . . . . . . . 16  |-  ( ( A. y  e.  S  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  /\  w  e.  S )  ->  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) )  e. 
dom 
~~>  )
181176, 180sylan 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  (
n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  )
182 climdm 12348 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  <->  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) )  ~~>  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) )
183181, 182sylib 189 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  (
n  e.  Z  |->  ( ( F `  n
) `  w )
)  ~~>  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) )
184101, 104, 106, 115, 183climi2 12305 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  E. v  e.  ( ZZ>= `  q ) A. m  e.  ( ZZ>=
`  v ) ( abs `  ( ( ( F `  m
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
( r  /  2
) )
185101r19.29uz 12154 . . . . . . . . . . . . . . 15  |-  ( ( A. m  e.  (
ZZ>= `  q ) ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  /\  E. v  e.  ( ZZ>= `  q ) A. m  e.  ( ZZ>= `  v )
( abs `  (
( ( F `  m ) `  w
)  -  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) ) )  <  ( r  / 
2 ) )  ->  E. v  e.  ( ZZ>=
`  q ) A. m  e.  ( ZZ>= `  v ) ( ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  /\  ( abs `  ( ( ( F `  m ) `
 w )  -  ( 
~~>  `  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) ) ) ) )  <  (
r  /  2 ) ) )
186101r19.2uz 12155 . . . . . . . . . . . . . . 15  |-  ( E. v  e.  ( ZZ>= `  q ) A. m  e.  ( ZZ>= `  v )
( ( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  /\  ( abs `  ( ( ( F `  m
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
( r  /  2
) )  ->  E. m  e.  ( ZZ>= `  q )
( ( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  /\  ( abs `  ( ( ( F `  m
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
( r  /  2
) ) )
187185, 186syl 16 . . . . . . . . . . . . . 14  |-  ( ( A. m  e.  (
ZZ>= `  q ) ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  /\  E. v  e.  ( ZZ>= `  q ) A. m  e.  ( ZZ>= `  v )
( abs `  (
( ( F `  m ) `  w
)  -  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) ) )  <  ( r  / 
2 ) )  ->  E. m  e.  ( ZZ>=
`  q ) ( ( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  /\  ( abs `  ( ( ( F `  m
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
( r  /  2
) ) )
1886ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  ->  F : Z --> ( CC 
^m  S ) )
189188ffvelrnda 5870 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  ->  ( F `  q
)  e.  ( CC 
^m  S ) )
190 elmapi 7038 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  q )  e.  ( CC  ^m  S )  ->  ( F `  q ) : S --> CC )
191189, 190syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  ->  ( F `  q
) : S --> CC )
192191ffvelrnda 5870 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  (
( F `  q
) `  w )  e.  CC )
193192adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  ( ( F `  q ) `  w )  e.  CC )
194 climcl 12293 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  w )
)  ~~>  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) )  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  w
) ) )  e.  CC )
195183, 194syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  w
) ) )  e.  CC )
196195adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) )  e.  CC )
1976ad5antr 715 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  F : Z
--> ( CC  ^m  S
) )
198197, 109ffvelrnd 5871 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  ( F `  m )  e.  ( CC  ^m  S ) )
199 elmapi 7038 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  m )  e.  ( CC  ^m  S )  ->  ( F `  m ) : S --> CC )
200198, 199syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  ( F `  m ) : S --> CC )
201 simplr 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  w  e.  S )
202200, 201ffvelrnd 5871 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  ( ( F `  m ) `  w )  e.  CC )
203 rpre 10618 . . . . . . . . . . . . . . . . 17  |-  ( r  e.  RR+  ->  r  e.  RR )
204203ad4antlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  r  e.  RR )
205 abs3lem 12142 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( F `
 q ) `  w )  e.  CC  /\  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) )  e.  CC )  /\  ( ( ( F `  m ) `
 w )  e.  CC  /\  r  e.  RR ) )  -> 
( ( ( abs `  ( ( ( F `
 q ) `  w )  -  (
( F `  m
) `  w )
) )  <  (
r  /  2 )  /\  ( abs `  (
( ( F `  m ) `  w
)  -  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) ) )  <  ( r  / 
2 ) )  -> 
( abs `  (
( ( F `  q ) `  w
)  -  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) ) )  <  r ) )
206193, 196, 202, 204, 205syl22anc 1185 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S
)  /\  m  e.  ( ZZ>= `  q )
)  ->  ( (
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  /\  ( abs `  ( ( ( F `  m
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
( r  /  2
) )  ->  ( abs `  ( ( ( F `  q ) `
 w )  -  ( 
~~>  `  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) ) ) ) )  <  r
) )
207206rexlimdva 2830 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  ( E. m  e.  ( ZZ>=
`  q ) ( ( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  /\  ( abs `  ( ( ( F `  m
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
( r  /  2
) )  ->  ( abs `  ( ( ( F `  q ) `
 w )  -  ( 
~~>  `  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) ) ) ) )  <  r
) )
208187, 207syl5 30 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  (
( A. m  e.  ( ZZ>= `  q )
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  /\  E. v  e.  ( ZZ>= `  q ) A. m  e.  ( ZZ>= `  v )
( abs `  (
( ( F `  m ) `  w
)  -  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) ) )  <  ( r  / 
2 ) )  -> 
( abs `  (
( ( F `  q ) `  w
)  -  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) ) )  <  r ) )
209184, 208mpan2d 656 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  ( A. m  e.  ( ZZ>=
`  q ) ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  ->  ( abs `  ( ( ( F `  q ) `
 w )  -  ( 
~~>  `  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) ) ) ) )  <  r
) )
210209ralimdva 2784 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  q  e.  Z )  ->  ( A. w  e.  S  A. m  e.  ( ZZ>= `  q )
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  ->  A. w  e.  S  ( abs `  ( ( ( F `  q
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
r ) )
211100, 210sylan2 461 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  ( p  e.  Z  /\  q  e.  ( ZZ>=
`  p ) ) )  ->  ( A. w  e.  S  A. m  e.  ( ZZ>= `  q ) ( abs `  ( ( ( F `
 q ) `  w )  -  (
( F `  m
) `  w )
) )  <  (
r  /  2 )  ->  A. w  e.  S  ( abs `  ( ( ( F `  q
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
r ) )
212211anassrs 630 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  p  e.  Z )  /\  q  e.  ( ZZ>= `  p )
)  ->  ( A. w  e.  S  A. m  e.  ( ZZ>= `  q ) ( abs `  ( ( ( F `
 q ) `  w )  -  (
( F `  m
) `  w )
) )  <  (
r  /  2 )  ->  A. w  e.  S  ( abs `  ( ( ( F `  q
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
r ) )
213212ralimdva 2784 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  /\  p  e.  Z )  ->  ( A. q  e.  ( ZZ>= `  p ) A. w  e.  S  A. m  e.  ( ZZ>=
`  q ) ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  ->  A. q  e.  ( ZZ>= `  p ) A. w  e.  S  ( abs `  ( ( ( F `  q
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
r ) )
214213reximdva 2818 . . . . . . 7  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  -> 
( E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) A. w  e.  S  A. m  e.  ( ZZ>=
`  q ) ( abs `  ( ( ( F `  q
) `  w )  -  ( ( F `
 m ) `  w ) ) )  <  ( r  / 
2 )  ->  E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) A. w  e.  S  ( abs `  ( ( ( F `  q
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
r ) )
21599, 214mpd 15 . . . . . 6  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  r  e.  RR+ )  ->  E. p  e.  Z  A. q  e.  ( ZZ>=
`  p ) A. w  e.  S  ( abs `  ( ( ( F `  q ) `
 w )  -  ( 
~~>  `  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) ) ) ) )  <  r
)
216215ralrimiva 2789 . . . . 5  |-  ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  ->  A. r  e.  RR+  E. p  e.  Z  A. q  e.  ( ZZ>= `  p ) A. w  e.  S  ( abs `  ( ( ( F `  q
) `  w )  -  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) ) )  < 
r )
2174adantr 452 . . . . . 6  |-  ( (
ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  ->  M  e.  ZZ )
218 eqidd 2437 . . . . . 6  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  ( q  e.  Z  /\  w  e.  S
) )  ->  (
( F `  q
) `  w )  =  ( ( F `
 q ) `  w ) )
219178fveq2d 5732 . . . . . . . 8  |-  ( y  =  w  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) )  =  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) )
220 eqid 2436 . . . . . . . 8  |-  ( y  e.  S  |->  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  y )
) ) )  =  ( y  e.  S  |->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) )
221 fvex 5742 . . . . . . . 8  |-  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) )  e.  _V
222219, 220, 221fvmpt 5806 . . . . . . 7  |-  ( w  e.  S  ->  (
( y  e.  S  |->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) ) `  w
)  =  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) )
223222adantl 453 . . . . . 6  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  w  e.  S )  ->  ( ( y  e.  S  |->  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  y )
) ) ) `  w )  =  (  ~~>  `
 ( n  e.  Z  |->  ( ( F `
 n ) `  w ) ) ) )
224 climdm 12348 . . . . . . . . 9  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
)  e.  dom  ~~>  <->  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  ~~>  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) )
225174, 224sylib 189 . . . . . . . 8  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x )  /\  y  e.  S )  ->  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  ~~>  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  y )
) ) )
226 climcl 12293 . . . . . . . 8  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
)  ~~>  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  y )
) )  ->  (  ~~>  `  ( n  e.  Z  |->  ( (