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

Theorem ulmdvlem3 19779
Description: Lemma for ulmdv 19780. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
ulmdv.z  |-  Z  =  ( ZZ>= `  M )
ulmdv.s  |-  ( ph  ->  S  e.  { RR ,  CC } )
ulmdv.m  |-  ( ph  ->  M  e.  ZZ )
ulmdv.f  |-  ( ph  ->  F : Z --> ( CC 
^m  X ) )
ulmdv.g  |-  ( ph  ->  G : X --> CC )
ulmdv.l  |-  ( (
ph  /\  z  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  ~~>  ( G `  z ) )
ulmdv.u  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) ( ~~> u `  X ) H )
Assertion
Ref Expression
ulmdvlem3  |-  ( (
ph  /\  z  e.  X )  ->  z
( S  _D  G
) ( H `  z ) )
Distinct variable groups:    z, k, F    z, G    z, H    k, M    ph, k, z    S, k, z    k, X, z   
k, Z, z
Allowed substitution hints:    G( k)    H( k)    M( z)

Proof of Theorem ulmdvlem3
Dummy variables  j  m  n  s  u  v  w  x  y 
r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ulmdv.m . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
2 uzid 10242 . . . . . 6  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
31, 2syl 15 . . . . 5  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
4 ulmdv.z . . . . 5  |-  Z  =  ( ZZ>= `  M )
53, 4syl6eleqr 2374 . . . 4  |-  ( ph  ->  M  e.  Z )
6 ulmdv.s . . . . . . 7  |-  ( ph  ->  S  e.  { RR ,  CC } )
7 ulmdv.f . . . . . . 7  |-  ( ph  ->  F : Z --> ( CC 
^m  X ) )
8 ulmdv.g . . . . . . 7  |-  ( ph  ->  G : X --> CC )
9 ulmdv.l . . . . . . 7  |-  ( (
ph  /\  z  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  ~~>  ( G `  z ) )
10 ulmdv.u . . . . . . 7  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) ( ~~> u `  X ) H )
114, 6, 1, 7, 8, 9, 10ulmdvlem2 19778 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  =  X )
12 recnprss 19254 . . . . . . . . 9  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
136, 12syl 15 . . . . . . . 8  |-  ( ph  ->  S  C_  CC )
1413adantr 451 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  S  C_  CC )
15 ffvelrn 5663 . . . . . . . . 9  |-  ( ( F : Z --> ( CC 
^m  X )  /\  k  e.  Z )  ->  ( F `  k
)  e.  ( CC 
^m  X ) )
167, 15sylan 457 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  ( CC  ^m  X
) )
17 elmapi 6792 . . . . . . . 8  |-  ( ( F `  k )  e.  ( CC  ^m  X )  ->  ( F `  k ) : X --> CC )
1816, 17syl 15 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k ) : X --> CC )
19 dvbsss 19252 . . . . . . . . 9  |-  dom  ( S  _D  ( F `  k ) )  C_  S
2019a1i 10 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  C_  S )
2111, 20eqsstr3d 3213 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  S )
22 eqid 2283 . . . . . . 7  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
23 eqid 2283 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
2414, 18, 21, 22, 23dvbssntr 19250 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2511, 24eqsstr3d 3213 . . . . 5  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
2625ralrimiva 2626 . . . 4  |-  ( ph  ->  A. k  e.  Z  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X ) )
27 biidd 228 . . . . 5  |-  ( k  =  M  ->  ( X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X )  <->  X  C_  (
( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
2827rspcv 2880 . . . 4  |-  ( M  e.  Z  ->  ( A. k  e.  Z  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X )  ->  X  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
295, 26, 28sylc 56 . . 3  |-  ( ph  ->  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
3029sselda 3180 . 2  |-  ( (
ph  /\  z  e.  X )  ->  z  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
31 ulmcl 19760 . . . . 5  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  H : X --> CC )
3210, 31syl 15 . . . 4  |-  ( ph  ->  H : X --> CC )
33 ffvelrn 5663 . . . 4  |-  ( ( H : X --> CC  /\  z  e.  X )  ->  ( H `  z
)  e.  CC )
3432, 33sylan 457 . . 3  |-  ( (
ph  /\  z  e.  X )  ->  ( H `  z )  e.  CC )
35 rphalfcl 10378 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
3635adantl 452 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
r  /  2 )  e.  RR+ )
37 rphalfcl 10378 . . . . . . 7  |-  ( ( r  /  2 )  e.  RR+  ->  ( ( r  /  2 )  /  2 )  e.  RR+ )
3836, 37syl 15 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
( r  /  2
)  /  2 )  e.  RR+ )
39 ulmrel 19757 . . . . . . . . . 10  |-  Rel  ( ~~> u `  X )
40 releldm 4911 . . . . . . . . . 10  |-  ( ( Rel  ( ~~> u `  X )  /\  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H )  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  e.  dom  (
~~> u `  X ) )
4139, 10, 40sylancr 644 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  e.  dom  (
~~> u `  X ) )
42 ulmscl 19758 . . . . . . . . . . 11  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  X  e.  _V )
4310, 42syl 15 . . . . . . . . . 10  |-  ( ph  ->  X  e.  _V )
44 ovex 5883 . . . . . . . . . . . . 13  |-  ( S  _D  ( F `  k ) )  e. 
_V
4544rgenw 2610 . . . . . . . . . . . 12  |-  A. k  e.  Z  ( S  _D  ( F `  k
) )  e.  _V
46 eqid 2283 . . . . . . . . . . . . 13  |-  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  =  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )
4746fnmpt 5370 . . . . . . . . . . . 12  |-  ( A. k  e.  Z  ( S  _D  ( F `  k ) )  e. 
_V  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  Fn  Z
)
4845, 47mp1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  Fn  Z
)
49 ulmf2 19763 . . . . . . . . . . 11  |-  ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  Fn  Z  /\  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) ( ~~> u `  X ) H )  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) : Z --> ( CC  ^m  X ) )
5048, 10, 49syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
514, 1, 43, 50ulmcau2 19773 . . . . . . . . 9  |-  ( ph  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  e.  dom  (
~~> u `  X )  <->  A. s  e.  RR+  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
) `  x )  -  ( ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  m ) `
 x ) ) )  <  s ) )
5241, 51mpbid 201 . . . . . . . 8  |-  ( ph  ->  A. s  e.  RR+  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  n
) `  x )  -  ( ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  m ) `
 x ) ) )  <  s )
534uztrn2 10245 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  Z  /\  n  e.  ( ZZ>= `  j ) )  ->  n  e.  Z )
5453ad2ant2lr 728 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  n  e.  Z )
55 fveq2 5525 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
5655oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  n )
) )
57 ovex 5883 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  n ) )  e. 
_V
5856, 46, 57fvmpt 5602 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
)  =  ( S  _D  ( F `  n ) ) )
5954, 58syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
)  =  ( S  _D  ( F `  n ) ) )
6059fveq1d 5527 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  (
( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  n
) `  x )  =  ( ( S  _D  ( F `  n ) ) `  x ) )
61 simprr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  ( ZZ>= `  n )
)
624uztrn2 10245 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  /\  m  e.  ( ZZ>= `  n ) )  ->  m  e.  Z )
6354, 61, 62syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  Z )
64 fveq2 5525 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  m  ->  ( F `  k )  =  ( F `  m ) )
6564oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  m  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  m )
) )
66 ovex 5883 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  m ) )  e. 
_V
6765, 46, 66fvmpt 5602 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  m
)  =  ( S  _D  ( F `  m ) ) )
6863, 67syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  m
)  =  ( S  _D  ( F `  m ) ) )
6968fveq1d 5527 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  (
( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  m
) `  x )  =  ( ( S  _D  ( F `  m ) ) `  x ) )
7060, 69oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  (
( ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 n ) `  x )  -  (
( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  m
) `  x )
)  =  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )
7170fveq2d 5529 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  ( abs `  ( ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
) `  x )  -  ( ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  m ) `
 x ) ) )  =  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) ) )
7271breq1d 4033 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  (
( abs `  (
( ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 n ) `  x )  -  (
( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  m
) `  x )
) )  <  s  <->  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s ) )
7372ralbidv 2563 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  ( A. x  e.  X  ( abs `  ( ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  n
) `  x )  -  ( ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  m ) `
 x ) ) )  <  s  <->  A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  s
) )
74732ralbidva 2583 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  Z )  ->  ( A. n  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n ) `
 x )  -  ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 m ) `  x ) ) )  <  s  <->  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s
) )
7574rexbidva 2560 . . . . . . . . 9  |-  ( ph  ->  ( E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
) `  x )  -  ( ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  m ) `
 x ) ) )  <  s  <->  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s
) )
7675ralbidv 2563 . . . . . . . 8  |-  ( ph  ->  ( A. s  e.  RR+  E. j  e.  Z  A. n  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n ) `
 x )  -  ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 m ) `  x ) ) )  <  s  <->  A. s  e.  RR+  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s
) )
7752, 76mpbid 201 . . . . . . 7  |-  ( ph  ->  A. s  e.  RR+  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s )
7877ad2antrr 706 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  A. s  e.  RR+  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s
)
79 breq2 4027 . . . . . . . . 9  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  (
( abs `  (
( ( S  _D  ( F `  n ) ) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s  <->  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 ) ) )
80792ralbidv 2585 . . . . . . . 8  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  ( A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s  <->  A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 ) ) )
8180rexralbidv 2587 . . . . . . 7  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  ( E. j  e.  Z  A. n  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  s  <->  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 ) ) )
8281rspcv 2880 . . . . . 6  |-  ( ( ( r  /  2
)  /  2 )  e.  RR+  ->  ( A. s  e.  RR+  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  s  ->  E. j  e.  Z  A. n  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 ) ) )
8338, 78, 82sylc 56 . . . . 5  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( r  /  2
)  /  2 ) )
841ad2antrr 706 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  M  e.  ZZ )
8556fveq1d 5527 . . . . . . . 8  |-  ( k  =  n  ->  (
( S  _D  ( F `  k )
) `  z )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
86 eqid 2283 . . . . . . . 8  |-  ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) )  =  ( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) )
87 fvex 5539 . . . . . . . 8  |-  ( ( S  _D  ( F `
 n ) ) `
 z )  e. 
_V
8885, 86, 87fvmpt 5602 . . . . . . 7  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) ) `  n )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
8988adantl 452 . . . . . 6  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
) `  n )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
9050ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) : Z --> ( CC 
^m  X ) )
91 simplr 731 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  z  e.  X )
92 fvex 5539 . . . . . . . . . 10  |-  ( ZZ>= `  M )  e.  _V
934, 92eqeltri 2353 . . . . . . . . 9  |-  Z  e. 
_V
9493mptex 5746 . . . . . . . 8  |-  ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) )  e.  _V
9594a1i 10 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
)  e.  _V )
9658adantl 452 . . . . . . . . 9  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  =  ( S  _D  ( F `  n ) ) )
9796fveq1d 5527 . . . . . . . 8  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
) `  z )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
9897, 89eqtr4d 2318 . . . . . . 7  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
) `  z )  =  ( ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) ) `
 n ) )
9910ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H )
1004, 84, 90, 91, 95, 98, 99ulmclm 19766 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
)  ~~>  ( H `  z ) )
1014, 84, 36, 89, 100climi2 11985 . . . . 5  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  E. j  e.  Z  A. n  e.  ( ZZ>= `  j )
( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) )
1024rexanuz2 11833 . . . . . . 7  |-  ( E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) )  <->  ( E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) ( abs `  ( ( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z )
) )  <  (
r  /  2 ) ) )
1034r19.2uz 11835 . . . . . . 7  |-  ( E. j  e.  Z  A. n  e.  ( ZZ>= `  j ) ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) )  ->  E. n  e.  Z  ( A. m  e.  (
ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) )
104102, 103sylbir 204 . . . . . 6  |-  ( ( E. j  e.  Z  A. n  e.  ( ZZ>=
`  j ) A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  E. j  e.  Z  A. n  e.  ( ZZ>= `  j )
( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) )  ->  E. n  e.  Z  ( A. m  e.  (
ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) )
10538adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
r  /  2 )  /  2 )  e.  RR+ )
106 simpllr 735 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  X )
107 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  e.  ( CC  ^m  X ) )
10890, 107sylan 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  e.  ( CC  ^m  X ) )
10996, 108eqeltrrd 2358 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) )  e.  ( CC  ^m  X ) )
110 elmapi 6792 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  _D  ( F `
 n ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
111109, 110syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) ) : X --> CC )
112 fdm 5393 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  _D  ( F `
 n ) ) : X --> CC  ->  dom  ( S  _D  ( F `  n )
)  =  X )
113111, 112syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  dom  ( S  _D  ( F `  n ) )  =  X )
114106, 113eleqtrrd 2360 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  dom  ( S  _D  ( F `  n )
) )
1156ad3antrrr 710 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  e.  { RR ,  CC }
)
116 dvfg 19256 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  { RR ,  CC }  ->  ( S  _D  ( F `  n
) ) : dom  ( S  _D  ( F `  n )
) --> CC )
117115, 116syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) ) : dom  ( S  _D  ( F `  n )
) --> CC )
118 ffun 5391 . . . . . . . . . . . . . . . . 17  |-  ( ( S  _D  ( F `
 n ) ) : dom  ( S  _D  ( F `  n ) ) --> CC 
->  Fun  ( S  _D  ( F `  n ) ) )
119 funfvbrb 5638 . . . . . . . . . . . . . . . . 17  |-  ( Fun  ( S  _D  ( F `  n )
)  ->  ( z  e.  dom  ( S  _D  ( F `  n ) )  <->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
) )
120117, 118, 1193syl 18 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( z  e.  dom  ( S  _D  ( F `  n ) )  <->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
) )
121114, 120mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
)
122 eqid 2283 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( X  \  { z } ) 
|->  ( ( ( ( F `  n ) `
 y )  -  ( ( F `  n ) `  z
) )  /  (
y  -  z ) ) )  =  ( y  e.  ( X 
\  { z } )  |->  ( ( ( ( F `  n
) `  y )  -  ( ( F `
 n ) `  z ) )  / 
( y  -  z
) ) )
123115, 12syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  C_  CC )
1247ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  F : Z --> ( CC  ^m  X ) )
125 ffvelrn 5663 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : Z --> ( CC 
^m  X )  /\  n  e.  Z )  ->  ( F `  n
)  e.  ( CC 
^m  X ) )
126124, 125sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n )  e.  ( CC  ^m  X ) )
127 elmapi 6792 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  n )  e.  ( CC  ^m  X )  ->  ( F `  n ) : X --> CC )
128126, 127syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n ) : X --> CC )
12921ralrimiva 2626 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. k  e.  Z  X  C_  S )
130 biidd 228 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  M  ->  ( X  C_  S  <->  X  C_  S
) )
131130rspcv 2880 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  Z  ->  ( A. k  e.  Z  X  C_  S  ->  X  C_  S ) )
1325, 129, 131sylc 56 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  C_  S )
133132ad3antrrr 710 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  S
)
13422, 23, 122, 123, 128, 133eldv 19248 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( z
( S  _D  ( F `  n )
) ( ( S  _D  ( F `  n ) ) `  z )  <->  ( z  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  /\  (
( S  _D  ( F `  n )
) `  z )  e.  ( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) lim CC  z ) ) ) )
135121, 134mpbid 201 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( z  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  /\  (
( S  _D  ( F `  n )
) `  z )  e.  ( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) lim CC  z ) ) )
136135simprd 449 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( ( S  _D  ( F `  n ) ) `  z )  e.  ( ( y  e.  ( X  \  { z } )  |->  ( ( ( ( F `  n ) `  y
)  -  ( ( F `  n ) `
 z ) )  /  ( y  -  z ) ) ) lim
CC  z ) )
137132adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  S )
13813adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  X )  ->  S  C_  CC )
139137, 138sstrd 3189 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  CC )
140139ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  CC )
141128, 140, 106dvlem 19246 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  /\  y  e.  ( X  \  { z } ) )  -> 
( ( ( ( F `  n ) `
 y )  -  ( ( F `  n ) `  z
) )  /  (
y  -  z ) )  e.  CC )
142141, 122fmptd 5684 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) : ( X 
\  { z } ) --> CC )
143 difss 3303 . . . . . . . . . . . . . . 15  |-  ( X 
\  { z } )  C_  X
144143, 140syl5ss 3190 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( X  \  { z } ) 
C_  CC )
145140, 106sseldd 3181 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  CC )
146142, 144, 145ellimc3 19229 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
( S  _D  ( F `  n )
) `  z )  e.  ( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) lim CC  z )  <-> 
( ( ( S  _D  ( F `  n ) ) `  z )  e.  CC  /\ 
A. s  e.  RR+  E. w  e.  RR+  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) `  v )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  s ) ) ) )
147136, 146mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
( S  _D  ( F `  n )
) `  z )  e.  CC  /\  A. s  e.  RR+  E. w  e.  RR+  A. v  e.  ( X  \  { z } ) ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  <  w )  -> 
( abs `  (
( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) `  v )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  s ) ) )
148147simprd 449 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  A. s  e.  RR+  E. w  e.  RR+  A. v  e.  ( X  \  { z } ) ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  <  w )  -> 
( abs `  (
( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) `  v )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  s ) )
149 fveq2 5525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  v  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  v ) )
150149oveq1d 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  v  ->  (
( ( F `  n ) `  y
)  -  ( ( F `  n ) `
 z ) )  =  ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) ) )
151 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  v  ->  (
y  -  z )  =  ( v  -  z ) )
152150, 151oveq12d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) )  =  ( ( ( ( F `  n
) `  v )  -  ( ( F `
 n ) `  z ) )  / 
( v  -  z
) ) )
153 ovex 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  e. 
_V
154152, 122, 153fvmpt 5602 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  ( X  \  { z } )  ->  ( ( y  e.  ( X  \  { z } ) 
|->  ( ( ( ( F `  n ) `
 y )  -  ( ( F `  n ) `  z
) )  /  (
y  -  z ) ) ) `  v
)  =  ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) ) )
155154oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  ( X  \  { z } )  ->  ( ( ( y  e.  ( X 
\  { z } )  |->  ( ( ( ( F `  n
) `  y )  -  ( ( F `
 n ) `  z ) )  / 
( y  -  z
) ) ) `  v )  -  (
( S  _D  ( F `  n )
) `  z )
)  =  ( ( ( ( ( F `
 n ) `  v )  -  (
( F `  n
) `  z )
)  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )
156155fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( v  e.  ( X  \  { z } )  ->  ( abs `  (
( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) `  v )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  =  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) ) )
157 id 19 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  s  =  ( ( r  /  2 )  / 
2 ) )
158156, 157breqan12rd 4039 . . . . . . . . . . . . . . 15  |-  ( ( s  =  ( ( r  /  2 )  /  2 )  /\  v  e.  ( X  \  { z } ) )  ->  ( ( abs `  ( ( ( y  e.  ( X 
\  { z } )  |->  ( ( ( ( F `  n
) `  y )  -  ( ( F `
 n ) `  z ) )  / 
( y  -  z
) ) ) `  v )  -  (
( S  _D  ( F `  n )
) `  z )
) )  <  s  <->  ( abs `  ( ( ( ( ( F `
 n ) `  v )  -  (
( F `  n
) `  z )
)  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  ( ( r  /  2 )  / 
2 ) ) )
159158imbi2d 307 . . . . . . . . . . . . . 14  |-  ( ( s  =  ( ( r  /  2 )  /  2 )  /\  v  e.  ( X  \  { z } ) )  ->  ( (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) `  v )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  s )  <->  ( (
v  =/=  z  /\  ( abs `  ( v  -  z ) )  <  w )  -> 
( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )
160159ralbidva 2559 . . . . . . . . . . . . 13  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  ( A. v  e.  ( X  \  { z } ) ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
w )  ->  ( abs `  ( ( ( y  e.  ( X 
\  { z } )  |->  ( ( ( ( F `  n
) `  y )  -  ( ( F `
 n ) `  z ) )  / 
( y  -  z
) ) ) `  v )  -  (
( S  _D  ( F `  n )
) `  z )
) )  <  s
)  <->  A. v  e.  ( X  \  { z } ) ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  <  w )  -> 
( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )
161160rexbidv 2564 . . . . . . . . . . . 12  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  ( E. w  e.  RR+  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) `  v )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  s )  <->  E. w  e.  RR+  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )
162161rspcv 2880 . . . . . . . . . . 11  |-  ( ( ( r  /  2
)  /  2 )  e.  RR+  ->  ( A. s  e.  RR+  E. w  e.  RR+  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( y  e.  ( X  \  {
z } )  |->  ( ( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) ) ) `  v )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  s )  ->  E. w  e.  RR+  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )
163105, 148, 162sylc 56 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  E. w  e.  RR+  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) )
164163adantrr 697 . . . . . . . . 9  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) ) ) )  ->  E. w  e.  RR+  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) )
165 cnxmet 18282 . . . . . . . . . . . . . . 15  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
166 xmetres2 17925 . . . . . . . . . . . . . . 15  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S ) )
167165, 138, 166sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  X )  ->  (
( abs  o.  -  )  |`  ( S  X.  S
) )  e.  ( * Met `  S
) )
168167ad3antrrr 710 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) ) )  /\  ( w  e.  RR+  /\  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )  ->  (
( abs  o.  -  )  |`  ( S  X.  S
) )  e.  ( * Met `  S
) )
16923cnfldtop 18293 . . . . . . . . . . . . . . . . . . . 20  |-  ( TopOpen ` fld )  e.  Top
170 resttop 16891 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  S  e.  { RR ,  CC } )  -> 
( ( TopOpen ` fld )t  S )  e.  Top )
171169, 6, 170sylancr 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  Top )
17223cnfldtopon 18292 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
173 resttopon 16892 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
174172, 13, 173sylancr 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
175 toponuni 16665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
176174, 175syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  S  =  U. (
( TopOpen ` fld )t  S ) )
177132, 176sseqtrd 3214 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  C_  U. (
( TopOpen ` fld )t  S ) )
178 eqid 2283 . . . . . . . . . . . . . . . . . . . 20  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
179178ntrss2 16794 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( TopOpen ` fld )t  S )  e.  Top  /\  X  C_  U. (
( TopOpen ` fld )t  S ) )  -> 
( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
180171, 177, 179syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
181180, 29eqssd 3196 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  =  X )
182178isopn3 16803 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( TopOpen ` fld )t  S )  e.  Top  /\  X  C_  U. (
( TopOpen ` fld )t  S ) )  -> 
( X  e.  ( ( TopOpen ` fld )t  S )  <->  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
)  =  X ) )
183171, 177, 182syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( X  e.  ( ( TopOpen ` fld )t  S )  <->  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
)  =  X ) )
184181, 183mpbird 223 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
185 eqid 2283 . . . . . . . . . . . . . . . . . 18  |-  ( ( abs  o.  -  )  |`  ( S  X.  S
) )  =  ( ( abs  o.  -  )  |`  ( S  X.  S ) )
18623cnfldtopn 18291 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
187 eqid 2283 . . . . . . . . . . . . . . . . . 18  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )
188185, 186, 187metrest 18070 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
189165, 13, 188sylancr 644 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
190184, 189eleqtrd 2359 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) )
191190adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  X )  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) )
192191ad3antrrr 710 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) ) )  /\  ( w  e.  RR+  /\  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) )
19391ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) ) )  /\  ( w  e.  RR+  /\  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )  ->  z  e.  X )
194 simprl 732 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) ) )  /\  ( w  e.  RR+  /\  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )  ->  w  e.  RR+ )
195187mopni3 18040 . . . . . . . . . . . . 13  |-  ( ( ( ( ( abs 
o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S )  /\  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) )  /\  z  e.  X )  /\  w  e.  RR+ )  ->  E. u  e.  RR+  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )
196168, 192, 193, 194, 195syl31anc 1185 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) ) )  /\  ( w  e.  RR+  /\  A. v  e.  ( X  \  {
z } ) ( ( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) ) )  ->  E. u  e.  RR+  ( u  < 
w  /\  ( z
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
)
197 anass 630 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  (
n  e.  Z  /\  ( A. m  e.  (
ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) ) )  /\  ( u  e.  RR+  /\  (
u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) ) )  /\  w  e.  RR+ ) 
<->  ( ( ( (
ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  (
n  e.  Z  /\  ( A. m  e.  (
ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) ) )  /\  ( ( u  e.  RR+  /\  (
u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ ) ) )
198 df-3an 936 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( n  e.  Z  /\  ( A. m  e.  (
ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) )  /\  ( ( ( u  e.  RR+  /\  (
u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) )  <-> 
( ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  x )  -  (
( S  _D  ( F `  m )
) `  x )
) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) )  /\  ( ( ( u  e.  RR+  /\  (
u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) )
199 anass 630 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  <->  ( ph  /\  ( z  e.  X  /\  r  e.  RR+ )
) )
2009ralrimiva 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
201 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  =  s  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  s ) )
202201mpteq2dv 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  s  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) ) )
203 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  s  ->  ( G `  z )  =  ( G `  s ) )
204202, 203breq12d 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  s  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) )  ~~>  ( G `  s
) ) )
205204rspccva 2883 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  /\  s  e.  X )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  s
) )  ~~>  ( G `
 s ) )
206200, 205sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  s  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  s )
)  ~~>  ( G `  s ) )
207 simprll 738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  z  e.  X )
208 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  r  e.  RR+ )
209 simprr3 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  (
( ( u  e.  RR+  /\  ( u  < 
w  /\  ( z
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
)  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
w )  ->  ( abs `  ( ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  (
( r  /  2
)  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
u ) ) ) )
210 simplll 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( u  e.  RR+  /\  ( u  < 
w  /\  ( z
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
)  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
w )  ->  ( abs `  ( ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  (
( r  /  2
)  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
u ) ) )  ->  u  e.  RR+ )
211209, 210syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  u  e.  RR+ )
212 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( u  e.  RR+  /\  ( u  < 
w  /\  ( z
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
)  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
w )  ->  ( abs `  ( ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  (
( r  /  2
)  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
u ) ) )  ->  w  e.  RR+ )
213209, 212syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  w  e.  RR+ )
214 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( u  e.  RR+  /\  ( u  < 
w  /\  ( z
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
)  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
w )  ->  ( abs `  ( ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  (
( r  /  2
)  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
u ) ) )  ->  ( u  < 
w  /\  ( z
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
)
215209, 214syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  (
u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )
216215simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  u  <  w )
217215simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  (
z ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
218 simpr3 963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( u  e.  RR+  /\  ( u  < 
w  /\  ( z
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) u )  C_  X )
)  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  ( ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
w )  ->  ( abs `  ( ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  (
( r  /  2
)  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z ) )  < 
u ) ) )  ->  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) )
219209, 218syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  (
v  =/=  z  /\  ( abs `  ( v  -  z ) )  <  u ) )
220219simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  ( abs `  ( v  -  z ) )  < 
u )
221 simprr1 1003 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  n  e.  Z )
222 simprr2 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  ( A. m  e.  ( ZZ>=
`  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( r  /  2
)  /  2 )  /\  ( abs `  (
( ( S  _D  ( F `  n ) ) `  z )  -  ( H `  z ) ) )  <  ( r  / 
2 ) ) )
223222simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( v  e.  ( X  \  { z } )  /\  (
( v  =/=  z  /\  ( abs `  (
v  -  z ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) )  /\  ( v  =/=  z  /\  ( abs `  ( v  -  z
) )  <  u
) ) ) ) ) )  ->  A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 ) )
224222simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  (