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

Theorem ulmcau 21803
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 21804 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 5031 . . . 4  |-  ( F  e.  dom  ( ~~> u `  S )  ->  ( F  e.  dom  ( ~~> u `  S )  <->  E. g  F ( ~~> u `  S ) g ) )
21ibi 241 . . 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 720 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  M  e.  ZZ )
6 ulmcau.f . . . . . . . . 9  |-  ( ph  ->  F : Z --> ( CC 
^m  S ) )
76ad2antrr 720 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F : Z --> ( CC 
^m  S ) )
8 eqidd 2442 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( k  e.  Z  /\  z  e.  S ) )  -> 
( ( F `  k ) `  z
)  =  ( ( F `  k ) `
 z ) )
9 eqidd 2442 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  z  e.  S
)  ->  ( g `  z )  =  ( g `  z ) )
10 simplr 749 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F ( ~~> u `  S ) g )
11 rphalfcl 11011 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR+ )
1211adantl 463 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  -> 
( x  /  2
)  e.  RR+ )
133, 5, 7, 8, 9, 10, 12ulmi 21794 . . . . . . 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 458 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  Z )
1514, 3syl6eleq 2531 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  ( ZZ>= `  M )
)
16 eluzelz 10866 . . . . . . . . . 10  |-  ( j  e.  ( ZZ>= `  M
)  ->  j  e.  ZZ )
17 uzid 10871 . . . . . . . . . 10  |-  ( j  e.  ZZ  ->  j  e.  ( ZZ>= `  j )
)
18 fveq2 5688 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  ( F `  k )  =  ( F `  j ) )
1918fveq1d 5690 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( F `  k
) `  z )  =  ( ( F `
 j ) `  z ) )
2019oveq1d 6105 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ( F `  k ) `  z
)  -  ( g `
 z ) )  =  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )
2120fveq2d 5692 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  =  ( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) ) )
2221breq1d 4299 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  <->  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) ) )
2322ralbidv 2733 . . . . . . . . . . 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 ) ) )
2423rspcv 3066 . . . . . . . . . 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 ) ) )
2515, 16, 17, 244syl 21 . . . . . . . . 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 ) ) )
26 r19.26 2847 . . . . . . . . . . . . . . 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 ) ) )
277ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
2827adantr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
29 elmapi 7230 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  j )  e.  ( CC  ^m  S )  ->  ( F `  j ) : S --> CC )
3028, 29syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  j ) : S --> CC )
3130ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( F `  j
) `  z )  e.  CC )
32 ulmcl 21789 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F ( ~~> u `  S
) g  ->  g : S --> CC )
3332ad4antlr 727 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  g : S
--> CC )
3433ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
g `  z )  e.  CC )
3531, 34abssubd 12935 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
3635breq1d 4299 . . . . . . . . . . . . . . . . . . 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 ) ) )
3736biimpd 207 . . . . . . . . . . . . . . . . . 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 ) ) )
383uztrn2 10874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
k  e.  Z )
39 ffvelrn 5838 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : Z --> ( CC 
^m  S )  /\  k  e.  Z )  ->  ( F `  k
)  e.  ( CC 
^m  S ) )
407, 38, 39syl2an 474 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( j  e.  Z  /\  k  e.  ( ZZ>= `  j )
) )  ->  ( F `  k )  e.  ( CC  ^m  S
) )
4140anassrs 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  k )  e.  ( CC  ^m  S ) )
42 elmapi 7230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  k )  e.  ( CC  ^m  S )  ->  ( F `  k ) : S --> CC )
4341, 42syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  k ) : S --> CC )
4443ffvelrnda 5840 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( F `  k
) `  z )  e.  CC )
45 rpre 10993 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  RR )
4645ad4antlr 727 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  x  e.  RR )
47 abs3lem 12822 . . . . . . . . . . . . . . . . . . 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 ) )
4844, 31, 34, 46, 47syl22anc 1214 . . . . . . . . . . . . . . . . . 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 ) )
4937, 48sylan2d 479 . . . . . . . . . . . . . . . . 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 ) )
5049ancomsd 451 . . . . . . . . . . . . . . . 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 ) )
5150ralimdva 2792 . . . . . . . . . . . . . . 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 ) )
5226, 51syl5bir 218 . . . . . . . . . . . . . 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
) )
5352expdimp 437 . . . . . . . . . . . . 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
) )
5453an32s 797 . . . . . . . . . . . 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
) )
5554ralimdva 2792 . . . . . . . . . . 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 ) )
5655ex 434 . . . . . . . . . 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 ) ) )
5756com23 78 . . . . . . . . 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 ) ) )
5825, 57mpdd 40 . . . . . . . 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 ) )
5958reximdva 2826 . . . . . . 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 ) )
6013, 59mpd 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 )
6160ralrimiva 2797 . . . . 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 )
6261ex 434 . . . 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 ) )
6362exlimdv 1695 . . 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 ) )
642, 63syl5 32 . 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
) )
65 ulmrel 21786 . . . 4  |-  Rel  ( ~~> u `  S )
66 ulmcau.s . . . . . . . . . 10  |-  ( ph  ->  S  e.  V )
673, 4, 66, 6ulmcaulem 21802 . . . . . . . . 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 ) )
6867biimpa 481 . . . . . . . 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 )
69 rphalfcl 11011 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
70 breq2 4293 . . . . . . . . . . . . 13  |-  ( x  =  ( r  / 
2 )  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
7170ralbidv 2733 . . . . . . . . . . . 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 ) ) )
72712ralbidv 2755 . . . . . . . . . . 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 ) ) )
7372rexbidv 2734 . . . . . . . . . 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 ) ) )
74 ralcom 2879 . . . . . . . . . . . . . 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
) )
75 fveq2 5688 . . . . . . . . . . . . . . 15  |-  ( q  =  k  ->  ( ZZ>=
`  q )  =  ( ZZ>= `  k )
)
76 fveq2 5688 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  q
) `  w )  =  ( ( F `
 q ) `  z ) )
77 fveq2 5688 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  m
) `  w )  =  ( ( F `
 m ) `  z ) )
7876, 77oveq12d 6108 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  z  ->  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) )  =  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )
7978fveq2d 5692 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  z  ->  ( abs `  ( ( ( F `  q ) `
 w )  -  ( ( F `  m ) `  w
) ) )  =  ( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
8079breq1d 4299 . . . . . . . . . . . . . . . . 17  |-  ( w  =  z  ->  (
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 q ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8180cbvralv 2945 . . . . . . . . . . . . . . . 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 ) )
82 fveq2 5688 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  =  k  ->  ( F `  q )  =  ( F `  k ) )
8382fveq1d 5690 . . . . . . . . . . . . . . . . . . . 20  |-  ( q  =  k  ->  (
( F `  q
) `  z )  =  ( ( F `
 k ) `  z ) )
8483oveq1d 6105 . . . . . . . . . . . . . . . . . . 19  |-  ( q  =  k  ->  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) )  =  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )
8584fveq2d 5692 . . . . . . . . . . . . . . . . . 18  |-  ( q  =  k  ->  ( abs `  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
8685breq1d 4299 . . . . . . . . . . . . . . . . 17  |-  ( q  =  k  ->  (
( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8786ralbidv 2733 . . . . . . . . . . . . . . . 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 ) ) )
8881, 87syl5bb 257 . . . . . . . . . . . . . . 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 ) ) )
8975, 88raleqbidv 2929 . . . . . . . . . . . . . 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
) ) )
9074, 89syl5bb 257 . . . . . . . . . . . . 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 ) ) )
9190cbvralv 2945 . . . . . . . . . . . 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
) )
92 fveq2 5688 . . . . . . . . . . . . 13  |-  ( p  =  j  ->  ( ZZ>=
`  p )  =  ( ZZ>= `  j )
)
9392raleqdv 2921 . . . . . . . . . . . 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 ) ) )
9491, 93syl5bb 257 . . . . . . . . . . 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 ) ) )
9594cbvrexv 2946 . . . . . . . . . 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
) )
9673, 95syl6bbr 263 . . . . . . . . 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 ) ) )
9796rspccva 3069 . . . . . . . 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 ) )
9868, 69, 97syl2an 474 . . . . . . 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 ) )
993uztrn2 10874 . . . . . . . . . . 11  |-  ( ( p  e.  Z  /\  q  e.  ( ZZ>= `  p ) )  -> 
q  e.  Z )
100 eqid 2441 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  q )  =  (
ZZ>= `  q )
101 eluzelz 10866 . . . . . . . . . . . . . . . 16  |-  ( q  e.  ( ZZ>= `  M
)  ->  q  e.  ZZ )
102101, 3eleq2s 2533 . . . . . . . . . . . . . . 15  |-  ( q  e.  Z  ->  q  e.  ZZ )
103102ad2antlr 721 . . . . . . . . . . . . . 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 )
10469adantl 463 . . . . . . . . . . . . . . 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+ )
105104ad2antrr 720 . . . . . . . . . . . . . 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+ )
106 simplr 749 . . . . . . . . . . . . . . . 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 )
1073uztrn2 10874 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Z  /\  m  e.  ( ZZ>= `  q ) )  ->  m  e.  Z )
108106, 107sylan 468 . . . . . . . . . . . . . . 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 )
109 fveq2 5688 . . . . . . . . . . . . . . . . 17  |-  ( n  =  m  ->  ( F `  n )  =  ( F `  m ) )
110109fveq1d 5690 . . . . . . . . . . . . . . . 16  |-  ( n  =  m  ->  (
( F `  n
) `  w )  =  ( ( F `
 m ) `  w ) )
111 eqid 2441 . . . . . . . . . . . . . . . 16  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) )
112 fvex 5698 . . . . . . . . . . . . . . . 16  |-  ( ( F `  m ) `
 w )  e. 
_V
113110, 111, 112fvmpt 5771 . . . . . . . . . . . . . . 15  |-  ( m  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  w
) ) `  m
)  =  ( ( F `  m ) `
 w ) )
114108, 113syl 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 ) )
1156adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
116115ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
117 elmapi 7230 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  n )  e.  ( CC  ^m  S )  ->  ( F `  n ) : S --> CC )
118116, 117syl 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 )
119118ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . . 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 )
120119an32s 797 . . . . . . . . . . . . . . . . . . . . 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 )
121 eqid 2441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  y ) )
122120, 121fmptd 5864 . . . . . . . . . . . . . . . . . . . 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 )
123122ffvelrnda 5840 . . . . . . . . . . . . . . . . . . 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 )
124 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  y ) )
125 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  j
) `  z )  =  ( ( F `
 j ) `  y ) )
126124, 125oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) )  =  ( ( ( F `  k ) `
 y )  -  ( ( F `  j ) `  y
) ) )
127126fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) ) )
128127breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  y  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
129128rspcv 3066 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  S  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x  ->  ( abs `  ( ( ( F `  k ) `
 y )  -  ( ( F `  j ) `  y
) ) )  < 
x ) )
130129ralimdv 2793 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
131130reximdv 2825 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
132131ralimdv 2793 . . . . . . . . . . . . . . . . . . . . . 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 ) )
133132impcom 430 . . . . . . . . . . . . . . . . . . . . 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 )
134133adantll 708 . . . . . . . . . . . . . . . . . . . 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
)
135 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( q  =  k  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  q
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  k )
)
136135oveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
137136fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
138137breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
139138cbvralv 2945 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
140 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  =  j  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  j )
)
141140oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
142141fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
143142breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
14492, 143raleqbidv 2929 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
145139, 144syl5bb 257 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
146145cbvrexv 2946 . . . . . . . . . . . . . . . . . . . . . . 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 )
147 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
148147fveq1d 5690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  (
( F `  n
) `  y )  =  ( ( F `
 k ) `  y ) )
149 fvex 5698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  k ) `
 y )  e. 
_V
150148, 121, 149fvmpt 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  k
)  =  ( ( F `  k ) `
 y ) )
15138, 150syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  =  ( ( F `  k
) `  y )
)
152 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  j  ->  ( F `  n )  =  ( F `  j ) )
153152fveq1d 5690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  j  ->  (
( F `  n
) `  y )  =  ( ( F `
 j ) `  y ) )
154 fvex 5698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  j ) `
 y )  e. 
_V
155153, 121, 154fvmpt 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
)  =  ( ( F `  j ) `
 y ) )
156155adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j )  =  ( ( F `  j
) `  y )
)
157151, 156oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
158157fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
159158breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
160159ralbidva 2729 . . . . . . . . . . . . . . . . . . . . . . . 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
) )
161160rexbiia 2746 . . . . . . . . . . . . . . . . . . . . . . 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 )
162146, 161bitri 249 . . . . . . . . . . . . . . . . . . . . . 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 )
163 breq2 4293 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( r  =  x  ->  (
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  r  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
164163ralbidv 2733 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
165164rexbidv 2734 . . . . . . . . . . . . . . . . . . . . . 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 ) )
166162, 165syl5bb 257 . . . . . . . . . . . . . . . . . . . . 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
) )
167166cbvralv 2945 . . . . . . . . . . . . . . . . . . . 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
)
168134, 167sylibr 212 . . . . . . . . . . . . . . . . . . 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 )
169 fvex 5698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ZZ>= `  M )  e.  _V
1703, 169eqeltri 2511 . . . . . . . . . . . . . . . . . . . . 21  |-  Z  e. 
_V
171170mptex 5945 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  e.  _V
172171a1i 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 )
1733, 123, 168, 172caucvg 13152 . . . . . . . . . . . . . . . . . 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  ~~>  )
174173ralrimiva 2797 . . . . . . . . . . . . . . . . 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  ~~>  )
175174ad2antrr 720 . . . . . . . . . . . . . . . 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  ~~>  )
176 fveq2 5688 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  w  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  w ) )
177176mpteq2dv 4376 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  w  ->  (
n  e.  Z  |->  ( ( F `  n
) `  y )
)  =  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) )
178177eleq1d 2507 . . . . . . . . . . . . . . . . 17  |-  ( y  =  w  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  <->  (
n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  ) )
179178rspccva 3069 . . . . . . . . . . . . . . . 16  |-  ( ( A. y  e.  S  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  /\  w  e.  S )  ->  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) )  e. 
dom 
~~>  )
180175, 179sylan 468 . . . . . . . . . . . . . . 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  ~~>  )
181 climdm 13028 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  <->  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) )  ~~>  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) )
182180, 181sylib 196 . . . . . . . . . . . . . 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 )
) ) )
183100, 103, 105, 114, 182climi2 12985 . . . . . . . . . . . . 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
) )
184100r19.29uz 12834 . . . . . . . . . . . . . . 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 ) ) )
185100r19.2uz 12835 . . . . . . . . . . . . . . 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
) ) )
186184, 185syl 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
) ) )
1876ad2antrr 720 . . . . . . . . . . . . . . . . . . . 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 ) )
188187ffvelrnda 5840 . . . . . . . . . . . . . . . . . . 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 ) )
189 elmapi 7230 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  q )  e.  ( CC  ^m  S )  ->  ( F `  q ) : S --> CC )
190188, 189syl 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 )
191190ffvelrnda 5840 . . . . . . . . . . . . . . . . 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 )
192191adantr 462 . . . . . . . . . . . . . . . 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 )
193 climcl 12973 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  w )
)  ~~>  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) )  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  w
) ) )  e.  CC )
194182, 193syl 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 )
195194adantr 462 . . . . . . . . . . . . . . . 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 )
1966ad5antr 728 . . . . . . . . . . . . . . . . . . 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
) )
197196, 108ffvelrnd 5841 . . . . . . . . . . . . . . . . . 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 ) )
198 elmapi 7230 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  m )  e.  ( CC  ^m  S )  ->  ( F `  m ) : S --> CC )
199197, 198syl 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 )
200 simplr 749 . . . . . . . . . . . . . . . . 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 )
201199, 200ffvelrnd 5841 . . . . . . . . . . . . . . . 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 )
202 rpre 10993 . . . . . . . . . . . . . . . . 17  |-  ( r  e.  RR+  ->  r  e.  RR )
203202ad4antlr 727 . . . . . . . . . . . . . . . 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 )
204 abs3lem 12822 . . . . . . . . . . . . . . . 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 ) )
205192, 195, 201, 203, 204syl22anc 1214 . . . . . . . . . . . . . . 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
) )
206205rexlimdva 2839 . . . . . . . . . . . . . 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
) )
207186, 206syl5 32 . . . . . . . . . . . . 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 ) )
208183, 207mpan2d 669 . . . . . . . . . . . 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
) )
209208ralimdva 2792 . . . . . . . . . . 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 ) )
21099, 209sylan2 471 . . . . . . . . . 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 ) )
211210anassrs 643 . . . . . . . . 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 ) )
212211ralimdva 2792 . . . . . . . 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 ) )
213212reximdva 2826 . . . . . . 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 ) )
21498, 213mpd 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
)
215214ralrimiva 2797 . . . . 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 )
2164adantr 462 . . . . . 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 )
217 eqidd 2442 . . . . . 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 ) )
218177fveq2d 5692 . . . . . . . 8  |-  ( y  =  w  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) )  =  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) )
219 eqid 2441 . . . . . . . 8  |-  ( y  e.  S  |->  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  y )
) ) )  =  ( y  e.  S  |->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) )
220 fvex 5698 . . . . . . . 8  |-  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) )  e.  _V
221218, 219, 220fvmpt 5771 . . . . . . 7  |-  ( w  e.  S  ->  (
( y  e.  S  |->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) ) `  w
)  =  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) )
222221adantl 463 . . . . . 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 ) ) ) )
223 climdm 13028 . . . . . . . . 9  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
)  e.  dom  ~~>  <->  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  ~~>  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) )
224173, 223sylib 196 . . . . . . . 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 )
) ) )
225 climcl 12973 . . . . . . . 8  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
)  ~~>  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  y )
) )  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) )  e.  CC )
226224, 225syl 16 . . . . . . 7  |-  ( ( ( ph  /\  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A.