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

Theorem ulmdvlem3 20320
Description: Lemma for ulmdv 20321. (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 10502 . . . . . 6  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
31, 2syl 16 . . . . 5  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
4 ulmdv.z . . . . 5  |-  Z  =  ( ZZ>= `  M )
53, 4syl6eleqr 2529 . . . 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 20319 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  =  X )
12 recnprss 19793 . . . . . . . . 9  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
136, 12syl 16 . . . . . . . 8  |-  ( ph  ->  S  C_  CC )
1413adantr 453 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  S  C_  CC )
157ffvelrnda 5872 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  ( CC  ^m  X
) )
16 elmapi 7040 . . . . . . . 8  |-  ( ( F `  k )  e.  ( CC  ^m  X )  ->  ( F `  k ) : X --> CC )
1715, 16syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k ) : X --> CC )
18 dvbsss 19791 . . . . . . . 8  |-  dom  ( S  _D  ( F `  k ) )  C_  S
1911, 18syl6eqssr 3401 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  S )
20 eqid 2438 . . . . . . 7  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
21 eqid 2438 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
2214, 17, 19, 20, 21dvbssntr 19789 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2311, 22eqsstr3d 3385 . . . . 5  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
2423ralrimiva 2791 . . . 4  |-  ( ph  ->  A. k  e.  Z  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X ) )
25 biidd 230 . . . . 5  |-  ( k  =  M  ->  ( X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X )  <->  X  C_  (
( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
2625rspcv 3050 . . . 4  |-  ( M  e.  Z  ->  ( A. k  e.  Z  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X )  ->  X  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
275, 24, 26sylc 59 . . 3  |-  ( ph  ->  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2827sselda 3350 . 2  |-  ( (
ph  /\  z  e.  X )  ->  z  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
29 ulmcl 20299 . . . . 5  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  H : X --> CC )
3010, 29syl 16 . . . 4  |-  ( ph  ->  H : X --> CC )
3130ffvelrnda 5872 . . 3  |-  ( (
ph  /\  z  e.  X )  ->  ( H `  z )  e.  CC )
32 rphalfcl 10638 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
3332adantl 454 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
r  /  2 )  e.  RR+ )
34 rphalfcl 10638 . . . . . . 7  |-  ( ( r  /  2 )  e.  RR+  ->  ( ( r  /  2 )  /  2 )  e.  RR+ )
3533, 34syl 16 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
( r  /  2
)  /  2 )  e.  RR+ )
36 ulmrel 20296 . . . . . . . . . 10  |-  Rel  ( ~~> u `  X )
37 releldm 5104 . . . . . . . . . 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 ) )
3836, 10, 37sylancr 646 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  e.  dom  (
~~> u `  X ) )
39 ulmscl 20297 . . . . . . . . . . 11  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  X  e.  _V )
4010, 39syl 16 . . . . . . . . . 10  |-  ( ph  ->  X  e.  _V )
41 ovex 6108 . . . . . . . . . . . . 13  |-  ( S  _D  ( F `  k ) )  e. 
_V
4241rgenw 2775 . . . . . . . . . . . 12  |-  A. k  e.  Z  ( S  _D  ( F `  k
) )  e.  _V
43 eqid 2438 . . . . . . . . . . . . 13  |-  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  =  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )
4443fnmpt 5573 . . . . . . . . . . . 12  |-  ( A. k  e.  Z  ( S  _D  ( F `  k ) )  e. 
_V  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  Fn  Z
)
4542, 44mp1i 12 . . . . . . . . . . 11  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  Fn  Z
)
46 ulmf2 20302 . . . . . . . . . . 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 ) )
4745, 10, 46syl2anc 644 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
484, 1, 40, 47ulmcau2 20314 . . . . . . . . 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 ) )
4938, 48mpbid 203 . . . . . . . 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 )
504uztrn2 10505 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  Z  /\  n  e.  ( ZZ>= `  j ) )  ->  n  e.  Z )
5150ad2ant2lr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  n  e.  Z )
52 fveq2 5730 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
5352oveq2d 6099 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  n )
) )
54 ovex 6108 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  n ) )  e. 
_V
5553, 43, 54fvmpt 5808 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
)  =  ( S  _D  ( F `  n ) ) )
5651, 55syl 16 . . . . . . . . . . . . . . . 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 ) ) )
5756fveq1d 5732 . . . . . . . . . . . . . . 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 ) )
58 simprr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  ( ZZ>= `  n )
)
594uztrn2 10505 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  /\  m  e.  ( ZZ>= `  n ) )  ->  m  e.  Z )
6051, 58, 59syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  Z )
61 fveq2 5730 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  m  ->  ( F `  k )  =  ( F `  m ) )
6261oveq2d 6099 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  m  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  m )
) )
63 ovex 6108 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  m ) )  e. 
_V
6462, 43, 63fvmpt 5808 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  m
)  =  ( S  _D  ( F `  m ) ) )
6560, 64syl 16 . . . . . . . . . . . . . . . 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 ) ) )
6665fveq1d 5732 . . . . . . . . . . . . . . 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 ) )
6757, 66oveq12d 6101 . . . . . . . . . . . . . 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 ) ) )
6867fveq2d 5734 . . . . . . . . . . . . 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 )
) ) )
6968breq1d 4224 . . . . . . . . . . . 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 ) )
7069ralbidv 2727 . . . . . . . . . . 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
) )
71702ralbidva 2747 . . . . . . . . . 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
) )
7271rexbidva 2724 . . . . . . . . 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
) )
7372ralbidv 2727 . . . . . . . 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
) )
7449, 73mpbid 203 . . . . . . 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 )
7574ad2antrr 708 . . . . . 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
)
76 breq2 4218 . . . . . . . . 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 ) ) )
77762ralbidv 2749 . . . . . . . 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 ) ) )
7877rexralbidv 2751 . . . . . . 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 ) ) )
7978rspcv 3050 . . . . . 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 ) ) )
8035, 75, 79sylc 59 . . . . 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 ) )
811ad2antrr 708 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  M  e.  ZZ )
8253fveq1d 5732 . . . . . . . 8  |-  ( k  =  n  ->  (
( S  _D  ( F `  k )
) `  z )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
83 eqid 2438 . . . . . . . 8  |-  ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) )  =  ( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) )
84 fvex 5744 . . . . . . . 8  |-  ( ( S  _D  ( F `
 n ) ) `
 z )  e. 
_V
8582, 83, 84fvmpt 5808 . . . . . . 7  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) ) `  n )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
8685adantl 454 . . . . . 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 ) )
8747ad2antrr 708 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) : Z --> ( CC 
^m  X ) )
88 simplr 733 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  z  e.  X )
89 fvex 5744 . . . . . . . . . 10  |-  ( ZZ>= `  M )  e.  _V
904, 89eqeltri 2508 . . . . . . . . 9  |-  Z  e. 
_V
9190mptex 5968 . . . . . . . 8  |-  ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) )  e.  _V
9291a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
)  e.  _V )
9355adantl 454 . . . . . . . . 9  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  =  ( S  _D  ( F `  n ) ) )
9493fveq1d 5732 . . . . . . . 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 ) )
9594, 86eqtr4d 2473 . . . . . . 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 ) )
9610ad2antrr 708 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H )
974, 81, 87, 88, 92, 95, 96ulmclm 20305 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
)  ~~>  ( H `  z ) )
984, 81, 33, 86, 97climi2 12307 . . . . 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 ) )
994rexanuz2 12155 . . . . . . 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 ) ) )
1004r19.2uz 12157 . . . . . . 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 ) ) )
10199, 100sylbir 206 . . . . . 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 ) ) )
10235adantr 453 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
r  /  2 )  /  2 )  e.  RR+ )
103 simpllr 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  X )
10487ffvelrnda 5872 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  e.  ( CC  ^m  X ) )
10593, 104eqeltrrd 2513 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) )  e.  ( CC  ^m  X ) )
106 elmapi 7040 . . . . . . . . . . . . . . . . 17  |-  ( ( S  _D  ( F `
 n ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
107 fdm 5597 . . . . . . . . . . . . . . . . 17  |-  ( ( S  _D  ( F `
 n ) ) : X --> CC  ->  dom  ( S  _D  ( F `  n )
)  =  X )
108105, 106, 1073syl 19 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  dom  ( S  _D  ( F `  n ) )  =  X )
109103, 108eleqtrrd 2515 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  dom  ( S  _D  ( F `  n )
) )
1106ad3antrrr 712 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  e.  { RR ,  CC }
)
111 dvfg 19795 . . . . . . . . . . . . . . . 16  |-  ( S  e.  { RR ,  CC }  ->  ( S  _D  ( F `  n
) ) : dom  ( S  _D  ( F `  n )
) --> CC )
112 ffun 5595 . . . . . . . . . . . . . . . 16  |-  ( ( S  _D  ( F `
 n ) ) : dom  ( S  _D  ( F `  n ) ) --> CC 
->  Fun  ( S  _D  ( F `  n ) ) )
113 funfvbrb 5845 . . . . . . . . . . . . . . . 16  |-  ( Fun  ( S  _D  ( F `  n )
)  ->  ( z  e.  dom  ( S  _D  ( F `  n ) )  <->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
) )
114110, 111, 112, 1134syl 20 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) )
115109, 114mpbid 203 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
)
116 eqid 2438 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( X  \  { z } ) 
|->  ( ( ( ( F `  n ) `
 y )  -  ( ( F `  n ) `  z
) )  /  (
y  -  z ) ) )  =  ( y  e.  ( X 
\  { z } )  |->  ( ( ( ( F `  n
) `  y )  -  ( ( F `
 n ) `  z ) )  / 
( y  -  z
) ) )
117110, 12syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  C_  CC )
1187ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  F : Z --> ( CC  ^m  X ) )
119118ffvelrnda 5872 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n )  e.  ( CC  ^m  X ) )
120 elmapi 7040 . . . . . . . . . . . . . . . 16  |-  ( ( F `  n )  e.  ( CC  ^m  X )  ->  ( F `  n ) : X --> CC )
121119, 120syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n ) : X --> CC )
12219ralrimiva 2791 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. k  e.  Z  X  C_  S )
123 biidd 230 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  M  ->  ( X  C_  S  <->  X  C_  S
) )
124123rspcv 3050 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  Z  ->  ( A. k  e.  Z  X  C_  S  ->  X  C_  S ) )
1255, 122, 124sylc 59 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  C_  S )
126125ad3antrrr 712 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  S
)
12720, 21, 116, 117, 121, 126eldv 19787 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) ) )
128115, 127mpbid 203 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) )
129128simprd 451 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
130125adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  S )
13113adantr 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  S  C_  CC )
132130, 131sstrd 3360 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  CC )
133132ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  CC )
134121, 133, 103dvlem 19785 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  /\  y  e.  ( X  \  { z } ) )  -> 
( ( ( ( F `  n ) `
 y )  -  ( ( F `  n ) `  z
) )  /  (
y  -  z ) )  e.  CC )
135134, 116fmptd 5895 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
136133ssdifssd 3487 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( X  \  { z } ) 
C_  CC )
137133, 103sseldd 3351 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  CC )
138135, 136, 137ellimc3 19768 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) ) )
139129, 138mpbid 203 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
140139simprd 451 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
141 fveq2 5730 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  v  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  v ) )
142141oveq1d 6098 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
( ( F `  n ) `  y
)  -  ( ( F `  n ) `
 z ) )  =  ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) ) )
143 oveq1 6090 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
y  -  z )  =  ( v  -  z ) )
144142, 143oveq12d 6101 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  v  ->  (
( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) )  =  ( ( ( ( F `  n
) `  v )  -  ( ( F `
 n ) `  z ) )  / 
( v  -  z
) ) )
145 ovex 6108 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  e. 
_V
146144, 116, 145fvmpt 5808 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
147146oveq1d 6098 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
148147fveq2d 5734 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
149 id 21 . . . . . . . . . . . . . . 15  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  s  =  ( ( r  /  2 )  / 
2 ) )
150148, 149breqan12rd 4230 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) )
151150imbi2d 309 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
152151ralbidva 2723 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
153152rexbidv 2728 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
154153rspcv 3050 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) )
155102, 140, 154sylc 59 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
156155adantrr 699 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
157 cnxmet 18809 . . . . . . . . . . . 12  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
158 xmetres2 18393 . . . . . . . . . . . 12  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S ) )
159157, 131, 158sylancr 646 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  X )  ->  (
( abs  o.  -  )  |`  ( S  X.  S
) )  e.  ( * Met `  S
) )
160159ad3antrrr 712 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) )
16121cnfldtop 18820 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  e.  Top
162 resttop 17226 . . . . . . . . . . . . . . . . 17  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  S  e.  { RR ,  CC } )  -> 
( ( TopOpen ` fld )t  S )  e.  Top )
163161, 6, 162sylancr 646 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  Top )
16421cnfldtopon 18819 . . . . . . . . . . . . . . . . . . 19  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
165 resttopon 17227 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
166164, 13, 165sylancr 646 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
167 toponuni 16994 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
168166, 167syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  =  U. (
( TopOpen ` fld )t  S ) )
169125, 168sseqtrd 3386 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  C_  U. (
( TopOpen ` fld )t  S ) )
170 eqid 2438 . . . . . . . . . . . . . . . . 17  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
171170ntrss2 17123 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( TopOpen ` fld )t  S )  e.  Top  /\  X  C_  U. (
( TopOpen ` fld )t  S ) )  -> 
( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
172163, 169, 171syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
173172, 27eqssd 3367 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  =  X )
174170isopn3 17132 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
175163, 169, 174syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  e.  ( ( TopOpen ` fld )t  S )  <->  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
)  =  X ) )
176173, 175mpbird 225 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
177 eqid 2438 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  |`  ( S  X.  S
) )  =  ( ( abs  o.  -  )  |`  ( S  X.  S ) )
17821cnfldtopn 18818 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
179 eqid 2438 . . . . . . . . . . . . . . 15  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )
180177, 178, 179metrest 18556 . . . . . . . . . . . . . 14  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
181157, 13, 180sylancr 646 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
182176, 181eleqtrd 2514 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) )
183182adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  X )  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) )
184183ad3antrrr 712 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) ) ) )
18588ad2antrr 708 . . . . . . . . . 10  |-  ( ( ( ( ( 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 )
186 simprl 734 . . . . . . . . . 10  |-  ( ( ( ( ( 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+ )
187179mopni3 18526 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) )
188160, 184, 185, 186, 187syl31anc 1188 . . . . . . . . 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 ) ) ) )  /\  ( 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 )
)
189 anass 632 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
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+ ) ) )
190 df-3an 939 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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
) ) ) ) )
191 anass 632 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  <->  ( ph  /\  ( z  e.  X  /\  r  e.  RR+ )
) )
1929ralrimiva 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
193 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  s  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  s ) )
194193mpteq2dv 4298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  s  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) ) )
195 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  s  ->  ( G `  z )  =  ( G `  s ) )
196194, 195breq12d 4227 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  s  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) )  ~~>  ( G `  s
) ) )
197196rspccva 3053 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  /\  s  e.  X )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  s
) )  ~~>  ( G `
 s ) )
198192, 197sylan 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  s )
)  ~~>  ( G `  s ) )
199 simprll 740 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 )
200 simprlr 741 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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+ )
201 simprr3 1008 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
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 ) ) ) )
202 simplll 736 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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+ )
203201, 202syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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+ )
204 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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+ )
205201, 204syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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+ )
206 simpllr 737 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
)
207201, 206syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
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 ) )
208207simpld 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 )
209207simprd 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 )
210 simpr3 966 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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
) )
211201, 210syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
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 ) )
212211simprd 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 )
213 simprr1 1006 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 )
214 simprr2 1007 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
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 ) ) )
215214simpld 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 ) )
216214simprd 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
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 `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )
217 simpr1 964 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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  =/=