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

Theorem ulmcau 21860
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 21861 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 5035 . . . 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 725 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  M  e.  ZZ )
6 ulmcau.f . . . . . . . . 9  |-  ( ph  ->  F : Z --> ( CC 
^m  S ) )
76ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F : Z --> ( CC 
^m  S ) )
8 eqidd 2444 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( k  e.  Z  /\  z  e.  S ) )  -> 
( ( F `  k ) `  z
)  =  ( ( F `  k ) `
 z ) )
9 eqidd 2444 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  z  e.  S
)  ->  ( g `  z )  =  ( g `  z ) )
10 simplr 754 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F ( ~~> u `  S ) g )
11 rphalfcl 11015 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR+ )
1211adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  -> 
( x  /  2
)  e.  RR+ )
133, 5, 7, 8, 9, 10, 12ulmi 21851 . . . . . . 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 461 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  Z )
1514, 3syl6eleq 2533 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  ( ZZ>= `  M )
)
16 eluzelz 10870 . . . . . . . . . 10  |-  ( j  e.  ( ZZ>= `  M
)  ->  j  e.  ZZ )
17 uzid 10875 . . . . . . . . . 10  |-  ( j  e.  ZZ  ->  j  e.  ( ZZ>= `  j )
)
18 fveq2 5691 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  ( F `  k )  =  ( F `  j ) )
1918fveq1d 5693 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( F `  k
) `  z )  =  ( ( F `
 j ) `  z ) )
2019oveq1d 6106 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ( F `  k ) `  z
)  -  ( g `
 z ) )  =  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )
2120fveq2d 5695 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  =  ( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) ) )
2221breq1d 4302 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  <->  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) ) )
2322ralbidv 2735 . . . . . . . . . . 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 3069 . . . . . . . . . 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 2849 . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
2827adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
29 elmapi 7234 . . . . . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . . . 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 21846 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F ( ~~> u `  S
) g  ->  g : S --> CC )
3332ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  g : S
--> CC )
3433ffvelrnda 5843 . . . . . . . . . . . . . . . . . . . . 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 12939 . . . . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . . . . 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 10878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
k  e.  Z )
39 ffvelrn 5841 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : Z --> ( CC 
^m  S )  /\  k  e.  Z )  ->  ( F `  k
)  e.  ( CC 
^m  S ) )
407, 38, 39syl2an 477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( j  e.  Z  /\  k  e.  ( ZZ>= `  j )
) )  ->  ( F `  k )  e.  ( CC  ^m  S
) )
4140anassrs 648 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  k )  e.  ( CC  ^m  S ) )
42 elmapi 7234 . . . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . 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 10997 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  RR )
4645ad4antlr 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  x  e.  RR )
47 abs3lem 12826 . . . . . . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . . 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 802 . . . . . . . . . . . 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 2794 . . . . . . . . . . 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 2828 . . . . . . 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 2799 . . . . 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 1690 . . 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 21843 . . . 4  |-  Rel  ( ~~> u `  S )
66 ulmcau.s . . . . . . . . . 10  |-  ( ph  ->  S  e.  V )
673, 4, 66, 6ulmcaulem 21859 . . . . . . . . 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 484 . . . . . . . 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 11015 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
70 breq2 4296 . . . . . . . . . . . . 13  |-  ( x  =  ( r  / 
2 )  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
7170ralbidv 2735 . . . . . . . . . . . 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 2757 . . . . . . . . . . 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 2736 . . . . . . . . . 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 2881 . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . 15  |-  ( q  =  k  ->  ( ZZ>=
`  q )  =  ( ZZ>= `  k )
)
76 fveq2 5691 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  q
) `  w )  =  ( ( F `
 q ) `  z ) )
77 fveq2 5691 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  m
) `  w )  =  ( ( F `
 m ) `  z ) )
7876, 77oveq12d 6109 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  z  ->  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) )  =  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )
7978fveq2d 5695 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  z  ->  ( abs `  ( ( ( F `  q ) `
 w )  -  ( ( F `  m ) `  w
) ) )  =  ( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
8079breq1d 4302 . . . . . . . . . . . . . . . . 17  |-  ( w  =  z  ->  (
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 q ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8180cbvralv 2947 . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  =  k  ->  ( F `  q )  =  ( F `  k ) )
8382fveq1d 5693 . . . . . . . . . . . . . . . . . . . 20  |-  ( q  =  k  ->  (
( F `  q
) `  z )  =  ( ( F `
 k ) `  z ) )
8483oveq1d 6106 . . . . . . . . . . . . . . . . . . 19  |-  ( q  =  k  ->  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) )  =  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )
8584fveq2d 5695 . . . . . . . . . . . . . . . . . 18  |-  ( q  =  k  ->  ( abs `  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
8685breq1d 4302 . . . . . . . . . . . . . . . . 17  |-  ( q  =  k  ->  (
( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8786ralbidv 2735 . . . . . . . . . . . . . . . 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 2931 . . . . . . . . . . . . . 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 2947 . . . . . . . . . . . 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 5691 . . . . . . . . . . . . 13  |-  ( p  =  j  ->  ( ZZ>=
`  p )  =  ( ZZ>= `  j )
)
9392raleqdv 2923 . . . . . . . . . . . 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 2948 . . . . . . . . . 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 3072 . . . . . . . 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 477 . . . . . . 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 10878 . . . . . . . . . . 11  |-  ( ( p  e.  Z  /\  q  e.  ( ZZ>= `  p ) )  -> 
q  e.  Z )
100 eqid 2443 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  q )  =  (
ZZ>= `  q )
101 eluzelz 10870 . . . . . . . . . . . . . . . 16  |-  ( q  e.  ( ZZ>= `  M
)  ->  q  e.  ZZ )
102101, 3eleq2s 2535 . . . . . . . . . . . . . . 15  |-  ( q  e.  Z  ->  q  e.  ZZ )
103102ad2antlr 726 . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . 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 10878 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Z  /\  m  e.  ( ZZ>= `  q ) )  ->  m  e.  Z )
108106, 107sylan 471 . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . 17  |-  ( n  =  m  ->  ( F `  n )  =  ( F `  m ) )
110109fveq1d 5693 . . . . . . . . . . . . . . . 16  |-  ( n  =  m  ->  (
( F `  n
) `  w )  =  ( ( F `
 m ) `  w ) )
111 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) )
112 fvex 5701 . . . . . . . . . . . . . . . 16  |-  ( ( F `  m ) `
 w )  e. 
_V
113110, 111, 112fvmpt 5774 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . . . . . . 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 7234 . . . . . . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . . . . 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 802 . . . . . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  y ) )
122120, 121fmptd 5867 . . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  y ) )
125 fveq2 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  j
) `  z )  =  ( ( F `
 j ) `  y ) )
126124, 125oveq12d 6109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) )  =  ( ( ( F `  k ) `
 y )  -  ( ( F `  j ) `  y
) ) )
127126fveq2d 5695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) ) )
128127breq1d 4302 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  y  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
129128rspcv 3069 . . . . . . . . . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( q  =  k  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  q
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  k )
)
136135oveq1d 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5695 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2947 . . . . . . . . . . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  =  j  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  j )
)
141140oveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5695 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2931 . . . . . . . . . . . . . . . . . . . . . . . . 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 2948 . . . . . . . . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
148147fveq1d 5693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  (
( F `  n
) `  y )  =  ( ( F `
 k ) `  y ) )
149 fvex 5701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  k ) `
 y )  e. 
_V
150148, 121, 149fvmpt 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  j  ->  ( F `  n )  =  ( F `  j ) )
153152fveq1d 5693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  j  ->  (
( F `  n
) `  y )  =  ( ( F `
 j ) `  y ) )
154 fvex 5701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  j ) `
 y )  e. 
_V
155153, 121, 154fvmpt 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
)  =  ( ( F `  j ) `
 y ) )
156155adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j )  =  ( ( F `  j
) `  y )
)
157151, 156oveq12d 6109 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5695 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . . . . . . . . . . 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 2731 . . . . . . . . . . . . . . . . . . . . . . . 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 2748 . . . . . . . . . . . . . . . . . . . . . . 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 4296 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( r  =  x  ->  (
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  r  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
164163ralbidv 2735 . . . . . . . . . . . . . . . . . . . . . . 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 2736 . . . . . . . . . . . . . . . . . . . . . 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 2947 . . . . . . . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ZZ>= `  M )  e.  _V
1703, 169eqeltri 2513 . . . . . . . . . . . . . . . . . . . . 21  |-  Z  e. 
_V
171170mptex 5948 . . . . . . . . . . . . . . . . . . . 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 13156 . . . . . . . . . . . . . . . . . 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 2799 . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  w  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  w ) )
177176mpteq2dv 4379 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  w  ->  (
n  e.  Z  |->  ( ( F `  n
) `  y )
)  =  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) )
178177eleq1d 2509 . . . . . . . . . . . . . . . . 17  |-  ( y  =  w  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  <->  (
n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  ) )
179178rspccva 3072 . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . 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 13032 . . . . . . . . . . . . . . 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 12989 . . . . . . . . . . . . 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 12838 . . . . . . . . . . . . . . 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 12839 . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . . 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 7234 . . . . . . . . . . . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . 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 12977 . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . 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 5844 . . . . . . . . . . . . . . . . . 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 7234 . . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . 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 5844 . . . . . . . . . . . . . . . 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 10997 . . . . . . . . . . . . . . . . 17  |-  ( r  e.  RR+  ->  r  e.  RR )
203202ad4antlr 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
)  /\  m  e.  ( ZZ>= `  q )
)  ->  r  e.  RR )
204 abs3lem 12826 . . . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . . . 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 2841 . . . . . . . . . . . . . 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 674 . . . . . . . . . . . 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 2794 . . . . . . . . . . 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 474 . . . . . . . . . 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 648 . . . . . . . . 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 2794 . . . . . . . 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 2828 . . . . . . 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 2799 . . . . 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 465 . . . . . 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 2444 . . . . . 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 5695 . . . . . . . 8  |-  ( y  =  w  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) )  =  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) )
219 eqid 2443 . . . . . . . 8  |-  ( y  e.  S  |->  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  y )
) ) )  =  ( y  e.  S  |->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) )
220 fvex 5701 . . . . . . . 8  |-  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) )  e.  _V
221218, 219, 220fvmpt 5774 . . . . . . 7  |-  ( w  e.  S  ->  (
( y  e.  S  |->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) ) ) ) `  w
)  =  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) ) )
222221adantl 466 . . . . . 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 13032 . . . . . . . . 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 12977 . . . . . . . 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.