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

Theorem ulmcau 19788
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 19789 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 4890 . . . 4  |-  ( F  e.  dom  ( ~~> u `  S )  ->  ( F  e.  dom  ( ~~> u `  S )  <->  E. g  F ( ~~> u `  S ) g ) )
21ibi 232 . . 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 706 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  M  e.  ZZ )
6 ulmcau.f . . . . . . . . 9  |-  ( ph  ->  F : Z --> ( CC 
^m  S ) )
76ad2antrr 706 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F : Z --> ( CC 
^m  S ) )
8 eqidd 2297 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( k  e.  Z  /\  z  e.  S ) )  -> 
( ( F `  k ) `  z
)  =  ( ( F `  k ) `
 z ) )
9 eqidd 2297 . . . . . . . 8  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  z  e.  S
)  ->  ( g `  z )  =  ( g `  z ) )
10 simplr 731 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  F ( ~~> u `  S ) g )
11 rphalfcl 10394 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR+ )
1211adantl 452 . . . . . . . 8  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  -> 
( x  /  2
)  e.  RR+ )
133, 5, 7, 8, 9, 10, 12ulmi 19781 . . . . . . 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 447 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  Z )
1514, 3syl6eleq 2386 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  ( ZZ>= `  M )
)
16 eluzelz 10254 . . . . . . . . . . 11  |-  ( j  e.  ( ZZ>= `  M
)  ->  j  e.  ZZ )
17 uzid 10258 . . . . . . . . . . 11  |-  ( j  e.  ZZ  ->  j  e.  ( ZZ>= `  j )
)
1815, 16, 173syl 18 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  j  e.  ( ZZ>= `  j )
)
19 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  ( F `  k )  =  ( F `  j ) )
2019fveq1d 5543 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  (
( F `  k
) `  z )  =  ( ( F `
 j ) `  z ) )
2120oveq1d 5889 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  (
( ( F `  k ) `  z
)  -  ( g `
 z ) )  =  ( ( ( F `  j ) `
 z )  -  ( g `  z
) ) )
2221fveq2d 5545 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( g `  z
) ) )  =  ( abs `  (
( ( F `  j ) `  z
)  -  ( g `
 z ) ) ) )
2322breq1d 4049 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( g `
 z ) ) )  <  ( x  /  2 )  <->  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) ) )
2423ralbidv 2576 . . . . . . . . . . 11  |-  ( k  =  j  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 )  <->  A. z  e.  S  ( abs `  ( ( ( F `
 j ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 ) ) )
2524rspcv 2893 . . . . . . . . . 10  |-  ( j  e.  ( ZZ>= `  j
)  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. z  e.  S  ( abs `  ( ( ( F `  j
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) ) )
2618, 25syl 15 . . . . . . . . 9  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
g `  z )
) )  <  (
x  /  2 )  ->  A. z  e.  S  ( abs `  ( ( ( F `  j
) `  z )  -  ( g `  z ) ) )  <  ( x  / 
2 ) ) )
27 r19.26 2688 . . . . . . . . . . . . . . 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 ) ) )
28 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : Z --> ( CC 
^m  S )  /\  j  e.  Z )  ->  ( F `  j
)  e.  ( CC 
^m  S ) )
297, 28sylan 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
3029adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  j )  e.  ( CC  ^m  S ) )
31 elmapi 6808 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  j )  e.  ( CC  ^m  S )  ->  ( F `  j ) : S --> CC )
3230, 31syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  j ) : S --> CC )
33 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F `  j
) : S --> CC  /\  z  e.  S )  ->  ( ( F `  j ) `  z
)  e.  CC )
3432, 33sylan 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( F `  j
) `  z )  e.  CC )
35 ulmcl 19776 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F ( ~~> u `  S
) g  ->  g : S --> CC )
3635ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  -> 
g : S --> CC )
3736ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  g : S
--> CC )
38 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g : S --> CC  /\  z  e.  S )  ->  ( g `  z
)  e.  CC )
3937, 38sylan 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
g `  z )  e.  CC )
4034, 39abssubd 11951 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
4140breq1d 4049 . . . . . . . . . . . . . . . . . . 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 ) ) )
4241biimpd 198 . . . . . . . . . . . . . . . . . 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 ) ) )
433uztrn2 10261 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
k  e.  Z )
44 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : Z --> ( CC 
^m  S )  /\  k  e.  Z )  ->  ( F `  k
)  e.  ( CC 
^m  S ) )
457, 43, 44syl2an 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  ( j  e.  Z  /\  k  e.  ( ZZ>= `  j )
) )  ->  ( F `  k )  e.  ( CC  ^m  S
) )
4645anassrs 629 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  k )  e.  ( CC  ^m  S ) )
47 elmapi 6808 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  k )  e.  ( CC  ^m  S )  ->  ( F `  k ) : S --> CC )
4846, 47syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  F ( ~~> u `  S ) g )  /\  x  e.  RR+ )  /\  j  e.  Z
)  /\  k  e.  ( ZZ>= `  j )
)  ->  ( F `  k ) : S --> CC )
49 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  k
) : S --> CC  /\  z  e.  S )  ->  ( ( F `  k ) `  z
)  e.  CC )
5048, 49sylan 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  (
( F `  k
) `  z )  e.  CC )
51 rpre 10376 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  RR+  ->  x  e.  RR )
5251adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  F
( ~~> u `  S
) g )  /\  x  e.  RR+ )  ->  x  e.  RR )
5352ad3antrrr 710 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  F ( ~~> u `  S )
g )  /\  x  e.  RR+ )  /\  j  e.  Z )  /\  k  e.  ( ZZ>= `  j )
)  /\  z  e.  S )  ->  x  e.  RR )
54 abs3lem 11838 . . . . . . . . . . . . . . . . . . 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 ) )
5550, 34, 39, 53, 54syl22anc 1183 . . . . . . . . . . . . . . . . . 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 ) )
5642, 55sylan2d 468 . . . . . . . . . . . . . . . . 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 ) )
5756ancomsd 440 . . . . . . . . . . . . . . . 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 ) )
5857ralimdva 2634 . . . . . . . . . . . . . . 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 ) )
5927, 58syl5bir 209 . . . . . . . . . . . . . 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
) )
6059expdimp 426 . . . . . . . . . . . . 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
) )
6160an32s 779 . . . . . . . . . . . 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
) )
6261ralimdva 2634 . . . . . . . . . . 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 ) )
6362ex 423 . . . . . . . . . 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 ) ) )
6463com23 72 . . . . . . . . 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 ) ) )
6526, 64mpdd 36 . . . . . . . 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 ) )
6665reximdva 2668 . . . . . . 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 ) )
6713, 66mpd 14 . . . . . 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 )
6867ralrimiva 2639 . . . . 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 )
6968ex 423 . . . 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 ) )
7069exlimdv 1626 . . 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 ) )
712, 70syl5 28 . 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
) )
72 ulmrel 19773 . . . 4  |-  Rel  ( ~~> u `  S )
73 ulmcau.s . . . . . . . . . 10  |-  ( ph  ->  S  e.  V )
743, 4, 73, 6ulmcaulem 19787 . . . . . . . . 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 ) )
7574biimpa 470 . . . . . . . 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 )
76 rphalfcl 10394 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
77 breq2 4043 . . . . . . . . . . . . 13  |-  ( x  =  ( r  / 
2 )  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
7877ralbidv 2576 . . . . . . . . . . . 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 ) ) )
79782ralbidv 2598 . . . . . . . . . . 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 ) ) )
8079rexbidv 2577 . . . . . . . . . 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 ) ) )
81 ralcom 2713 . . . . . . . . . . . . . 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
) )
82 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( q  =  k  ->  ( ZZ>=
`  q )  =  ( ZZ>= `  k )
)
83 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  q
) `  w )  =  ( ( F `
 q ) `  z ) )
84 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  z  ->  (
( F `  m
) `  w )  =  ( ( F `
 m ) `  z ) )
8583, 84oveq12d 5892 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  z  ->  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) )  =  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )
8685fveq2d 5545 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  z  ->  ( abs `  ( ( ( F `  q ) `
 w )  -  ( ( F `  m ) `  w
) ) )  =  ( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
8786breq1d 4049 . . . . . . . . . . . . . . . . 17  |-  ( w  =  z  ->  (
( abs `  (
( ( F `  q ) `  w
)  -  ( ( F `  m ) `
 w ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 q ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
8887cbvralv 2777 . . . . . . . . . . . . . . . 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 ) )
89 fveq2 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  =  k  ->  ( F `  q )  =  ( F `  k ) )
9089fveq1d 5543 . . . . . . . . . . . . . . . . . . . 20  |-  ( q  =  k  ->  (
( F `  q
) `  z )  =  ( ( F `
 k ) `  z ) )
9190oveq1d 5889 . . . . . . . . . . . . . . . . . . 19  |-  ( q  =  k  ->  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) )  =  ( ( ( F `  k ) `
 z )  -  ( ( F `  m ) `  z
) ) )
9291fveq2d 5545 . . . . . . . . . . . . . . . . . 18  |-  ( q  =  k  ->  ( abs `  ( ( ( F `  q ) `
 z )  -  ( ( F `  m ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  m ) `
 z ) ) ) )
9392breq1d 4049 . . . . . . . . . . . . . . . . 17  |-  ( q  =  k  ->  (
( abs `  (
( ( F `  q ) `  z
)  -  ( ( F `  m ) `
 z ) ) )  <  ( r  /  2 )  <->  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  m
) `  z )
) )  <  (
r  /  2 ) ) )
9493ralbidv 2576 . . . . . . . . . . . . . . . 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 ) ) )
9588, 94syl5bb 248 . . . . . . . . . . . . . . 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 ) ) )
9682, 95raleqbidv 2761 . . . . . . . . . . . . . 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
) ) )
9781, 96syl5bb 248 . . . . . . . . . . . . 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 ) ) )
9897cbvralv 2777 . . . . . . . . . . . 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
) )
99 fveq2 5541 . . . . . . . . . . . . 13  |-  ( p  =  j  ->  ( ZZ>=
`  p )  =  ( ZZ>= `  j )
)
10099raleqdv 2755 . . . . . . . . . . . 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 ) ) )
10198, 100syl5bb 248 . . . . . . . . . . 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 ) ) )
102101cbvrexv 2778 . . . . . . . . . 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
) )
10380, 102syl6bbr 254 . . . . . . . . 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 ) ) )
104103rspccva 2896 . . . . . . . 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 ) )
10575, 76, 104syl2an 463 . . . . . . 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 ) )
1063uztrn2 10261 . . . . . . . . . . 11  |-  ( ( p  e.  Z  /\  q  e.  ( ZZ>= `  p ) )  -> 
q  e.  Z )
107 eqid 2296 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  q )  =  (
ZZ>= `  q )
108 eluzelz 10254 . . . . . . . . . . . . . . . 16  |-  ( q  e.  ( ZZ>= `  M
)  ->  q  e.  ZZ )
109108, 3eleq2s 2388 . . . . . . . . . . . . . . 15  |-  ( q  e.  Z  ->  q  e.  ZZ )
110109ad2antlr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) A. z  e.  S  ( abs `  ( ( ( F `
 k ) `  z )  -  (
( F `  j
) `  z )
) )  <  x
)  /\  r  e.  RR+ )  /\  q  e.  Z )  /\  w  e.  S )  ->  q  e.  ZZ )
11176adantl 452 . . . . . . . . . . . . . . 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+ )
112111ad2antrr 706 . . . . . . . . . . . . . 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+ )
113 simplr 731 . . . . . . . . . . . . . . . 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 )
1143uztrn2 10261 . . . . . . . . . . . . . . . 16  |-  ( ( q  e.  Z  /\  m  e.  ( ZZ>= `  q ) )  ->  m  e.  Z )
115113, 114sylan 457 . . . . . . . . . . . . . . 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 )
116 fveq2 5541 . . . . . . . . . . . . . . . . 17  |-  ( n  =  m  ->  ( F `  n )  =  ( F `  m ) )
117116fveq1d 5543 . . . . . . . . . . . . . . . 16  |-  ( n  =  m  ->  (
( F `  n
) `  w )  =  ( ( F `
 m ) `  w ) )
118 eqid 2296 . . . . . . . . . . . . . . . 16  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) )
119 fvex 5555 . . . . . . . . . . . . . . . 16  |-  ( ( F `  m ) `
 w )  e. 
_V
120117, 118, 119fvmpt 5618 . . . . . . . . . . . . . . 15  |-  ( m  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  w
) ) `  m
)  =  ( ( F `  m ) `
 w ) )
121115, 120syl 15 . . . . . . . . . . . . . 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 ) )
1226adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
123 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : Z --> ( CC 
^m  S )  /\  n  e.  Z )  ->  ( F `  n
)  e.  ( CC 
^m  S ) )
124122, 123sylan 457 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
125 elmapi 6808 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  n )  e.  ( CC  ^m  S )  ->  ( F `  n ) : S --> CC )
126124, 125syl 15 . . . . . . . . . . . . . . . . . . . . . . 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 )
127 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( F `  n
) : S --> CC  /\  y  e.  S )  ->  ( ( F `  n ) `  y
)  e.  CC )
128126, 127sylan 457 . . . . . . . . . . . . . . . . . . . . . 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 )
129128an32s 779 . . . . . . . . . . . . . . . . . . . . 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 )
130 eqid 2296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  =  ( n  e.  Z  |->  ( ( F `
 n ) `  y ) )
131129, 130fmptd 5700 . . . . . . . . . . . . . . . . . . . 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 )
132 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( n  e.  Z  |->  ( ( F `  n ) `  y
) ) : Z --> CC  /\  q  e.  Z
)  ->  ( (
n  e.  Z  |->  ( ( F `  n
) `  y )
) `  q )  e.  CC )
133131, 132sylan 457 . . . . . . . . . . . . . . . . . . 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 )
134 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  y ) )
135 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  y  ->  (
( F `  j
) `  z )  =  ( ( F `
 j ) `  y ) )
136134, 135oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  y  ->  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) )  =  ( ( ( F `  k ) `
 y )  -  ( ( F `  j ) `  y
) ) )
137136fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  y  ->  ( abs `  ( ( ( F `  k ) `
 z )  -  ( ( F `  j ) `  z
) ) )  =  ( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) ) )
138137breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  y  ->  (
( abs `  (
( ( F `  k ) `  z
)  -  ( ( F `  j ) `
 z ) ) )  <  x  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
139138rspcv 2893 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  S  ->  ( A. z  e.  S  ( abs `  ( ( ( F `  k
) `  z )  -  ( ( F `
 j ) `  z ) ) )  <  x  ->  ( abs `  ( ( ( F `  k ) `
 y )  -  ( ( F `  j ) `  y
) ) )  < 
x ) )
140139ralimdv 2635 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
141140reximdv 2667 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
142141ralimdv 2635 . . . . . . . . . . . . . . . . . . . . . 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 ) )
143142impcom 419 . . . . . . . . . . . . . . . . . . . . 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 )
144143adantll 694 . . . . . . . . . . . . . . . . . . . 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
)
145 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( q  =  k  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  q
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  k )
)
146145oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
147146fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
148147breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
149148cbvralv 2777 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
150 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  =  j  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  p
)  =  ( ( n  e.  Z  |->  ( ( F `  n
) `  y )
) `  j )
)
151150oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
152151fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
153152breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
15499, 153raleqbidv 2761 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
155149, 154syl5bb 248 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
156155cbvrexv 2778 . . . . . . . . . . . . . . . . . . . . . . 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 )
157 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
158157fveq1d 5543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  (
( F `  n
) `  y )  =  ( ( F `
 k ) `  y ) )
159 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  k ) `
 y )  e. 
_V
160158, 130, 159fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  k
)  =  ( ( F `  k ) `
 y ) )
16143, 160syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  k )  =  ( ( F `  k
) `  y )
)
162 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  j  ->  ( F `  n )  =  ( F `  j ) )
163162fveq1d 5543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  j  ->  (
( F `  n
) `  y )  =  ( ( F `
 j ) `  y ) )
164 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F `  j ) `
 y )  e. 
_V
165163, 130, 164fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  Z  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) ) `  j
)  =  ( ( F `  j ) `
 y ) )
166165adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  Z  /\  k  e.  ( ZZ>= `  j ) )  -> 
( ( n  e.  Z  |->  ( ( F `
 n ) `  y ) ) `  j )  =  ( ( F `  j
) `  y )
)
167161, 166oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
168167fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
169168breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
170169ralbidva 2572 . . . . . . . . . . . . . . . . . . . . . . . 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
) )
171170rexbiia 2589 . . . . . . . . . . . . . . . . . . . . . . 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 )
172156, 171bitri 240 . . . . . . . . . . . . . . . . . . . . . 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 )
173 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( r  =  x  ->  (
( abs `  (
( ( F `  k ) `  y
)  -  ( ( F `  j ) `
 y ) ) )  <  r  <->  ( abs `  ( ( ( F `
 k ) `  y )  -  (
( F `  j
) `  y )
) )  <  x
) )
174173ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
175174rexbidv 2577 . . . . . . . . . . . . . . . . . . . . . 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 ) )
176172, 175syl5bb 248 . . . . . . . . . . . . . . . . . . . . 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
) )
177176cbvralv 2777 . . . . . . . . . . . . . . . . . . . 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
)
178144, 177sylibr 203 . . . . . . . . . . . . . . . . . . 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 )
179 fvex 5555 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ZZ>= `  M )  e.  _V
1803, 179eqeltri 2366 . . . . . . . . . . . . . . . . . . . . 21  |-  Z  e. 
_V
181180mptex 5762 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  Z  |->  ( ( F `  n ) `
 y ) )  e.  _V
182181a1i 10 . . . . . . . . . . . . . . . . . . 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 )
1833, 133, 178, 182caucvg 12167 . . . . . . . . . . . . . . . . . 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  ~~>  )
184183ralrimiva 2639 . . . . . . . . . . . . . . . . 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  ~~>  )
185184ad2antrr 706 . . . . . . . . . . . . . . . 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  ~~>  )
186 fveq2 5541 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  w  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  w ) )
187186mpteq2dv 4123 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  w  ->  (
n  e.  Z  |->  ( ( F `  n
) `  y )
)  =  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) )
188187eleq1d 2362 . . . . . . . . . . . . . . . . 17  |-  ( y  =  w  ->  (
( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  <->  (
n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  ) )
189188rspccva 2896 . . . . . . . . . . . . . . . 16  |-  ( ( A. y  e.  S  ( n  e.  Z  |->  ( ( F `  n ) `  y
) )  e.  dom  ~~>  /\  w  e.  S )  ->  ( n  e.  Z  |->  ( ( F `
 n ) `  w ) )  e. 
dom 
~~>  )
190185, 189sylan 457 . . . . . . . . . . . . . . 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  ~~>  )
191 climdm 12044 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  w )
)  e.  dom  ~~>  <->  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) )  ~~>  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `
 w ) ) ) )
192190, 191sylib 188 . . . . . . . . . . . . . 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 )
) ) )
193107, 110, 112, 121, 192climi2 12001 . . . . . . . . . . . . 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
) )
194107r19.29uz 11850 . . . . . . . . . . . . . . 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 ) ) )
195107r19.2uz 11851 . . . . . . . . . . . . . . 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
) ) )
196194, 195syl 15 . . . . . . . . . . . . . 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
) ) )
1976ad2antrr 706 . . . . . . . . . . . . . . . . . . . 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 ) )
198 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : Z --> ( CC 
^m  S )  /\  q  e.  Z )  ->  ( F `  q
)  e.  ( CC 
^m  S ) )
199197, 198sylan 457 . . . . . . . . . . . . . . . . . . 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 ) )
200 elmapi 6808 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  q )  e.  ( CC  ^m  S )  ->  ( F `  q ) : S --> CC )
201199, 200syl 15 . . . . . . . . . . . . . . . . . 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 )
202 ffvelrn 5679 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  q
) : S --> CC  /\  w  e.  S )  ->  ( ( F `  q ) `  w
)  e.  CC )
203201, 202sylan 457 . . . . . . . . . . . . . . . . 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 )
204203adantr 451 . . . . . . . . . . . . . . . 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 )
205 climcl 11989 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  |->  ( ( F `  n
) `  w )
)  ~~>  (  ~~>  `  (
n  e.  Z  |->  ( ( F `  n
) `  w )
) )  ->  (  ~~>  `  ( n  e.  Z  |->  ( ( F `  n ) `  w
) ) )  e.  CC )
206192, 205syl 15 . . . . . . . . . . . . . . . . 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 )
207206adantr 451 . . . . . . . . . . . . . . . 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 )
208197ad3antrrr 710 . . . . . . . . . . . . . . . . . . 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
) )
209 ffvelrn 5679 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : Z --> ( CC 
^m  S )  /\  m  e.  Z )  ->  ( F `  m
)  e.  ( CC 
^m  S ) )
210208, 115, 209syl2anc 642 . . . . . . . . . . . . . . . . . 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 ) )
211 elmapi 6808 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  m )  e.  ( CC  ^m  S )  ->  ( F `  m ) : S --> CC )
212210, 211syl 15 . . . . . . . . . . . . . . . . 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 )
213 simplr 731 . . . . . . . . . . . . . . . . 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 )
214 ffvelrn 5679 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  m
) : S --> CC  /\  w  e.  S )  ->  ( ( F `  m ) `  w
)  e.  CC )
215212, 213, 214syl2anc 642 . . . . . . . . . . . . . . . 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 )
216 rpre 10376 . . . . . . . . . . . . . . . . . 18  |-  ( r  e.  RR+  ->  r  e.  RR )
217216adantl 452 . . . . . . . . . . . . . . . . 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+ )  -> 
r  e.  RR )
218217ad3antrrr 710 . . . . . . . . . . . . . . . 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 )
219 abs3lem 11838 . . . . . . . . . . . . . . . 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 ) )
220204, 207, 215, 218, 219syl22anc 1183 . . . . . . . . . . . . . . 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
) )
221220rexlimdva 2680 . . . . . . . . . . . . . 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
) )
222196, 221syl5 28 . . . . . . . . . . . . 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 ) )
223193, 222mpan2d 655 . . . . . . . . . . . 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
) )
224223ralimdva 2634 . . . . . . . . . . 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 ) )
225106, 224sylan2 460 . . . . . . . . . 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 ) )
226225anassrs 629 . . . . . . . . 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 ) )
227226ralimdva 2634 . . . . . . . 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 ) )
228227reximdva 2668 . . . . . . 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 ) )
229105, 228mpd 14 . . . . . 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
)
230229ralrimiva 2639 . . . . 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 )
2314adantr 451 . . . . . 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 )
232 eqidd 2297 . . . . . 6  |-  ( ( ( ph  /\  A. x  e.