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

Theorem ulmdvlem3 22923
Description: Lemma for ulmdv 22924. (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 11120 . . . . . 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 2556 . . . 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 22922 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  =  X )
12 recnprss 22434 . . . . . . . . 9  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
136, 12syl 16 . . . . . . . 8  |-  ( ph  ->  S  C_  CC )
1413adantr 465 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  S  C_  CC )
157ffvelrnda 6032 . . . . . . . 8  |-  ( (
ph  /\  k  e.  Z )  ->  ( F `  k )  e.  ( CC  ^m  X
) )
16 elmapi 7459 . . . . . . . 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 22432 . . . . . . . 8  |-  dom  ( S  _D  ( F `  k ) )  C_  S
1911, 18syl6eqssr 3550 . . . . . . 7  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  S )
20 eqid 2457 . . . . . . 7  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
21 eqid 2457 . . . . . . 7  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
2214, 17, 19, 20, 21dvbssntr 22430 . . . . . 6  |-  ( (
ph  /\  k  e.  Z )  ->  dom  ( S  _D  ( F `  k )
)  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  X
) )
2311, 22eqsstr3d 3534 . . . . 5  |-  ( (
ph  /\  k  e.  Z )  ->  X  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
2423ralrimiva 2871 . . . 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 3206 . . . 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 3499 . 2  |-  ( (
ph  /\  z  e.  X )  ->  z  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  X ) )
29 ulmcl 22902 . . . . 5  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  H : X --> CC )
3010, 29syl 16 . . . 4  |-  ( ph  ->  H : X --> CC )
3130ffvelrnda 6032 . . 3  |-  ( (
ph  /\  z  e.  X )  ->  ( H `  z )  e.  CC )
32 rphalfcl 11269 . . . . . . . 8  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
3332adantl 466 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
r  /  2 )  e.  RR+ )
34 rphalfcl 11269 . . . . . . 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 22899 . . . . . . . . . 10  |-  Rel  ( ~~> u `  X )
37 releldm 5245 . . . . . . . . . 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 663 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  e.  dom  (
~~> u `  X ) )
39 ulmscl 22900 . . . . . . . . . . 11  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  X  e.  _V )
4010, 39syl 16 . . . . . . . . . 10  |-  ( ph  ->  X  e.  _V )
41 ovex 6324 . . . . . . . . . . . . 13  |-  ( S  _D  ( F `  k ) )  e. 
_V
4241rgenw 2818 . . . . . . . . . . . 12  |-  A. k  e.  Z  ( S  _D  ( F `  k
) )  e.  _V
43 eqid 2457 . . . . . . . . . . . . 13  |-  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  =  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )
4443fnmpt 5713 . . . . . . . . . . . 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 22905 . . . . . . . . . . 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 661 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
484, 1, 40, 47ulmcau2 22917 . . . . . . . . 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 11123 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  Z  /\  n  e.  ( ZZ>= `  j ) )  ->  n  e.  Z )
5150ad2ant2lr 747 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  n  e.  Z )
52 fveq2 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
5352oveq2d 6312 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  n )
) )
54 ovex 6324 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  n ) )  e. 
_V
5553, 43, 54fvmpt 5956 . . . . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . . . 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 757 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  ( ZZ>= `  n )
)
594uztrn2 11123 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  Z  /\  m  e.  ( ZZ>= `  n ) )  ->  m  e.  Z )
6051, 58, 59syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  Z )  /\  (
n  e.  ( ZZ>= `  j )  /\  m  e.  ( ZZ>= `  n )
) )  ->  m  e.  Z )
61 fveq2 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  m  ->  ( F `  k )  =  ( F `  m ) )
6261oveq2d 6312 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  m  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  m )
) )
63 ovex 6324 . . . . . . . . . . . . . . . . . 18  |-  ( S  _D  ( F `  m ) )  e. 
_V
6462, 43, 63fvmpt 5956 . . . . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . . . 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 6314 . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . 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 4466 . . . . . . . . . . . 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 2896 . . . . . . . . . . 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 2899 . . . . . . . . . 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 2965 . . . . . . . . 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 2896 . . . . . . . 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 725 . . . . . 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 4460 . . . . . . . . 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 2901 . . . . . . . 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 2976 . . . . . . 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 3206 . . . . . 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 725 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  M  e.  ZZ )
8253fveq1d 5874 . . . . . . . 8  |-  ( k  =  n  ->  (
( S  _D  ( F `  k )
) `  z )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
83 eqid 2457 . . . . . . . 8  |-  ( k  e.  Z  |->  ( ( S  _D  ( F `
 k ) ) `
 z ) )  =  ( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) )
84 fvex 5882 . . . . . . . 8  |-  ( ( S  _D  ( F `
 n ) ) `
 z )  e. 
_V
8582, 83, 84fvmpt 5956 . . . . . . 7  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( S  _D  ( F `  k ) ) `  z ) ) `  n )  =  ( ( S  _D  ( F `  n ) ) `  z ) )
8685adantl 466 . . . . . 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 725 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) : Z --> ( CC 
^m  X ) )
88 simplr 755 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  z  e.  X )
89 fvex 5882 . . . . . . . . . 10  |-  ( ZZ>= `  M )  e.  _V
904, 89eqeltri 2541 . . . . . . . . 9  |-  Z  e. 
_V
9190mptex 6144 . . . . . . . 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 466 . . . . . . . . 9  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) `  n )  =  ( S  _D  ( F `  n ) ) )
9493fveq1d 5874 . . . . . . . 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 2501 . . . . . . 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 725 . . . . . . 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 22908 . . . . . 6  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  (
k  e.  Z  |->  ( ( S  _D  ( F `  k )
) `  z )
)  ~~>  ( H `  z ) )
984, 81, 33, 86, 97climi2 13346 . . . . 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 13194 . . . . . . 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 13196 . . . . . . 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 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( (
r  /  2 )  /  2 )  e.  RR+ )
103 simpllr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  X )
10487ffvelrnda 6032 . . . . . . . . . . . . . . . . . 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 2546 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( S  _D  ( F `  n
) )  e.  ( CC  ^m  X ) )
106 elmapi 7459 . . . . . . . . . . . . . . . . 17  |-  ( ( S  _D  ( F `
 n ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
107 fdm 5741 . . . . . . . . . . . . . . . . 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 2548 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  dom  ( S  _D  ( F `  n )
) )
1106ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  S  e.  { RR ,  CC }
)
111 dvfg 22436 . . . . . . . . . . . . . . . 16  |-  ( S  e.  { RR ,  CC }  ->  ( S  _D  ( F `  n
) ) : dom  ( S  _D  ( F `  n )
) --> CC )
112 ffun 5739 . . . . . . . . . . . . . . . 16  |-  ( ( S  _D  ( F `
 n ) ) : dom  ( S  _D  ( F `  n ) ) --> CC 
->  Fun  ( S  _D  ( F `  n ) ) )
113 funfvbrb 6001 . . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  ->  F : Z --> ( CC  ^m  X ) )
119118ffvelrnda 6032 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( F `  n )  e.  ( CC  ^m  X ) )
120 elmapi 7459 . . . . . . . . . . . . . . . 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 2871 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. k  e.  Z  X  C_  S )
123 biidd 237 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  M  ->  ( X  C_  S  <->  X  C_  S
) )
124123rspcv 3206 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  Z  ->  ( A. k  e.  Z  X  C_  S  ->  X  C_  S ) )
1255, 122, 124sylc 60 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  C_  S )
126125ad3antrrr 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  S
)
12720, 21, 116, 117, 121, 126eldv 22428 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  S )
13113adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  X )  ->  S  C_  CC )
132130, 131sstrd 3509 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  X )  ->  X  C_  CC )
133132ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  X  C_  CC )
134121, 133, 103dvlem 22426 . . . . . . . . . . . . . 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 6056 . . . . . . . . . . . . 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 3638 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  ( X  \  { z } ) 
C_  CC )
137133, 103sseldd 3500 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  /\  n  e.  Z
)  ->  z  e.  CC )
138135, 136, 137ellimc3 22409 . . . . . . . . . . . 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 463 . . . . . . . . . 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 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  v  ->  (
( F `  n
) `  y )  =  ( ( F `
 n ) `  v ) )
142141oveq1d 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
( ( F `  n ) `  y
)  -  ( ( F `  n ) `
 z ) )  =  ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) ) )
143 oveq1 6303 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  v  ->  (
y  -  z )  =  ( v  -  z ) )
144142, 143oveq12d 6314 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  v  ->  (
( ( ( F `
 n ) `  y )  -  (
( F `  n
) `  z )
)  /  ( y  -  z ) )  =  ( ( ( ( F `  n
) `  v )  -  ( ( F `
 n ) `  z ) )  / 
( v  -  z
) ) )
145 ovex 6324 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  e. 
_V
146144, 116, 145fvmpt 5956 . . . . . . . . . . . . . . . . 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 6311 . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . 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 4472 . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . 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 2968 . . . . . . . . . . 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 3206 . . . . . . . . . 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 716 . . . . . . . 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 anass 649 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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+ ) ) )
158 df-3an 975 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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
) ) ) ) )
159 anass 649 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  X )  /\  r  e.  RR+ )  <->  ( ph  /\  ( z  e.  X  /\  r  e.  RR+ )
) )
1609ralrimiva 2871 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
161 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  s  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  s ) )
162161mpteq2dv 4544 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  s  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) ) )
163 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  s  ->  ( G `  z )  =  ( G `  s ) )
164162, 163breq12d 4469 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  s  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 s ) )  ~~>  ( G `  s
) ) )
165164rspccva 3209 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  /\  s  e.  X )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  s
) )  ~~>  ( G `
 s ) )
166160, 165sylan 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  s  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  s )
)  ~~>  ( G `  s ) )
167 simprll 763 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 )
168 simprlr 764 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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+ )
169 simprr3 1046 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) ) ) )
170 simplll 759 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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+ )
171169, 170syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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+ )
172 simplr 755 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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+ )
173169, 172syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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+ )
174 simpllr 760 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
)
175169, 174syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) )
176175simpld 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 )
177175simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 )
178 simpr3 1004 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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
) )
179169, 178syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) )
180179simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 )
181 simprr1 1044 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 )
182 simprr2 1045 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) ) )
183182simpld 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 ) )
184182simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 ) )
185 simpr1 1002 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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  e.  ( X  \  { z } ) )
186169, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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  e.  ( X  \  {
z } ) )
187186eldifad 3483 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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  e.  X )
188179simpld 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 )
189 simpr2 1003 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) )  < 
w )  ->  ( abs `  ( ( ( ( ( F `  n ) `  v
)  -  ( ( F `  n ) `
 z ) )  /  ( v  -  z ) )  -  ( ( S  _D  ( F `  n ) ) `  z ) ) )  <  (
( r  /  2
)  /  2 ) ) )
190169, 189syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) )  <  w )  ->  ( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) )
191188, 190mpand 675 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 ) )  <  w  -> 
( abs `  (
( ( ( ( F `  n ) `
 v )  -  ( ( F `  n ) `  z
) )  /  (
v  -  z ) )  -  ( ( S  _D  ( F `
 n ) ) `
 z ) ) )  <  ( ( r  /  2 )  /  2 ) ) )
1924, 6, 1, 7, 8, 166, 10, 167, 168, 171, 173, 176, 177, 180, 181, 183, 184, 187, 188, 191ulmdvlem1 22921 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( (
z  e.  X  /\  r  e.  RR+ )  /\  ( n  e.  Z  /\  ( A. m  e.  ( ZZ>= `  n ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  n )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( r  /  2 )  / 
2 )  /\  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 z )  -  ( H `  z ) ) )  <  (
r  /  2 ) )  /\  ( ( ( u  e.  RR+  /\  ( u  <  w  /\  ( z ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) u )  C_  X ) )  /\  w  e.  RR+ )  /\  ( 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 `  ( ( ( ( G `  v
)  -  ( G `
 z ) )  /  ( v  -  z ) )  -  ( H `  z ) ) )  <  r
)
193