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

Theorem ulmdvlem3 20271
Description: Lemma for ulmdv 20272. (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 10456 . . . . . 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 2495 . . . 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 20270 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  =  X )
12 recnprss 19744 . . . . . . . . 9  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
136, 12syl 16 . . . . . . . 8  |-  ( ph  ->  S  C_  CC )
1413adantr 452 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  S  C_  CC )
157ffvelrnda 5829 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  ( CC  ^m  X
) )
16 elmapi 6997 . . . . . . . 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 19742 . . . . . . . 8  |-  dom  ( S  _D  ( F `  k ) )  C_  S
1911, 18syl6eqssr 3359 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  S )
20 eqid 2404 . . . . . . 7  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
21 eqid 2404 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
2214, 17, 19, 20, 21dvbssntr 19740 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2311, 22eqsstr3d 3343 . . . . 5  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
2423ralrimiva 2749 . . . 4  |-  ( ph  ->  A. k  e.  Z  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X ) )
25 biidd 229 . . . . 5  |-  ( k  =  M  ->  ( X  C_  ( ( int `  ( ( TopOpen ` fld )t  S ) ) `  X )  <->  X  C_  (
( int `  (
( TopOpen ` fld )t  S ) ) `  X ) ) )
2625rspcv 3008 . . . 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 58 . . 3  |-  ( ph  ->  X  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2827sselda 3308 . 2  |-  ( (
ph  /\  z  e.  X )  ->  z  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
29 ulmcl 20250 . . . . 5  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  H : X --> CC )
3010, 29syl 16 . . . 4  |-  ( ph  ->  H : X --> CC )
3130ffvelrnda 5829 . . 3  |-  ( (
ph  /\  z  e.  X )  ->  ( H `  z )  e.  CC )
32 rphalfcl 10592 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
3332adantl 453 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
r  /  2 )  e.  RR+ )
34 rphalfcl 10592 . . . . . . 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 20247 . . . . . . . . . 10  |-  Rel  ( ~~> u `  X )
37 releldm 5061 . . . . . . . . . 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 645 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  e.  dom  (
~~> u `  X ) )
39 ulmscl 20248 . . . . . . . . . . 11  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  X  e.  _V )
4010, 39syl 16 . . . . . . . . . 10  |-  ( ph  ->  X  e.  _V )
41 ovex 6065 . . . . . . . . . . . . 13  |-  ( S  _D  ( F `  k ) )  e. 
_V
4241rgenw 2733 . . . . . . . . . . . 12  |-  A. k  e.  Z  ( S  _D  ( F `  k
) )  e.  _V
43 eqid 2404 . . . . . . . . . . . . 13  |-  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  =  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )
4443fnmpt 5530 . . . . . . . . . . . 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 20253 . . . . . . . . . . 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 643 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
484, 1, 40, 47ulmcau2 20265 . . . . . . . . 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 202 . . . . . . . 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 10459 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  Z  /\  n  e.  ( ZZ>= `  j ) )  ->  n  e.  Z )
5150ad2ant2lr 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  n  e.  Z )
52 fveq2 5687 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
5352oveq2d 6056 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  n )
) )
54 ovex 6065 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  n ) )  e. 
_V
5553, 43, 54fvmpt 5765 . . . . . . . . . . . . . . . . 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 5689 . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  ( ZZ>= `  n )
)
594uztrn2 10459 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  /\  m  e.  ( ZZ>= `  n ) )  ->  m  e.  Z )
6051, 58, 59syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  Z )
61 fveq2 5687 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  m  ->  ( F `  k )  =  ( F `  m ) )
6261oveq2d 6056 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  m  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  m )
) )
63 ovex 6065 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  m ) )  e. 
_V
6462, 43, 63fvmpt 5765 . . . . . . . . . . . . . . . . 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 5689 . . . . . . . . . . . . . . 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 6058 . . . . . . . . . . . . . 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 5691 . . . . . . . . . . . . 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 4182 . . . . . . . . . . . 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 2686 . . . . . . . . . . 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 2706 . . . . . . . . . 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 2683 . . . . . . . . 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 2686 . . . . . . . 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 202 . . . . . . 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 707 . . . . . 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 4176 . . . . . . . . 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 2708 . . . . . . . 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 2710 . . . . . . 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 3008 . . . . . 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 58 . . . . 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 707 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  M  e.  ZZ )
8253fveq1d 5689 . . . . . . . 8  |-  ( k  =  n  ->  (
( S  _D  ( F `  k )
) `  z )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
83 eqid 2404 . . . . . . . 8  |-  ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) )  =  ( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) )
84 fvex 5701 . . . . . . . 8  |-  ( ( S  _D  ( F `
 n ) ) `
 z )  e. 
_V
8582, 83, 84fvmpt 5765 . . . . . . 7  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) ) `  n )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
8685adantl 453 . . . . . 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 707 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) : Z --> ( CC 
^m  X ) )
88 simplr 732 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  z  e.  X )
89 fvex 5701 . . . . . . . . . 10  |-  ( ZZ>= `  M )  e.  _V
904, 89eqeltri 2474 . . . . . . . . 9  |-  Z  e. 
_V
9190mptex 5925 . . . . . . . 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 453 . . . . . . . . 9  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  =  ( S  _D  ( F `  n ) ) )
9493fveq1d 5689 . . . . . . . 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 2439 . . . . . . 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 707 . . . . . . 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 20256 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
)  ~~>  ( H `  z ) )
984, 81, 33, 86, 97climi2 12260 . . . . 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 12108 . . . . . . 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 12110 . . . . . . 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 205 . . . . . 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 452 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
r  /  2 )  /  2 )  e.  RR+ )
103 simpllr 736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  X )
10487ffvelrnda 5829 . . . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) )  e.  ( CC  ^m  X ) )
106 elmapi 6997 . . . . . . . . . . . . . . . . 17  |-  ( ( S  _D  ( F `
 n ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
107 fdm 5554 . . . . . . . . . . . . . . . . 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 2481 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  dom  ( S  _D  ( F `  n )
) )
1106ad3antrrr 711 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  e.  { RR ,  CC }
)
111 dvfg 19746 . . . . . . . . . . . . . . . . 17  |-  ( S  e.  { RR ,  CC }  ->  ( S  _D  ( F `  n
) ) : dom  ( S  _D  ( F `  n )
) --> CC )
112110, 111syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) ) : dom  ( S  _D  ( F `  n )
) --> CC )
113 ffun 5552 . . . . . . . . . . . . . . . 16  |-  ( ( S  _D  ( F `
 n ) ) : dom  ( S  _D  ( F `  n ) ) --> CC 
->  Fun  ( S  _D  ( F `  n ) ) )
114 funfvbrb 5802 . . . . . . . . . . . . . . . 16  |-  ( Fun  ( S  _D  ( F `  n )
)  ->  ( z  e.  dom  ( S  _D  ( F `  n ) )  <->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
) )
115112, 113, 1143syl 19 . . . . . . . . . . . . . . 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 )
) )
116109, 115mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z ( S  _D  ( F `  n ) ) ( ( S  _D  ( F `  n )
) `  z )
)
117 eqid 2404 . . . . . . . . . . . . . . 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
) ) )
118110, 12syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  C_  CC )
1197ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  F : Z --> ( CC  ^m  X ) )
120119ffvelrnda 5829 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n )  e.  ( CC  ^m  X ) )
121 elmapi 6997 . . . . . . . . . . . . . . . 16  |-  ( ( F `  n )  e.  ( CC  ^m  X )  ->  ( F `  n ) : X --> CC )
122120, 121syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n ) : X --> CC )
12319ralrimiva 2749 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. k  e.  Z  X  C_  S )
124 biidd 229 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  M  ->  ( X  C_  S  <->  X  C_  S
) )
125124rspcv 3008 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  Z  ->  ( A. k  e.  Z  X  C_  S  ->  X  C_  S ) )
1265, 123, 125sylc 58 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  C_  S )
127126ad3antrrr 711 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  S
)
12820, 21, 117, 118, 122, 127eldv 19738 . . . . . . . . . . . . . 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 ) ) ) )
129116, 128mpbid 202 . . . . . . . . . . . . 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 ) ) )
130129simprd 450 . . . . . . . . . . . 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 ) )
131126adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  S )
13213adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  S  C_  CC )
133131, 132sstrd 3318 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  CC )
134133ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  CC )
135122, 134, 103dvlem 19736 . . . . . . . . . . . . . 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 )
136135, 117fmptd 5852 . . . . . . . . . . . . 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 )
137134ssdifssd 3445 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( X  \  { z } ) 
C_  CC )
138134, 103sseldd 3309 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  CC )
139136, 137, 138ellimc3 19719 . . . . . . . . . . . 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 ) ) ) )
140130, 139mpbid 202 . . . . . . . . . . 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 ) ) )
141140simprd 450 . . . . . . . . . 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 ) )
142 fveq2 5687 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  v  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  v ) )
143142oveq1d 6055 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
( ( F `  n ) `  y
)  -  ( ( F `  n ) `
 z ) )  =  ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) ) )
144 oveq1 6047 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
y  -  z )  =  ( v  -  z ) )
145143, 144oveq12d 6058 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  v  ->  (
( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) )  =  ( ( ( ( F `  n
) `  v )  -  ( ( F `
 n ) `  z ) )  / 
( v  -  z
) ) )
146 ovex 6065 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  e. 
_V
147145, 117, 146fvmpt 5765 . . . . . . . . . . . . . . . . 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 ) ) )
148147oveq1d 6055 . . . . . . . . . . . . . . . 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 ) ) )
149148fveq2d 5691 . . . . . . . . . . . . . . 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 ) ) ) )
150 id 20 . . . . . . . . . . . . . . 15  |-  ( s  =  ( ( r  /  2 )  / 
2 )  ->  s  =  ( ( r  /  2 )  / 
2 ) )
151149, 150breqan12rd 4188 . . . . . . . . . . . . . 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 ) ) )
152151imbi2d 308 . . . . . . . . . . . . 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 ) ) ) )
153152ralbidva 2682 . . . . . . . . . . . 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 ) ) ) )
154153rexbidv 2687 . . . . . . . . . . 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 ) ) ) )
155154rspcv 3008 . . . . . . . . . 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 ) ) ) )
156102, 141, 155sylc 58 . . . . . . . . 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 ) ) )
157156adantrr 698 . . . . . . . 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 ) ) )
158 cnxmet 18760 . . . . . . . . . . . 12  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
159 xmetres2 18344 . . . . . . . . . . . 12  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S ) )
160158, 132, 159sylancr 645 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  X )  ->  (
( abs  o.  -  )  |`  ( S  X.  S
) )  e.  ( * Met `  S
) )
161160ad3antrrr 711 . . . . . . . . . 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
) )
16221cnfldtop 18771 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  e.  Top
163 resttop 17178 . . . . . . . . . . . . . . . . 17  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  S  e.  { RR ,  CC } )  -> 
( ( TopOpen ` fld )t  S )  e.  Top )
164162, 6, 163sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  Top )
16521cnfldtopon 18770 . . . . . . . . . . . . . . . . . . 19  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
166 resttopon 17179 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
167165, 13, 166sylancr 645 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
168 toponuni 16947 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
169167, 168syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  =  U. (
( TopOpen ` fld )t  S ) )
170126, 169sseqtrd 3344 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  C_  U. (
( TopOpen ` fld )t  S ) )
171 eqid 2404 . . . . . . . . . . . . . . . . 17  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
172171ntrss2 17076 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( TopOpen ` fld )t  S )  e.  Top  /\  X  C_  U. (
( TopOpen ` fld )t  S ) )  -> 
( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
173164, 170, 172syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  C_  X
)
174173, 27eqssd 3325 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X )  =  X )
175171isopn3 17085 . . . . . . . . . . . . . . 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 ) )
176164, 170, 175syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  e.  ( ( TopOpen ` fld )t  S )  <->  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
)  =  X ) )
177174, 176mpbird 224 . . . . . . . . . . . . 13  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
178 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( ( abs  o.  -  )  |`  ( S  X.  S
) )  =  ( ( abs  o.  -  )  |`  ( S  X.  S ) )
17921cnfldtopn 18769 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
180 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) )
181178, 179, 180metrest 18507 . . . . . . . . . . . . . 14  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
182158, 13, 181sylancr 645 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( S  X.  S ) ) ) )
183177, 182eleqtrd 2480 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) )
184183adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  X )  ->  X  e.  ( MetOpen `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) )
185184ad3antrrr 711 . . . . . . . . . 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
) ) ) )
18688ad2antrr 707 . . . . . . . . . 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 )
187 simprl 733 . . . . . . . . . 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+ )
188180mopni3 18477 . . . . . . . . . 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 ) )
189161, 185, 186, 187, 188syl31anc 1187 . . . . . . . . 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 )
)
190 anass 631 . . . . . . . . . . . . . . . . . 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+ ) ) )
191 df-3an 938 . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
192 anass 631 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  <->  ( ph  /\  ( z  e.  X  /\  r  e.  RR+ )
) )
1939ralrimiva 2749 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
194 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  s  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  s ) )
195194mpteq2dv 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  s  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) ) )
196 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  s  ->  ( G `  z )  =  ( G `  s ) )
197195, 196breq12d 4185 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  s  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) )  ~~>  ( G `  s
) ) )
198197rspccva 3011 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  /\  s  e.  X )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  s
) )  ~~>  ( G `
 s ) )
199193, 198sylan 458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  s  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  s )
)  ~~>  ( G `  s ) )
200 simprll 739 . . . . . . . . . . . . . . . . . . . . . . . 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 )
201 simprlr 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
) ) ) ) ) )  ->  r  e.  RR+ )
202 simprr3 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
) ) ) ) ) )  ->  (
( ( 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 ) ) ) )
203 simplll 735 . . . . . . . . . . . . . . . . . . . . . . . . 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+ )
204202, 203syl 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+ )
205 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . 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+ )
206202, 205syl 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+ )
207 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
208202, 207syl 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 ) )
209208simpld 446 . . . . . . . . . . . . . . . . . . . . . . . 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 )
210208simprd 450 . . . . . . . . . . . . . . . . . . . . . . . 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 )
211 simpr3 965 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
212202, 211syl 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 ) )
213212simprd 450 . . . . . . . . . . . . . . . . . . . . . . . 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 )
214 simprr1 1005 . . . . . . . . . . . . . . . . . . . . . . . 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 )
215 simprr2 1006 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
216215simpld 446 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
217215simprd 450 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
218 simpr1 963 . . . . . . . . . . . . . . . . . . . . . . . . . 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