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

Theorem ulmdvlem3 21752
Description: Lemma for ulmdv 21753. (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 10863 . . . . . 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 2524 . . . 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 21751 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  =  X )
12 recnprss 21221 . . . . . . . . 9  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
136, 12syl 16 . . . . . . . 8  |-  ( ph  ->  S  C_  CC )
1413adantr 462 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  S  C_  CC )
157ffvelrnda 5831 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  ( CC  ^m  X
) )
16 elmapi 7222 . . . . . . . 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 21219 . . . . . . . 8  |-  dom  ( S  _D  ( F `  k ) )  C_  S
1911, 18syl6eqssr 3395 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  S )
20 eqid 2433 . . . . . . 7  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
21 eqid 2433 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
2214, 17, 19, 20, 21dvbssntr 21217 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2311, 22eqsstr3d 3379 . . . . 5  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
2423ralrimiva 2789 . . . 4  |-  ( ph  ->  A. k  e.  Z  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X ) )
25 biidd 237 . . . . 5  |-  ( k  =  M  ->  ( X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X )  <->  X  C_  (
( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
2625rspcv 3058 . . . 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 60 . . 3  |-  ( ph  ->  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2827sselda 3344 . 2  |-  ( (
ph  /\  z  e.  X )  ->  z  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
29 ulmcl 21731 . . . . 5  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  H : X --> CC )
3010, 29syl 16 . . . 4  |-  ( ph  ->  H : X --> CC )
3130ffvelrnda 5831 . . 3  |-  ( (
ph  /\  z  e.  X )  ->  ( H `  z )  e.  CC )
32 rphalfcl 11003 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
3332adantl 463 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
r  /  2 )  e.  RR+ )
34 rphalfcl 11003 . . . . . . 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 21728 . . . . . . . . . 10  |-  Rel  ( ~~> u `  X )
37 releldm 5059 . . . . . . . . . 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 656 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  e.  dom  (
~~> u `  X ) )
39 ulmscl 21729 . . . . . . . . . . 11  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  X  e.  _V )
4010, 39syl 16 . . . . . . . . . 10  |-  ( ph  ->  X  e.  _V )
41 ovex 6105 . . . . . . . . . . . . 13  |-  ( S  _D  ( F `  k ) )  e. 
_V
4241rgenw 2773 . . . . . . . . . . . 12  |-  A. k  e.  Z  ( S  _D  ( F `  k
) )  e.  _V
43 eqid 2433 . . . . . . . . . . . . 13  |-  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  =  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )
4443fnmpt 5525 . . . . . . . . . . . 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 21734 . . . . . . . . . . 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 654 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
484, 1, 40, 47ulmcau2 21746 . . . . . . . . 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 210 . . . . . . . 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 10866 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  Z  /\  n  e.  ( ZZ>= `  j ) )  ->  n  e.  Z )
5150ad2ant2lr 740 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  n  e.  Z )
52 fveq2 5679 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
5352oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  n )
) )
54 ovex 6105 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  n ) )  e. 
_V
5553, 43, 54fvmpt 5762 . . . . . . . . . . . . . . . . 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 5681 . . . . . . . . . . . . . . 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 749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  ( ZZ>= `  n )
)
594uztrn2 10866 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  /\  m  e.  ( ZZ>= `  n ) )  ->  m  e.  Z )
6051, 58, 59syl2anc 654 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  Z )
61 fveq2 5679 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  m  ->  ( F `  k )  =  ( F `  m ) )
6261oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  m  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  m )
) )
63 ovex 6105 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  m ) )  e. 
_V
6462, 43, 63fvmpt 5762 . . . . . . . . . . . . . . . . 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 5681 . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . 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 5683 . . . . . . . . . . . . 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 4290 . . . . . . . . . . . 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 2725 . . . . . . . . . . 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 2745 . . . . . . . . . 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 2722 . . . . . . . . 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 2725 . . . . . . . 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 210 . . . . . . 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 718 . . . . . 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 4284 . . . . . . . . 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 2747 . . . . . . . 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 2749 . . . . . . 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 3058 . . . . . 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 60 . . . . 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 718 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  M  e.  ZZ )
8253fveq1d 5681 . . . . . . . 8  |-  ( k  =  n  ->  (
( S  _D  ( F `  k )
) `  z )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
83 eqid 2433 . . . . . . . 8  |-  ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) )  =  ( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) )
84 fvex 5689 . . . . . . . 8  |-  ( ( S  _D  ( F `
 n ) ) `
 z )  e. 
_V
8582, 83, 84fvmpt 5762 . . . . . . 7  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) ) `  n )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
8685adantl 463 . . . . . 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 718 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) : Z --> ( CC 
^m  X ) )
88 simplr 747 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  z  e.  X )
89 fvex 5689 . . . . . . . . . 10  |-  ( ZZ>= `  M )  e.  _V
904, 89eqeltri 2503 . . . . . . . . 9  |-  Z  e. 
_V
9190mptex 5935 . . . . . . . 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 463 . . . . . . . . 9  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  =  ( S  _D  ( F `  n ) ) )
9493fveq1d 5681 . . . . . . . 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 2468 . . . . . . 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 718 . . . . . . 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 21737 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
)  ~~>  ( H `  z ) )
984, 81, 33, 86, 97climi2 12973 . . . . 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 12821 . . . . . . 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 12823 . . . . . . 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 213 . . . . . 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 462 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
r  /  2 )  /  2 )  e.  RR+ )
103 simpllr 751 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  X )
10487ffvelrnda 5831 . . . . . . . . . . . . . . . . . 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 2508 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) )  e.  ( CC  ^m  X ) )
106 elmapi 7222 . . . . . . . . . . . . . . . . 17  |-  ( ( S  _D  ( F `
 n ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
107 fdm 5551 . . . . . . . . . . . . . . . . 17  |-  ( ( S  _D  ( F `
 n ) ) : X --> CC  ->  dom  ( S  _D  ( F `  n )
)  =  X )
108105, 106, 1073syl 20 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  dom  ( S  _D  ( F `  n ) )  =  X )
109103, 108eleqtrrd 2510 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  dom  ( S  _D  ( F `  n )
) )
1106ad3antrrr 722 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  e.  { RR ,  CC }
)
111 dvfg 21223 . . . . . . . . . . . . . . . 16  |-  ( S  e.  { RR ,  CC }  ->  ( S  _D  ( F `  n
) ) : dom  ( S  _D  ( F `  n )
) --> CC )
112 ffun 5549 . . . . . . . . . . . . . . . 16  |-  ( ( S  _D  ( F `
 n ) ) : dom  ( S  _D  ( F `  n ) ) --> CC 
->  Fun  ( S  _D  ( F `  n ) ) )
113 funfvbrb 5804 . . . . . . . . . . . . . . . 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 21 . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
)
116 eqid 2433 . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  F : Z --> ( CC  ^m  X ) )
119118ffvelrnda 5831 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n )  e.  ( CC  ^m  X ) )
120 elmapi 7222 . . . . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. k  e.  Z  X  C_  S )
123 biidd 237 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  M  ->  ( X  C_  S  <->  X  C_  S
) )
124123rspcv 3058 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  Z  ->  ( A. k  e.  Z  X  C_  S  ->  X  C_  S ) )
1255, 122, 124sylc 60 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  C_  S )
126125ad3antrrr 722 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  S
)
12720, 21, 116, 117, 121, 126eldv 21215 . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 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 460 . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  S )
13113adantr 462 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  S  C_  CC )
132130, 131sstrd 3354 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  CC )
133132ad2antrr 718 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  CC )
134121, 133, 103dvlem 21213 . . . . . . . . . . . . . 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 5855 . . . . . . . . . . . . 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 3482 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( X  \  { z } ) 
C_  CC )
137133, 103sseldd 3345 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  CC )
138135, 136, 137ellimc3 21196 . . . . . . . . . . . 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 210 . . . . . . . . . . 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 460 . . . . . . . . . 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 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  v  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  v ) )
142141oveq1d 6095 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
( ( F `  n ) `  y
)  -  ( ( F `  n ) `
 z ) )  =  ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) ) )
143 oveq1 6087 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
y  -  z )  =  ( v  -  z ) )
144142, 143oveq12d 6098 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  v  ->  (
( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) )  =  ( ( ( ( F `  n
) `  v )  -  ( ( F `
 n ) `  z ) )  / 
( v  -  z
) ) )
145 ovex 6105 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  e. 
_V
146144, 116, 145fvmpt 5762 . . . . . . . . . . . . . . . . 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 6095 . . . . . . . . . . . . . . . 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 5683 . . . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . . 15  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  s  =  ( ( r  /  2 )  / 
2 ) )
150148, 149breqan12rd 4296 . . . . . . . . . . . . . 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 316 . . . . . . . . . . . . 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 2721 . . . . . . . . . . . 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 2726 . . . . . . . . . . 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 3058 . . . . . . . . . 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 60 . . . . . . . . 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 709 . . . . . . . 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 20194 . . . . . . . . . . . 12  |-  ( abs 
o.  -  )  e.  ( *Met `  CC )
158 xmetres2 19778 . . . . . . . . . . . 12  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  S  C_  CC )  -> 
( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( *Met `  S ) )
159157, 131, 158sylancr 656 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  X )  ->  (
( abs  o.  -  )  |`  ( S  X.  S
) )  e.  ( *Met `  S
) )
160159ad3antrrr 722 . . . . . . . . . 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 20205 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  e.  Top
162 resttop 18606 . . . . . . . . . . . . . . . . 17  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  S  e.  { RR ,  CC } )  -> 
( ( TopOpen ` fld )t  S )  e.  Top )
163161, 6, 162sylancr 656 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  Top )
16421cnfldtopon 20204 . . . . . . . . . . . . . . . . . . 19  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
165 resttopon 18607 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
166164, 13, 165sylancr 656 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
167 toponuni 18374 . . . . . . . . . . . . . . . . . 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 3380 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  C_  U. (
( TopOpen ` fld )t  S ) )
170 eqid 2433 . . . . . . . . . . . . . . . . 17  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
171170ntrss2 18503 . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
173172, 27eqssd 3361 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  =  X )
174170isopn3 18512 . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  e.  ( ( TopOpen ` fld )t  S )  <->  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
)  =  X ) )
176173, 175mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
177 eqid 2433 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  |`  ( S  X.  S
) )  =  ( ( abs  o.  -  )  |`  ( S  X.  S ) )
17821cnfldtopn 20203 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
179 eqid 2433 . . . . . . . . . . . . . . 15  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )
180177, 178, 179metrest 19941 . . . . . . . . . . . . . 14  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  S  C_  CC )  -> 
( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
181157, 13, 180sylancr 656 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
182176, 181eleqtrd 2509 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) )
183182adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  X )  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) )
184183ad3antrrr 722 . . . . . . . . . 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 718 . . . . . . . . . 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 748 . . . . . . . . . 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 19911 . . . . . . . . . 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 1214 . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . 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 960 . . . . . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  <->  ( ph  /\  ( z  e.  X  /\  r  e.  RR+ )
) )
1929ralrimiva 2789 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
193 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  s  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  s ) )
194193mpteq2dv 4367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  s  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) ) )
195 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  s  ->  ( G `  z )  =  ( G `  s ) )
196194, 195breq12d 4293 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  s  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) )  ~~>  ( G `  s
) ) )
197196rspccva 3061 . . . . . . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  s )
)  ~~>  ( G `  s ) )
199 simprll 754 . . . . . . . . . . . . . . . . . . . . . . . 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 755 . . . . . . . . . . . . . . . . . . . . . . . 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 1031 . . . . . . . . . . . . . . . . . . . . . . . . 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 750 . . . . . . . . . . . . . . . . . . . . . . . . 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 747 . . . . . . . . . . . . . . . . . . . . . . . . 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 751 . . . . . . . . . . . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . . . . . . . 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 989 . . . . . . . . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . . . . . . . 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 1029 . . . . . . . . . . . . . . . . . . . . . . . 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 1030 . . . . . . . . . . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . . . . . . . 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 987 . . . . . . . . . . . . . . . . . . . . . . . . . 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  =/=