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

Theorem ulmdvlem1 19793
Description: Lemma for ulmdv 19796. (Contributed by Mario Carneiro, 3-Mar-2015.)
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 )
ulmdvlem1.c  |-  ( (
ph  /\  ps )  ->  C  e.  X )
ulmdvlem1.r  |-  ( (
ph  /\  ps )  ->  R  e.  RR+ )
ulmdvlem1.u  |-  ( (
ph  /\  ps )  ->  U  e.  RR+ )
ulmdvlem1.v  |-  ( (
ph  /\  ps )  ->  W  e.  RR+ )
ulmdvlem1.l  |-  ( (
ph  /\  ps )  ->  U  <  W )
ulmdvlem1.b  |-  ( (
ph  /\  ps )  ->  ( C ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) U )  C_  X )
ulmdvlem1.a  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  <  U )
ulmdvlem1.n  |-  ( (
ph  /\  ps )  ->  N  e.  Z )
ulmdvlem1.1  |-  ( (
ph  /\  ps )  ->  A. m  e.  (
ZZ>= `  N ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( R  /  2
)  /  2 ) )
ulmdvlem1.2  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( S  _D  ( F `  N ) ) `  C )  -  ( H `  C ) ) )  <  ( R  / 
2 ) )
ulmdvlem1.y  |-  ( (
ph  /\  ps )  ->  Y  e.  X )
ulmdvlem1.3  |-  ( (
ph  /\  ps )  ->  Y  =/=  C )
ulmdvlem1.4  |-  ( (
ph  /\  ps )  ->  ( ( abs `  ( Y  -  C )
)  <  W  ->  ( abs `  ( ( ( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  /  ( Y  -  C ) )  -  ( ( S  _D  ( F `  N ) ) `  C ) ) )  <  ( ( R  /  2 )  / 
2 ) ) )
Assertion
Ref Expression
ulmdvlem1  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( H `  C ) ) )  <  R )
Distinct variable groups:    k, m, x, z, F    z, G    k, N, m, x    C, k, z    z, H    k, M, x    ph, k, m, x, z    S, k, m, x, z    R, m, x    k, X, m, x, z    k, Y, z    k, Z, m, x, z
Allowed substitution hints:    ps( x, z, k, m)    C( x, m)    R( z, k)    U( x, z, k, m)    G( x, k, m)    H( x, k, m)    M( z, m)    N( z)    W( x, z, k, m)    Y( x, m)

Proof of Theorem ulmdvlem1
Dummy variables  n  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ulmdv.g . . . . . 6  |-  ( ph  ->  G : X --> CC )
21adantr 451 . . . . 5  |-  ( (
ph  /\  ps )  ->  G : X --> CC )
3 ulmdvlem1.y . . . . 5  |-  ( (
ph  /\  ps )  ->  Y  e.  X )
42, 3ffvelrnd 5682 . . . 4  |-  ( (
ph  /\  ps )  ->  ( G `  Y
)  e.  CC )
5 ulmdvlem1.c . . . . 5  |-  ( (
ph  /\  ps )  ->  C  e.  X )
62, 5ffvelrnd 5682 . . . 4  |-  ( (
ph  /\  ps )  ->  ( G `  C
)  e.  CC )
74, 6subcld 9173 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( G `  Y )  -  ( G `  C )
)  e.  CC )
8 ulmdvlem1.n . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  N  e.  Z )
9 fveq2 5541 . . . . . . . . . . . . 13  |-  ( k  =  N  ->  ( F `  k )  =  ( F `  N ) )
109oveq2d 5890 . . . . . . . . . . . 12  |-  ( k  =  N  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  N )
) )
11 eqid 2296 . . . . . . . . . . . 12  |-  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  =  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )
12 ovex 5899 . . . . . . . . . . . 12  |-  ( S  _D  ( F `  N ) )  e. 
_V
1310, 11, 12fvmpt 5618 . . . . . . . . . . 11  |-  ( N  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  N
)  =  ( S  _D  ( F `  N ) ) )
148, 13syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  N
)  =  ( S  _D  ( F `  N ) ) )
15 ovex 5899 . . . . . . . . . . . . . . 15  |-  ( S  _D  ( F `  k ) )  e. 
_V
1615rgenw 2623 . . . . . . . . . . . . . 14  |-  A. k  e.  Z  ( S  _D  ( F `  k
) )  e.  _V
1711fnmpt 5386 . . . . . . . . . . . . . 14  |-  ( A. k  e.  Z  ( S  _D  ( F `  k ) )  e. 
_V  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  Fn  Z
)
1816, 17mp1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) )  Fn  Z
)
19 ulmdv.u . . . . . . . . . . . . 13  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) ( ~~> u `  X ) H )
20 ulmf2 19779 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
2118, 19, 20syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
2221adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
2322, 8ffvelrnd 5682 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  N
)  e.  ( CC 
^m  X ) )
2414, 23eqeltrrd 2371 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( S  _D  ( F `  N )
)  e.  ( CC 
^m  X ) )
25 elmapi 6808 . . . . . . . . 9  |-  ( ( S  _D  ( F `
 N ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  N ) ) : X --> CC )
2624, 25syl 15 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( S  _D  ( F `  N )
) : X --> CC )
27 fdm 5409 . . . . . . . 8  |-  ( ( S  _D  ( F `
 N ) ) : X --> CC  ->  dom  ( S  _D  ( F `  N )
)  =  X )
2826, 27syl 15 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  dom  ( S  _D  ( F `  N ) )  =  X )
29 dvbsss 19268 . . . . . . . 8  |-  dom  ( S  _D  ( F `  N ) )  C_  S
3029a1i 10 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  dom  ( S  _D  ( F `  N ) )  C_  S )
3128, 30eqsstr3d 3226 . . . . . 6  |-  ( (
ph  /\  ps )  ->  X  C_  S )
32 ulmdv.s . . . . . . . 8  |-  ( ph  ->  S  e.  { RR ,  CC } )
33 recnprss 19270 . . . . . . . 8  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
3432, 33syl 15 . . . . . . 7  |-  ( ph  ->  S  C_  CC )
3534adantr 451 . . . . . 6  |-  ( (
ph  /\  ps )  ->  S  C_  CC )
3631, 35sstrd 3202 . . . . 5  |-  ( (
ph  /\  ps )  ->  X  C_  CC )
3736, 3sseldd 3194 . . . 4  |-  ( (
ph  /\  ps )  ->  Y  e.  CC )
3836, 5sseldd 3194 . . . 4  |-  ( (
ph  /\  ps )  ->  C  e.  CC )
3937, 38subcld 9173 . . 3  |-  ( (
ph  /\  ps )  ->  ( Y  -  C
)  e.  CC )
40 ulmdvlem1.3 . . . 4  |-  ( (
ph  /\  ps )  ->  Y  =/=  C )
41 subeq0 9089 . . . . . 6  |-  ( ( Y  e.  CC  /\  C  e.  CC )  ->  ( ( Y  -  C )  =  0  <-> 
Y  =  C ) )
4237, 38, 41syl2anc 642 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( Y  -  C )  =  0  <-> 
Y  =  C ) )
4342necon3bid 2494 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( Y  -  C )  =/=  0  <->  Y  =/=  C ) )
4440, 43mpbird 223 . . 3  |-  ( (
ph  /\  ps )  ->  ( Y  -  C
)  =/=  0 )
457, 39, 44divcld 9552 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  e.  CC )
46 ulmcl 19776 . . . . 5  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  H : X --> CC )
4719, 46syl 15 . . . 4  |-  ( ph  ->  H : X --> CC )
4847adantr 451 . . 3  |-  ( (
ph  /\  ps )  ->  H : X --> CC )
4948, 5ffvelrnd 5682 . 2  |-  ( (
ph  /\  ps )  ->  ( H `  C
)  e.  CC )
5026, 5ffvelrnd 5682 . 2  |-  ( (
ph  /\  ps )  ->  ( ( S  _D  ( F `  N ) ) `  C )  e.  CC )
51 ulmdvlem1.r . . 3  |-  ( (
ph  /\  ps )  ->  R  e.  RR+ )
5251rpred 10406 . 2  |-  ( (
ph  /\  ps )  ->  R  e.  RR )
5345, 50subcld 9173 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ( ( G `  Y )  -  ( G `  C ) )  / 
( Y  -  C
) )  -  (
( S  _D  ( F `  N )
) `  C )
)  e.  CC )
5453abscld 11934 . . 3  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( S  _D  ( F `  N ) ) `  C ) ) )  e.  RR )
55 ulmdv.f . . . . . . . . . . . 12  |-  ( ph  ->  F : Z --> ( CC 
^m  X ) )
5655adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  F : Z --> ( CC 
^m  X ) )
5756, 8ffvelrnd 5682 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( F `  N
)  e.  ( CC 
^m  X ) )
58 elmapi 6808 . . . . . . . . . 10  |-  ( ( F `  N )  e.  ( CC  ^m  X )  ->  ( F `  N ) : X --> CC )
5957, 58syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( F `  N
) : X --> CC )
6059, 3ffvelrnd 5682 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( ( F `  N ) `  Y
)  e.  CC )
6159, 5ffvelrnd 5682 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( ( F `  N ) `  C
)  e.  CC )
6260, 61subcld 9173 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  e.  CC )
6362, 39, 44divcld 9552 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  e.  CC )
6445, 63subcld 9173 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( ( ( G `  Y )  -  ( G `  C ) )  / 
( Y  -  C
) )  -  (
( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  /  ( Y  -  C ) ) )  e.  CC )
6564abscld 11934 . . . 4  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  e.  RR )
6663, 50subcld 9173 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) )  -  (
( S  _D  ( F `  N )
) `  C )
)  e.  CC )
6766abscld 11934 . . . 4  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  -  ( ( S  _D  ( F `
 N ) ) `
 C ) ) )  e.  RR )
6865, 67readdcld 8878 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  +  ( abs `  (
( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  -  ( ( S  _D  ( F `
 N ) ) `
 C ) ) ) )  e.  RR )
6952rehalfcld 9974 . . 3  |-  ( (
ph  /\  ps )  ->  ( R  /  2
)  e.  RR )
7045, 50, 63abs3difd 11958 . . 3  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( S  _D  ( F `  N ) ) `  C ) ) )  <_  ( ( abs `  ( ( ( ( G `  Y )  -  ( G `  C ) )  / 
( Y  -  C
) )  -  (
( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  /  ( Y  -  C ) ) ) )  +  ( abs `  ( ( ( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  /  ( Y  -  C ) )  -  ( ( S  _D  ( F `  N ) ) `  C ) ) ) ) )
7169rehalfcld 9974 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( R  / 
2 )  /  2
)  e.  RR )
724, 60, 6, 61sub4d 9222 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) )  =  ( ( ( G `  Y
)  -  ( G `
 C ) )  -  ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) ) ) )
7372oveq1d 5889 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( ( ( G `  Y )  -  ( ( F `
 N ) `  Y ) )  -  ( ( G `  C )  -  (
( F `  N
) `  C )
) )  /  ( Y  -  C )
)  =  ( ( ( ( G `  Y )  -  ( G `  C )
)  -  ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) ) )  /  ( Y  -  C ) ) )
747, 62, 39, 44divsubdird 9591 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( ( ( G `  Y )  -  ( G `  C ) )  -  ( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
) )  /  ( Y  -  C )
)  =  ( ( ( ( G `  Y )  -  ( G `  C )
)  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )
7573, 74eqtrd 2328 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( ( ( ( G `  Y )  -  ( ( F `
 N ) `  Y ) )  -  ( ( G `  C )  -  (
( F `  N
) `  C )
) )  /  ( Y  -  C )
)  =  ( ( ( ( G `  Y )  -  ( G `  C )
)  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )
7675fveq2d 5545 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) )  /  ( Y  -  C ) ) )  =  ( abs `  ( ( ( ( G `  Y )  -  ( G `  C ) )  / 
( Y  -  C
) )  -  (
( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  /  ( Y  -  C ) ) ) ) )
774, 60subcld 9173 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( G `  Y )  -  (
( F `  N
) `  Y )
)  e.  CC )
786, 61subcld 9173 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( G `  C )  -  (
( F `  N
) `  C )
)  e.  CC )
7977, 78subcld 9173 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) )  e.  CC )
8079, 39, 44absdivd 11953 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) )  /  ( Y  -  C ) ) )  =  ( ( abs `  ( ( ( G `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( G `
 C )  -  ( ( F `  N ) `  C
) ) ) )  /  ( abs `  ( Y  -  C )
) ) )
8176, 80eqtr3d 2330 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  =  ( ( abs `  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  /  ( abs `  ( Y  -  C ) ) ) )
82 eqid 2296 . . . . . . . 8  |-  ( ZZ>= `  N )  =  (
ZZ>= `  N )
83 ulmdv.z . . . . . . . . . 10  |-  Z  =  ( ZZ>= `  M )
848, 83syl6eleq 2386 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  N  e.  ( ZZ>= `  M ) )
85 eluzelz 10254 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
8684, 85syl 15 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  N  e.  ZZ )
87 ulmdv.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ZZ )
8887adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  M  e.  ZZ )
89 ulmdv.l . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  ~~>  ( G `  z ) )
9089ralrimiva 2639 . . . . . . . . . . . . 13  |-  ( ph  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
9190adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
92 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( z  =  Y  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  Y ) )
9392mpteq2dv 4123 . . . . . . . . . . . . . 14  |-  ( z  =  Y  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 Y ) ) )
94 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( z  =  Y  ->  ( G `  z )  =  ( G `  Y ) )
9593, 94breq12d 4052 . . . . . . . . . . . . 13  |-  ( z  =  Y  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 Y ) )  ~~>  ( G `  Y
) ) )
9695rspcv 2893 . . . . . . . . . . . 12  |-  ( Y  e.  X  ->  ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  -> 
( k  e.  Z  |->  ( ( F `  k ) `  Y
) )  ~~>  ( G `
 Y ) ) )
973, 91, 96sylc 56 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  Y
) )  ~~>  ( G `
 Y ) )
98 fvex 5555 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  M )  e.  _V
9983, 98eqeltri 2366 . . . . . . . . . . . . 13  |-  Z  e. 
_V
10099mptex 5762 . . . . . . . . . . . 12  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  Y )  -  ( ( F `
 N ) `  Y ) ) )  e.  _V
101100a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
) )  e.  _V )
102 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
103102fveq1d 5543 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( F `  k
) `  Y )  =  ( ( F `
 n ) `  Y ) )
104 eqid 2296 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( F `  k ) `
 Y ) )  =  ( k  e.  Z  |->  ( ( F `
 k ) `  Y ) )
105 fvex 5555 . . . . . . . . . . . . . 14  |-  ( ( F `  n ) `
 Y )  e. 
_V
106103, 104, 105fvmpt 5618 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  Y
) ) `  n
)  =  ( ( F `  n ) `
 Y ) )
107106adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  Y )
) `  n )  =  ( ( F `
 n ) `  Y ) )
10856ffvelrnda 5681 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( F `  n )  e.  ( CC  ^m  X ) )
109 elmapi 6808 . . . . . . . . . . . . . 14  |-  ( ( F `  n )  e.  ( CC  ^m  X )  ->  ( F `  n ) : X --> CC )
110108, 109syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( F `  n ) : X --> CC )
1113adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  Y  e.  X )
112110, 111ffvelrnd 5682 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  n ) `  Y )  e.  CC )
113107, 112eqeltrd 2370 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  Y )
) `  n )  e.  CC )
114103oveq1d 5889 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
115 eqid 2296 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  Y )  -  ( ( F `
 N ) `  Y ) ) )  =  ( k  e.  Z  |->  ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
116 ovex 5899 . . . . . . . . . . . . . 14  |-  ( ( ( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) )  e. 
_V
117114, 115, 116fvmpt 5618 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
) ) `  n
)  =  ( ( ( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) ) )
118117adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) ) ) `  n )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
119107oveq1d 5889 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( k  e.  Z  |->  ( ( F `  k ) `  Y
) ) `  n
)  -  ( ( F `  N ) `
 Y ) )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
120118, 119eqtr4d 2331 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) ) ) `  n )  =  ( ( ( k  e.  Z  |->  ( ( F `  k
) `  Y )
) `  n )  -  ( ( F `
 N ) `  Y ) ) )
12183, 88, 97, 60, 101, 113, 120climsubc1 12127 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
) )  ~~>  ( ( G `  Y )  -  ( ( F `
 N ) `  Y ) ) )
12299mptex 5762 . . . . . . . . . . 11  |-  ( k  e.  Z  |->  ( ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  k ) `
 C )  -  ( ( F `  N ) `  C
) ) ) )  e.  _V
123122a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  e.  _V )
124 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( z  =  C  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  C ) )
125124mpteq2dv 4123 . . . . . . . . . . . . . 14  |-  ( z  =  C  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 C ) ) )
126 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( z  =  C  ->  ( G `  z )  =  ( G `  C ) )
127125, 126breq12d 4052 . . . . . . . . . . . . 13  |-  ( z  =  C  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 C ) )  ~~>  ( G `  C
) ) )
128127rspcv 2893 . . . . . . . . . . . 12  |-  ( C  e.  X  ->  ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  -> 
( k  e.  Z  |->  ( ( F `  k ) `  C
) )  ~~>  ( G `
 C ) ) )
1295, 91, 128sylc 56 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  C
) )  ~~>  ( G `
 C ) )
13099mptex 5762 . . . . . . . . . . . 12  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) )  e.  _V
131130a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) )  e.  _V )
132102fveq1d 5543 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( F `  k
) `  C )  =  ( ( F `
 n ) `  C ) )
133 eqid 2296 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( F `  k ) `
 C ) )  =  ( k  e.  Z  |->  ( ( F `
 k ) `  C ) )
134 fvex 5555 . . . . . . . . . . . . . 14  |-  ( ( F `  n ) `
 C )  e. 
_V
135132, 133, 134fvmpt 5618 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  C
) ) `  n
)  =  ( ( F `  n ) `
 C ) )
136135adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  C )
) `  n )  =  ( ( F `
 n ) `  C ) )
1375adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  C  e.  X )
138110, 137ffvelrnd 5682 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  n ) `  C )  e.  CC )
139136, 138eqeltrd 2370 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  C )
) `  n )  e.  CC )
140132oveq1d 5889 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
141 eqid 2296 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) )  =  ( k  e.  Z  |->  ( ( ( F `  k ) `
 C )  -  ( ( F `  N ) `  C
) ) )
142 ovex 5899 . . . . . . . . . . . . . 14  |-  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) )  e. 
_V
143140, 141, 142fvmpt 5618 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) ) `  n
)  =  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) )
144143adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) `  n )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
145136oveq1d 5889 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( k  e.  Z  |->  ( ( F `  k ) `  C
) ) `  n
)  -  ( ( F `  N ) `
 C ) )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
146144, 145eqtr4d 2331 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) `  n )  =  ( ( ( k  e.  Z  |->  ( ( F `  k
) `  C )
) `  n )  -  ( ( F `
 N ) `  C ) ) )
14783, 88, 129, 61, 131, 139, 146climsubc1 12127 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) )  ~~>  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) )
14860adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  N ) `  Y )  e.  CC )
149112, 148subcld 9173 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) )  e.  CC )
150118, 149eqeltrd 2370 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) ) ) `  n )  e.  CC )
15161adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  N ) `  C )  e.  CC )
152138, 151subcld 9173 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) )  e.  CC )
153144, 152eqeltrd 2370 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) `  n )  e.  CC )
154114, 140oveq12d 5892 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  (
( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) )  =  ( ( ( ( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) )  -  ( ( ( F `
 n ) `  C )  -  (
( F `  N
) `  C )
) ) )
155 eqid 2296 . . . . . . . . . . . . 13  |-  ( k  e.  Z  |->  ( ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  k ) `
 C )  -  ( ( F `  N ) `  C
) ) ) )  =  ( k  e.  Z  |->  ( ( ( ( F `  k
) `  Y )  -  ( ( F `
 N ) `  Y ) )  -  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) ) )
156 ovex 5899 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )  e. 
_V
157154, 155, 156fvmpt 5618 . . . . . . . . . . . 12  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) `  n
)  =  ( ( ( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) ) )
158157adantl 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) `  n )  =  ( ( ( ( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) )  -  ( ( ( F `
 n ) `  C )  -  (
( F `  N
) `  C )
) ) )
159118, 144oveq12d 5892 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( k  e.  Z  |->  ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
) ) `  n
)  -  ( ( k  e.  Z  |->  ( ( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) `  n ) )  =  ( ( ( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) ) )
160158, 159eqtr4d 2331 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) `  n )  =  ( ( ( k  e.  Z  |->  ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) ) ) `  n )  -  ( ( k  e.  Z  |->  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) `
 n ) ) )
16183, 88, 121, 123, 147, 150, 153, 160climsub 12123 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  ~~>  ( ( ( G `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( G `
 C )  -  ( ( F `  N ) `  C
) ) ) )
16299mptex 5762 . . . . . . . . . 10  |-  ( k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) )  e. 
_V
163162a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( abs `  (
( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) )  e.  _V )
164149, 152subcld 9173 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )  e.  CC )
165158, 164eqeltrd 2370 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) `  n )  e.  CC )
166154fveq2d 5545 . . . . . . . . . . . 12  |-  ( k  =  n  ->  ( abs `  ( ( ( ( F `  k
) `  Y )  -  ( ( F `
 N ) `  Y ) )  -  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) ) )  =  ( abs `  (
( ( ( F `
 n ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) )
167 eqid 2296 . . . . . . . . . . . 12  |-  ( k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) )  =  ( k  e.  Z  |->  ( abs `  (
( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) )
168 fvex 5555 . . . . . . . . . . . 12  |-  ( abs `  ( ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  n ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  e.  _V
169166, 167, 168fvmpt 5618 . . . . . . . . . . 11  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( abs `  (
( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) ) `  n
)  =  ( abs `  ( ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  n ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) )
170169adantl 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  k ) `
 C )  -  ( ( F `  N ) `  C
) ) ) ) ) `  n )  =  ( abs `  (
( ( ( F `
 n ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) )
171158fveq2d 5545 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( abs `  ( ( k  e.  Z  |->  ( ( ( ( F `  k
) `  Y )  -  ( ( F `
 N ) `  Y ) )  -  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) ) ) `  n ) )  =  ( abs `  (
( ( ( F `
 n ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) )
172170, 171eqtr4d 2331 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  k ) `
 C )  -  ( ( F `  N ) `  C
) ) ) ) ) `  n )  =  ( abs `  (
( k  e.  Z  |->  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) `  n
) ) )
17383, 161, 163, 88, 165, 172climabs 12093 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( abs `  (
( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) )  ~~>  ( abs `  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) )
17439abscld 11934 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  e.  RR )
17571, 174remulcld 8879 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) )  e.  RR )
176175recnd 8877 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) )  e.  CC )
17783eqimss2i 3246 . . . . . . . . . 10  |-  ( ZZ>= `  M )  C_  Z
178177, 99climconst2 12038 . . . . . . . . 9  |-  ( ( ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) )  e.  CC  /\  M  e.  ZZ )  ->  ( Z  X.  { ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) } )  ~~>  ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) )
179176, 88, 178syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( Z  X.  {
( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) } )  ~~>  ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
18083uztrn2 10261 . . . . . . . . . . 11  |-  ( ( N  e.  Z  /\  n  e.  ( ZZ>= `  N ) )  ->  n  e.  Z )
1818, 180sylan 457 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  n  e.  Z
)
182181, 169syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) ) `  n )  =  ( abs `  ( ( ( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) ) ) )
183164abscld 11934 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( abs `  ( ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  n ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  e.  RR )
184181, 183syldan 456 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( abs `  (
( ( ( F `
 n ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) ) )  e.  RR )
185182, 184eqeltrd 2370 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) ) `  n )  e.  RR )
186 ovex 5899 . . . . . . . . . . 11  |-  ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) )  e.  _V
187186fvconst2 5745 . . . . . . . . . 10  |-  ( n  e.  Z  ->  (
( Z  X.  {
( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) } ) `  n
)  =  ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
188181, 187syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( Z  X.  { ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) } ) `
 n )  =  ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) )
189175adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( R  /  2 )  /  2 )  x.  ( abs `  ( Y  -  C )
) )  e.  RR )
190188, 189eqeltrd 2370 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( Z  X.  { ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) } ) `
 n )  e.  RR )
191181, 110syldan 456 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  n ) : X --> CC )
192 ffn 5405 . . . . . . . . . . . . . 14  |-  ( ( F `  n ) : X --> CC  ->  ( F `  n )  Fn  X )
193191, 192syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  n )  Fn  X
)
19459adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  N ) : X --> CC )
195 ffn 5405 . . . . . . . . . . . . . 14  |-  ( ( F `  N ) : X --> CC  ->  ( F `  N )  Fn  X )
196194, 195syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  N )  Fn  X
)
197 ulmscl 19774 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  X  e.  _V )
19819, 197syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  _V )
199198ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  X  e.  _V )
2003adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  Y  e.  X
)
201 fnfvof 6106 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  n )  Fn  X  /\  ( F `  N
)  Fn  X )  /\  ( X  e. 
_V  /\  Y  e.  X ) )  -> 
( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 Y )  =  ( ( ( F `
 n ) `  Y )  -  (
( F `  N
) `  Y )
) )
202193, 196, 199, 200, 201syl22anc 1183 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( F `  n )  o F  -  ( F `  N )
) `  Y )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
2035adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  C  e.  X
)
204 fnfvof 6106 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  n )  Fn  X  /\  ( F `  N
)  Fn  X )  /\  ( X  e. 
_V  /\  C  e.  X ) )  -> 
( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 C )  =  ( ( ( F `
 n ) `  C )  -  (
( F `  N
) `  C )
) )
205193, 196, 199, 203, 204syl22anc 1183 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( F `  n )  o F  -  ( F `  N )
) `  C )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
206202, 205oveq12d 5892 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( ( F `  n
)  o F  -  ( F `  N ) ) `  Y )  -  ( ( ( F `  n )  o F  -  ( F `  N )
) `  C )
)  =  ( ( ( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) ) )
207206fveq2d 5545 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( abs `  (
( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 Y )  -  ( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 C ) ) )  =  ( abs `  ( ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  n ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) )
20831, 3sseldd 3194 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ps )  ->  Y  e.  S )
20931, 5sseldd 3194 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ps )  ->  C  e.  S )
210208, 209ovresd 6004 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S
) ) C )  =  ( Y ( abs  o.  -  ) C ) )
211 eqid 2296 . . . . . . . . . . . . . . . . . 18  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
212211cnmetdval 18296 . . . . . . . . . . . . . . . . 17  |-  ( ( Y  e.  CC  /\  C  e.  CC )  ->  ( Y ( abs 
o.  -  ) C
)  =  ( abs `  ( Y  -  C
) ) )
21337, 38, 212syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  ( Y ( abs 
o.  -  ) C
)  =  ( abs `  ( Y  -  C
) ) )
214210, 213eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S
) ) C )  =  ( abs `  ( Y  -  C )
) )
215 ulmdvlem1.a . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  <  U )
216214, 215eqbrtrd 4059 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S
) ) C )  <  U )
217 cnxmet 18298 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
218 xmetres2 17941 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S ) )
219217, 35, 218sylancr 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S ) )
220 ulmdvlem1.u . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  U  e.  RR+ )
221220rpxrd 10407 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  U  e.  RR* )
222 elbl3 17967 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( abs 
o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S )  /\  U  e.  RR* )  /\  ( C  e.  S  /\  Y  e.  S )
)  ->  ( Y  e.  ( C ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) U )  <->  ( Y
( ( abs  o.  -  )  |`  ( S  X.  S ) ) C )  <  U
) )
223219, 221, 209, 208, 222syl22anc 1183 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  ( Y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )  <->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S ) ) C )  <  U ) )
224216, 223mpbird 223 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  Y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
225224adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  Y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
226 blcntr 17980 . . . . . . . . . . . . . 14  |-  ( ( ( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S )  /\  C  e.  S  /\  U  e.  RR+ )  ->  C  e.  ( C ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) U ) )
227219, 209, 220, 226syl3anc 1182 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  C  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
228227adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  C  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
229225, 228jca 518 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( Y  e.  ( C ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) U )  /\  C  e.  ( C
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) ) )
23032ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  S  e.  { RR ,  CC } )
231 eqid 2296 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  |`  ( S  X.  S
) )  =  ( ( abs  o.  -  )  |`  ( S  X.  S ) )
23231adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  X  C_  S
)
233191ffvelrnda 5681 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  n
) `  y )  e.  CC )
234194ffvelrnda 5681 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  N
) `  y )  e.  CC )
235233, 234subcld 9173 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( ( F `  n ) `  y
)  -  ( ( F `  N ) `
 y ) )  e.  CC )
236 eqid 2296 . . . . . . . . . . . . . 14  |-  ( y  e.  X  |->  ( ( ( F `  n
) `  y )  -  ( ( F `
 N ) `  y ) ) )  =  ( y  e.  X  |->  ( ( ( F `  n ) `
 y )  -  ( ( F `  N ) `  y
) ) )
237235, 236fmptd 5700 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( y  e.  X  |->  ( ( ( F `  n ) `
 y )  -  ( ( F `  N ) `  y
) ) ) : X --> CC )
238 fvex 5555 . . . . . . . . . . . . . . . 16  |-  ( ( F `  n ) `
 y )  e. 
_V
239238a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  n
) `  y )  e.  _V )
240 fvex 5555 . . . . . . . . . . . . . . . 16  |-  ( ( F `  N ) `
 y )  e. 
_V
241240a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  N
) `  y )  e.  _V )
242191feqmptd 5591 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  n )  =  ( y  e.  X  |->  ( ( F `  n
) `  y )
) )
243194feqmptd 5591 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  N )  =  ( y  e.  X  |->  ( ( F `  N
) `  y )
) )
244199, 239, 241, 242, 243offval2 6111 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( F `
 n )  o F  -  ( F `
 N ) )  =  ( y  e.  X  |->  ( ( ( F `  n ) `
 y )  -  ( ( F `  N ) `  y
) ) ) )
245244feq1d 5395 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( F `  n )  o F  -  ( F `  N )
) : X --> CC  <->  ( y  e.  X  |->  ( ( ( F `  n
) `  y )  -  ( ( F `
 N ) `  y ) ) ) : X --> CC ) )
246237, 245mpbird 223 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( F `
 n )  o F  -  ( F `
 N ) ) : X --> CC )
247209adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  C  e.  S
)
248221adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  U  e.  RR* )
249 eqid 2296 . . . . . . . . . . . 12  |-  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )  =  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )
250 ulmdvlem1.b . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  ( C ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) U )  C_  X )
251250adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( C (
ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )  C_  X )
252244oveq2d 5890 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( ( F `  n )  o F  -  ( F `  N ) ) )  =  ( S  _D  ( y  e.  X  |->  ( ( ( F `
 n ) `  y )  -  (
( F `  N
) `  y )
) ) ) )
253 fvex 5555 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  _D  ( F `
 n ) ) `
 y )  e. 
_V
254253a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  n )
) `  y )  e.  _V )
255242oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) )  =  ( S  _D  ( y  e.  X  |->  ( ( F `
 n ) `  y ) ) ) )
256102oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  n  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  n )
) )
257 ovex 5899 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S  _D  ( F `  n ) )  e. 
_V
258256, 11, 257fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
)  =  ( S  _D  ( F `  n ) ) )
259181, 258syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 n )  =  ( S  _D  ( F `  n )
) )
26021ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) : Z --> ( CC  ^m  X ) )
261260, 181ffvelrnd 5682 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 n )  e.  ( CC  ^m  X
) )
262259, 261eqeltrrd 2371 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) )  e.  ( CC 
^m  X ) )
263 elmapi 6808 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( S  _D  ( F `
 n ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
264262, 263syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
265264feqmptd 5591 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `
 n ) ) `
 y ) ) )
266255, 265eqtr3d 2330 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( y  e.  X  |->  ( ( F `  n ) `  y
) ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `  n ) ) `  y ) ) )
267 fvex 5555 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  _D  ( F `
 N ) ) `
 y )  e. 
_V
268267a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  N )
) `  y )  e.  _V )
269243oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  N ) )  =  ( S  _D  ( y  e.  X  |->  ( ( F `
 N ) `  y ) ) ) )
27026adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  N ) ) : X --> CC )
271270feqmptd 5591 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  N ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `
 N ) ) `
 y ) ) )
272269, 271eqtr3d 2330 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( y  e.  X  |->  ( ( F `  N ) `  y
) ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `  N ) ) `  y ) ) )
273230, 233, 254, 266, 234, 268, 272dvmptsub 19332 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( y  e.  X  |->  ( ( ( F `
 n ) `  y )  -  (
( F `  N
) `  y )
) ) )  =  ( y  e.  X  |->  ( ( ( S  _D  ( F `  n ) ) `  y )  -  (
( S  _D  ( F `  N )
) `  y )
) ) )
274252, 273eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( ( F `  n )  o F  -  ( F `  N ) ) )  =  ( y  e.  X  |->  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) ) )
275274dmeqd 4897 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  dom  ( S  _D  ( ( F `  n )  o F  -  ( F `  N ) ) )  =  dom  ( y  e.  X  |->  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) ) )
276 ovex 5899 . . . . . . . . . . . . . . 15  |-  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) )  e. 
_V
277 eqid 2296 . . . . . . . . . . . . . . 15  |-  ( y  e.  X  |->  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  =  ( y  e.  X  |->  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )
278276, 277dmmpti 5389 . . . . . . . . . . . . . 14  |-  dom  (
y  e.  X  |->  ( ( ( S  _D  ( F `  n ) ) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  =  X
279275, 278syl6eq 2344 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  dom  ( S  _D  ( ( F `  n )  o F  -  ( F `  N ) ) )  =  X )
280251, 279sseqtr4d 3228 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( C (
ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )  C_  dom  ( S  _D  ( ( F `
 n )  o F  -  ( F `
 N ) ) ) )
28171adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( R  /  2 )  / 
2 )  e.  RR )
282251sselda 3193 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )  ->  y  e.  X )
283274fveq1d 5543 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( S  _D  ( ( F `
 n )  o F  -  ( F `
 N ) ) ) `  y )  =  ( ( y  e.  X  |->  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) ) `
 y ) )
284277fvmpt2 5624 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  X  /\  ( ( ( S  _D  ( F `  n ) ) `  y )  -  (
( S  _D  ( F `  N )
) `  y )
)  e.  _V )  ->  ( ( y  e.  X  |->  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) ) `  y
)  =  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )
285276, 284mpan2 652 . . . . . . . . . . . . . . . 16  |-  ( y  e.  X  ->  (
( y  e.  X  |->  ( ( ( S  _D  ( F `  n ) ) `  y )  -  (
( S  _D  ( F `  N )
) `  y )
) ) `  y
)  =  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )
286283, 285sylan9eq 2348 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  (
( F `  n
)  o F  -  ( F `  N ) ) ) `  y
)  =  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )
287286fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( S  _D  ( ( F `
 n )  o F  -  ( F `
 N ) ) ) `  y ) )  =  ( abs `  ( ( ( S  _D  ( F `  n ) ) `  y )  -  (
( S  _D  ( F `  N )
) `  y )
) ) )
288276a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( ( S  _D  ( F `  n ) ) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) )  e. 
_V )
289230, 235, 288, 273dvmptcl 19324 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( ( S  _D  ( F `  n ) ) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) )  e.  CC )
290289abscld 11934 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  e.  RR )
29171ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( R  /  2
)  /  2 )  e.  RR )
292264ffvelrnda 5681 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  n )
) `  y )  e.  CC )
293270ffvelrnda 5681 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  N )
) `  y )  e.  CC )
294292, 293abssubd 11951 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  =  ( abs `  ( ( ( S  _D  ( F `  N )
) `  y )  -  ( ( S  _D  ( F `  n ) ) `  y ) ) ) )
295 ulmdvlem1.1 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ps )  ->  A. m  e.  (
ZZ>= `  N ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( R  /  2
)  /  2 ) )
296 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  =  n  ->  ( F `  m )  =  ( F `  n ) )
297296oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  =  n  ->  ( S  _D  ( F `  m ) )  =  ( S  _D  ( F `  n )
) )
298297fveq1d 5543 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  =  n  ->  (
( S  _D  ( F `  m )
) `  x )  =  ( ( S  _D  ( F `  n ) ) `  x ) )
299298oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  (
( ( S  _D  ( F `  N ) ) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) )  =  ( ( ( S  _D  ( F `  N ) ) `  x )  -  (
( S  _D  ( F `  n )
) `  x )
) )
300299fveq2d 5545 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  n  ->  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  =  ( abs `  ( ( ( S  _D  ( F `  N )
) `  x )  -  ( ( S  _D  ( F `  n ) ) `  x ) ) ) )
301300breq1d 4049 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
( abs `  (
( ( S  _D  ( F `  N ) ) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( R  /  2 )  / 
2 )  <->  ( abs `  ( ( ( S  _D  ( F `  N ) ) `  x )  -  (
( S  _D  ( F `  n )
) `  x )
) )  <  (
( R  /  2
)  /  2 ) ) )
302301ralbidv 2576 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  ( A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  N )
) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  ( ( R  /  2 )  / 
2 )  <->  A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  N ) ) `  x )  -  (
( S  _D  ( F `  n )
) `  x )
) )  <  (
( R  /  2
)  /  2 ) ) )
303302rspccva 2896 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. m  e.  (
ZZ>= `  N ) A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 x )  -  ( ( S  _D  ( F `  m ) ) `  x ) ) )  <  (
( R  /  2
)  /  2 )  /\  n  e.  (
ZZ>= `  N ) )  ->  A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  N )
) `  x )  -  ( ( S  _D  ( F `  n ) ) `  x ) ) )  <  ( ( R  /  2 )  / 
2 ) )
304295, 303sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  N )
) `  x )  -  ( ( S  _D  ( F `  n ) ) `  x ) ) )  <  ( ( R  /  2 )  / 
2 ) )
305 fveq2 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( S  _D  ( F `  N )
) `  x )  =  ( ( S  _D  ( F `  N ) ) `  y ) )
306 fveq2 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( S  _D  ( F `  n )
) `  x )  =  ( ( S  _D  ( F `  n ) ) `  y ) )
307305, 306oveq12d 5892 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
( ( S  _D  ( F `  N ) ) `  x )  -  ( ( S  _D  ( F `  n ) ) `  x ) )  =  ( ( ( S  _D  ( F `  N ) ) `  y )  -  (
( S  _D  ( F `  n )
) `  y )
) )
308307fveq2d 5545 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 x )  -  ( ( S  _D  ( F `  n ) ) `  x ) ) )  =  ( abs `  ( ( ( S  _D  ( F `  N )
) `  y )  -  ( ( S  _D  ( F `  n ) ) `  y ) ) ) )
309308breq1d 4049 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
( abs `  (
( ( S  _D  ( F `  N ) ) `  x )  -  ( ( S  _D  ( F `  n ) ) `  x ) ) )  <  ( ( R  /  2 )  / 
2 )  <->  ( abs `  ( ( ( S  _D  ( F `  N ) ) `  y )  -  (
( S  _D  ( F `  n )
) `  y )
) )  <  (
( R  /  2
)  /  2 ) ) )
310309rspccva 2896 . . . . . . . . . . . . . . . . 17  |-  ( ( A. x  e.  X  ( abs `  ( ( ( S  _D  ( F `  N )
) `  x )  -  ( ( S  _D  ( F `  n ) ) `  x ) ) )  <  ( ( R  /  2 )  / 
2 )  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 y )  -  ( ( S  _D  ( F `  n ) ) `  y ) ) )  <  (
( R  /  2
)  /  2 ) )
311304, 310sylan 457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 y )  -  ( ( S  _D  ( F `  n ) ) `  y ) ) )  <  (
( R  /  2
)  /  2 ) )
312294, 311eqbrtrd 4059 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  <  (
( R  /  2
)  /  2 ) )
313290, 291, 312ltled 8983 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  <_  (
( R  /  2
)  /  2 ) )
314287, 313eqbrtrd 4059 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( S  _D  ( ( F `
 n )  o F  -  ( F `
 N ) ) ) `  y ) )  <_  ( ( R  /  2 )  / 
2 ) )
315282, 314syldan 456 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )  ->  ( abs `  ( ( S  _D  ( ( F `
 n )  o F  -  ( F `
 N ) ) ) `  y ) )  <_  ( ( R  /  2 )  / 
2 ) )
316230, 231, 232, 246, 247, 248, 249, 280, 281, 315dvlip2 19358 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  ( Y  e.  ( C ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) U )  /\  C  e.  ( C
( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) ) )  -> 
( abs `  (
( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 Y )  -  ( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 C ) ) )  <_  ( (
( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
317229, 316mpdan 649 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( abs `  (
( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 Y )  -  ( ( ( F `
 n )  o F  -  ( F `
 N ) ) `
 C ) ) )  <_  ( (
( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
318207, 317eqbrtrrd 4061 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( abs `  (
( ( ( F `
 n ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) ) )  <_  ( (
( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
319318, 182, 1883brtr4d 4069 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) ) `  n )  <_  (
( Z  X.  {
( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) } ) `  n
) )
32082, 86, 173, 179, 185, 190, 319climle 12129 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( G `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) ) )  <_  ( (
( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
32179abscld 11934 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( G `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) ) )  e.  RR )
32239, 44absrpcld 11946 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  e.  RR+ )
323321, 71, 322ledivmul2d 10456 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ( ( abs `  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  /  ( abs `  ( Y  -  C ) ) )  <_  ( ( R  /  2 )  / 
2 )  <->  ( abs `  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  <_  (
( ( R  / 
2 )  /  2
)  x.  ( abs `  ( Y  -  C
) ) ) ) )
324320, 323mpbird 223 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( abs `  (
( ( G `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) ) )  /  ( abs `  ( Y  -  C
) ) )  <_ 
( ( R  / 
2 )  /  2
) )
32581, 324eqbrtrd 4059 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  <_  ( ( R  /  2 )  / 
2 ) )
326220rpred 10406 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  U  e.  RR )
327 ulmdvlem1.v . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  W  e.  RR+ )
328327rpred 10406 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  W  e.  RR )
329 ulmdvlem1.l . . . . . . 7  |-  ( (
ph  /\  ps )  ->  U  <  W )
330174, 326, 328, 215, 329lttrd 8993 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  <  W )
331 ulmdvlem1.4 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( abs `  ( Y  -  C )
)  <  W  ->  ( abs `  ( ( ( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  /  ( Y  -  C ) )  -  ( ( S  _D  ( F `  N ) ) `  C ) ) )  <  ( ( R  /  2 )  / 
2 ) ) )
332330, 331mpd 14 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  -  ( ( S  _D  ( F `
 N ) ) `
 C ) ) )  <  ( ( R  /  2 )  /  2 ) )
33365, 67, 71, 71, 325, 332leltaddd 9409 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  +  ( abs `  (
( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  -  ( ( S  _D  ( F `
 N ) ) `
 C ) ) ) )  <  (
( ( R  / 
2 )  /  2
)  +  ( ( R  /  2 )  /  2 ) ) )
33469recnd 8877 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( R  /  2
)  e.  CC )
3353342halvesd 9973 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ( R  /  2 )  / 
2 )  +  ( ( R  /  2
)  /  2 ) )  =  ( R  /  2 ) )
336333, 335breqtrd 4063 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  +  ( abs `  (
( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  -  ( ( S  _D  ( F `
 N ) ) `
 C ) ) ) )  <  ( R  /  2 ) )
33754, 68, 69, 70,