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

Theorem ulmdvlem1 20269
Description: Lemma for ulmdv 20272. (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 452 . . . . 5  |-  ( (
ph  /\  ps )  ->  G : X --> CC )
3 ulmdvlem1.y . . . . 5  |-  ( (
ph  /\  ps )  ->  Y  e.  X )
42, 3ffvelrnd 5830 . . . 4  |-  ( (
ph  /\  ps )  ->  ( G `  Y
)  e.  CC )
5 ulmdvlem1.c . . . . 5  |-  ( (
ph  /\  ps )  ->  C  e.  X )
62, 5ffvelrnd 5830 . . . 4  |-  ( (
ph  /\  ps )  ->  ( G `  C
)  e.  CC )
74, 6subcld 9367 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( G `  Y )  -  ( G `  C )
)  e.  CC )
8 ulmdvlem1.n . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  N  e.  Z )
9 fveq2 5687 . . . . . . . . . . . . 13  |-  ( k  =  N  ->  ( F `  k )  =  ( F `  N ) )
109oveq2d 6056 . . . . . . . . . . . 12  |-  ( k  =  N  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  N )
) )
11 eqid 2404 . . . . . . . . . . . 12  |-  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  =  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )
12 ovex 6065 . . . . . . . . . . . 12  |-  ( S  _D  ( F `  N ) )  e. 
_V
1310, 11, 12fvmpt 5765 . . . . . . . . . . 11  |-  ( N  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  N
)  =  ( S  _D  ( F `  N ) ) )
148, 13syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  N
)  =  ( S  _D  ( F `  N ) ) )
15 ovex 6065 . . . . . . . . . . . . . . 15  |-  ( S  _D  ( F `  k ) )  e. 
_V
1615rgenw 2733 . . . . . . . . . . . . . 14  |-  A. k  e.  Z  ( S  _D  ( F `  k
) )  e.  _V
1711fnmpt 5530 . . . . . . . . . . . . . 14  |-  ( A. k  e.  Z  ( S  _D  ( F `  k ) )  e. 
_V  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) )  Fn  Z
)
1816, 17mp1i 12 . . . . . . . . . . . . 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 20253 . . . . . . . . . . . . 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 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
2221adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) : Z --> ( CC  ^m  X ) )
2322, 8ffvelrnd 5830 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `  N
)  e.  ( CC 
^m  X ) )
2414, 23eqeltrrd 2479 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( S  _D  ( F `  N )
)  e.  ( CC 
^m  X ) )
25 elmapi 6997 . . . . . . . . 9  |-  ( ( S  _D  ( F `
 N ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  N ) ) : X --> CC )
2624, 25syl 16 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( S  _D  ( F `  N )
) : X --> CC )
27 fdm 5554 . . . . . . . 8  |-  ( ( S  _D  ( F `
 N ) ) : X --> CC  ->  dom  ( S  _D  ( F `  N )
)  =  X )
2826, 27syl 16 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  dom  ( S  _D  ( F `  N ) )  =  X )
29 dvbsss 19742 . . . . . . 7  |-  dom  ( S  _D  ( F `  N ) )  C_  S
3028, 29syl6eqssr 3359 . . . . . 6  |-  ( (
ph  /\  ps )  ->  X  C_  S )
31 ulmdv.s . . . . . . . 8  |-  ( ph  ->  S  e.  { RR ,  CC } )
32 recnprss 19744 . . . . . . . 8  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
3331, 32syl 16 . . . . . . 7  |-  ( ph  ->  S  C_  CC )
3433adantr 452 . . . . . 6  |-  ( (
ph  /\  ps )  ->  S  C_  CC )
3530, 34sstrd 3318 . . . . 5  |-  ( (
ph  /\  ps )  ->  X  C_  CC )
3635, 3sseldd 3309 . . . 4  |-  ( (
ph  /\  ps )  ->  Y  e.  CC )
3735, 5sseldd 3309 . . . 4  |-  ( (
ph  /\  ps )  ->  C  e.  CC )
3836, 37subcld 9367 . . 3  |-  ( (
ph  /\  ps )  ->  ( Y  -  C
)  e.  CC )
39 ulmdvlem1.3 . . . 4  |-  ( (
ph  /\  ps )  ->  Y  =/=  C )
4036, 37, 39subne0d 9376 . . 3  |-  ( (
ph  /\  ps )  ->  ( Y  -  C
)  =/=  0 )
417, 38, 40divcld 9746 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  e.  CC )
42 ulmcl 20250 . . . . 5  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  H : X --> CC )
4319, 42syl 16 . . . 4  |-  ( ph  ->  H : X --> CC )
4443adantr 452 . . 3  |-  ( (
ph  /\  ps )  ->  H : X --> CC )
4544, 5ffvelrnd 5830 . 2  |-  ( (
ph  /\  ps )  ->  ( H `  C
)  e.  CC )
4626, 5ffvelrnd 5830 . 2  |-  ( (
ph  /\  ps )  ->  ( ( S  _D  ( F `  N ) ) `  C )  e.  CC )
47 ulmdvlem1.r . . 3  |-  ( (
ph  /\  ps )  ->  R  e.  RR+ )
4847rpred 10604 . 2  |-  ( (
ph  /\  ps )  ->  R  e.  RR )
4941, 46subcld 9367 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ( ( G `  Y )  -  ( G `  C ) )  / 
( Y  -  C
) )  -  (
( S  _D  ( F `  N )
) `  C )
)  e.  CC )
5049abscld 12193 . . 3  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( S  _D  ( F `  N ) ) `  C ) ) )  e.  RR )
51 ulmdv.f . . . . . . . . . . . 12  |-  ( ph  ->  F : Z --> ( CC 
^m  X ) )
5251adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  F : Z --> ( CC 
^m  X ) )
5352, 8ffvelrnd 5830 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( F `  N
)  e.  ( CC 
^m  X ) )
54 elmapi 6997 . . . . . . . . . 10  |-  ( ( F `  N )  e.  ( CC  ^m  X )  ->  ( F `  N ) : X --> CC )
5553, 54syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( F `  N
) : X --> CC )
5655, 3ffvelrnd 5830 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( ( F `  N ) `  Y
)  e.  CC )
5755, 5ffvelrnd 5830 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( ( F `  N ) `  C
)  e.  CC )
5856, 57subcld 9367 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  e.  CC )
5958, 38, 40divcld 9746 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  e.  CC )
6041, 59subcld 9367 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( ( ( G `  Y )  -  ( G `  C ) )  / 
( Y  -  C
) )  -  (
( ( ( F `
 N ) `  Y )  -  (
( F `  N
) `  C )
)  /  ( Y  -  C ) ) )  e.  CC )
6160abscld 12193 . . . 4  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  e.  RR )
6259, 46subcld 9367 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) )  -  (
( S  _D  ( F `  N )
) `  C )
)  e.  CC )
6362abscld 12193 . . . 4  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  -  ( ( S  _D  ( F `
 N ) ) `
 C ) ) )  e.  RR )
6461, 63readdcld 9071 . . 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 )
6548rehalfcld 10170 . . 3  |-  ( (
ph  /\  ps )  ->  ( R  /  2
)  e.  RR )
6641, 46, 59abs3difd 12217 . . 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 ) ) ) ) )
6765rehalfcld 10170 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ( R  / 
2 )  /  2
)  e.  RR )
684, 56, 6, 57sub4d 9416 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) )  =  ( ( ( G `  Y
)  -  ( G `
 C ) )  -  ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) ) ) )
6968oveq1d 6055 . . . . . . . . 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 ) ) )
707, 58, 38, 40divsubdird 9785 . . . . . . . . 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
) ) ) )
7169, 70eqtrd 2436 . . . . . . . 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
) ) ) )
7271fveq2d 5691 . . . . . . 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 ) ) ) ) )
734, 56subcld 9367 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( G `  Y )  -  (
( F `  N
) `  Y )
)  e.  CC )
746, 57subcld 9367 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( G `  C )  -  (
( F `  N
) `  C )
)  e.  CC )
7573, 74subcld 9367 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( ( ( G `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( G `  C
)  -  ( ( F `  N ) `
 C ) ) )  e.  CC )
7675, 38, 40absdivd 12212 . . . . . . 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 )
) ) )
7772, 76eqtr3d 2438 . . . . . 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 ) ) ) )
78 eqid 2404 . . . . . . . 8  |-  ( ZZ>= `  N )  =  (
ZZ>= `  N )
79 ulmdv.z . . . . . . . . . 10  |-  Z  =  ( ZZ>= `  M )
808, 79syl6eleq 2494 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  N  e.  ( ZZ>= `  M ) )
81 eluzelz 10452 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
8280, 81syl 16 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  N  e.  ZZ )
83 ulmdv.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ZZ )
8483adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  M  e.  ZZ )
85 ulmdv.l . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  X )  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  ~~>  ( G `  z ) )
8685ralrimiva 2749 . . . . . . . . . . . . 13  |-  ( ph  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
8786adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z ) )
88 fveq2 5687 . . . . . . . . . . . . . . 15  |-  ( z  =  Y  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  Y ) )
8988mpteq2dv 4256 . . . . . . . . . . . . . 14  |-  ( z  =  Y  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 Y ) ) )
90 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( z  =  Y  ->  ( G `  z )  =  ( G `  Y ) )
9189, 90breq12d 4185 . . . . . . . . . . . . 13  |-  ( z  =  Y  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 Y ) )  ~~>  ( G `  Y
) ) )
9291rspcv 3008 . . . . . . . . . . . 12  |-  ( Y  e.  X  ->  ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  -> 
( k  e.  Z  |->  ( ( F `  k ) `  Y
) )  ~~>  ( G `
 Y ) ) )
933, 87, 92sylc 58 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  Y
) )  ~~>  ( G `
 Y ) )
94 fvex 5701 . . . . . . . . . . . . . 14  |-  ( ZZ>= `  M )  e.  _V
9579, 94eqeltri 2474 . . . . . . . . . . . . 13  |-  Z  e. 
_V
9695mptex 5925 . . . . . . . . . . . 12  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  Y )  -  ( ( F `
 N ) `  Y ) ) )  e.  _V
9796a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
) )  e.  _V )
98 fveq2 5687 . . . . . . . . . . . . . . 15  |-  ( k  =  n  ->  ( F `  k )  =  ( F `  n ) )
9998fveq1d 5689 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( F `  k
) `  Y )  =  ( ( F `
 n ) `  Y ) )
100 eqid 2404 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( F `  k ) `
 Y ) )  =  ( k  e.  Z  |->  ( ( F `
 k ) `  Y ) )
101 fvex 5701 . . . . . . . . . . . . . 14  |-  ( ( F `  n ) `
 Y )  e. 
_V
10299, 100, 101fvmpt 5765 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  Y
) ) `  n
)  =  ( ( F `  n ) `
 Y ) )
103102adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  Y )
) `  n )  =  ( ( F `
 n ) `  Y ) )
10452ffvelrnda 5829 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( F `  n )  e.  ( CC  ^m  X ) )
105 elmapi 6997 . . . . . . . . . . . . . 14  |-  ( ( F `  n )  e.  ( CC  ^m  X )  ->  ( F `  n ) : X --> CC )
106104, 105syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( F `  n ) : X --> CC )
1073adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  Y  e.  X )
108106, 107ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  n ) `  Y )  e.  CC )
109103, 108eqeltrd 2478 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  Y )
) `  n )  e.  CC )
11099oveq1d 6055 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
111 eqid 2404 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  Y )  -  ( ( F `
 N ) `  Y ) ) )  =  ( k  e.  Z  |->  ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
112 ovex 6065 . . . . . . . . . . . . . 14  |-  ( ( ( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) )  e. 
_V
113110, 111, 112fvmpt 5765 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
) ) `  n
)  =  ( ( ( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) ) )
114113adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) ) ) `  n )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
115103oveq1d 6055 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( k  e.  Z  |->  ( ( F `  k ) `  Y
) ) `  n
)  -  ( ( F `  N ) `
 Y ) )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
116114, 115eqtr4d 2439 . . . . . . . . . . 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 ) ) )
11779, 84, 93, 56, 97, 109, 116climsubc1 12386 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
) )  ~~>  ( ( G `  Y )  -  ( ( F `
 N ) `  Y ) ) )
11895mptex 5925 . . . . . . . . . . 11  |-  ( k  e.  Z  |->  ( ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  k ) `
 C )  -  ( ( F `  N ) `  C
) ) ) )  e.  _V
119118a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  e.  _V )
120 fveq2 5687 . . . . . . . . . . . . . . 15  |-  ( z  =  C  ->  (
( F `  k
) `  z )  =  ( ( F `
 k ) `  C ) )
121120mpteq2dv 4256 . . . . . . . . . . . . . 14  |-  ( z  =  C  ->  (
k  e.  Z  |->  ( ( F `  k
) `  z )
)  =  ( k  e.  Z  |->  ( ( F `  k ) `
 C ) ) )
122 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( z  =  C  ->  ( G `  z )  =  ( G `  C ) )
123121, 122breq12d 4185 . . . . . . . . . . . . 13  |-  ( z  =  C  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  <->  ( k  e.  Z  |->  ( ( F `  k ) `
 C ) )  ~~>  ( G `  C
) ) )
124123rspcv 3008 . . . . . . . . . . . 12  |-  ( C  e.  X  ->  ( A. z  e.  X  ( k  e.  Z  |->  ( ( F `  k ) `  z
) )  ~~>  ( G `
 z )  -> 
( k  e.  Z  |->  ( ( F `  k ) `  C
) )  ~~>  ( G `
 C ) ) )
1255, 87, 124sylc 58 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( F `  k ) `  C
) )  ~~>  ( G `
 C ) )
12695mptex 5925 . . . . . . . . . . . 12  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) )  e.  _V
127126a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) )  e.  _V )
12898fveq1d 5689 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( F `  k
) `  C )  =  ( ( F `
 n ) `  C ) )
129 eqid 2404 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( F `  k ) `
 C ) )  =  ( k  e.  Z  |->  ( ( F `
 k ) `  C ) )
130 fvex 5701 . . . . . . . . . . . . . 14  |-  ( ( F `  n ) `
 C )  e. 
_V
131128, 129, 130fvmpt 5765 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( F `  k ) `  C
) ) `  n
)  =  ( ( F `  n ) `
 C ) )
132131adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  C )
) `  n )  =  ( ( F `
 n ) `  C ) )
1335adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  C  e.  X )
134106, 133ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  n ) `  C )  e.  CC )
135132, 134eqeltrd 2478 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( F `  k
) `  C )
) `  n )  e.  CC )
136128oveq1d 6055 . . . . . . . . . . . . . 14  |-  ( k  =  n  ->  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
137 eqid 2404 . . . . . . . . . . . . . 14  |-  ( k  e.  Z  |->  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) )  =  ( k  e.  Z  |->  ( ( ( F `  k ) `
 C )  -  ( ( F `  N ) `  C
) ) )
138 ovex 6065 . . . . . . . . . . . . . 14  |-  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) )  e. 
_V
139136, 137, 138fvmpt 5765 . . . . . . . . . . . . 13  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) ) `  n
)  =  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) )
140139adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) `  n )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
141132oveq1d 6055 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( k  e.  Z  |->  ( ( F `  k ) `  C
) ) `  n
)  -  ( ( F `  N ) `
 C ) )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
142140, 141eqtr4d 2439 . . . . . . . . . . 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 ) ) )
14379, 84, 125, 57, 127, 135, 142climsubc1 12386 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( ( ( F `
 k ) `  C )  -  (
( F `  N
) `  C )
) )  ~~>  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) )
14456adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  N ) `  Y )  e.  CC )
145108, 144subcld 9367 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( F `  n
) `  Y )  -  ( ( F `
 N ) `  Y ) )  e.  CC )
146114, 145eqeltrd 2478 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  Y
)  -  ( ( F `  N ) `
 Y ) ) ) `  n )  e.  CC )
14757adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( ( F `  N ) `  C )  e.  CC )
148134, 147subcld 9367 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) )  e.  CC )
149140, 148eqeltrd 2478 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) `  n )  e.  CC )
150110, 136oveq12d 6058 . . . . . . . . . . . . 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 )
) ) )
151 eqid 2404 . . . . . . . . . . . . 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 )
) ) )
152 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )  e. 
_V
153150, 151, 152fvmpt 5765 . . . . . . . . . . . 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
) ) ) )
154153adantl 453 . . . . . . . . . . 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 )
) ) )
155114, 140oveq12d 6058 . . . . . . . . . . 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
) ) ) )
156154, 155eqtr4d 2439 . . . . . . . . . 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 ) ) )
15779, 84, 117, 119, 143, 146, 149, 156climsub 12382 . . . . . . . . 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
) ) ) )
15895mptex 5925 . . . . . . . . . 10  |-  ( k  e.  Z  |->  ( abs `  ( ( ( ( F `  k ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  k ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) ) )  e. 
_V
159158a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( k  e.  Z  |->  ( abs `  (
( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) )  e.  _V )
160145, 148subcld 9367 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
( ( F `  n ) `  Y
)  -  ( ( F `  N ) `
 Y ) )  -  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )  e.  CC )
161154, 160eqeltrd 2478 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( (
k  e.  Z  |->  ( ( ( ( F `
 k ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  k
) `  C )  -  ( ( F `
 N ) `  C ) ) ) ) `  n )  e.  CC )
162150fveq2d 5691 . . . . . . . . . . . 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 ) ) ) ) )
163 eqid 2404 . . . . . . . . . . . 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 ) ) ) ) )
164 fvex 5701 . . . . . . . . . . . 12  |-  ( abs `  ( ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  n ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  e.  _V
165162, 163, 164fvmpt 5765 . . . . . . . . . . 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 ) ) ) ) )
166165adantl 453 . . . . . . . . . 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 ) ) ) ) )
167154fveq2d 5691 . . . . . . . . . 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 ) ) ) ) )
168166, 167eqtr4d 2439 . . . . . . . . 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
) ) )
16979, 157, 159, 84, 161, 168climabs 12352 . . . . . . . 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 ) ) ) ) )
17038abscld 12193 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  e.  RR )
17167, 170remulcld 9072 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) )  e.  RR )
172171recnd 9070 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) )  e.  CC )
17379eqimss2i 3363 . . . . . . . . . 10  |-  ( ZZ>= `  M )  C_  Z
174173, 95climconst2 12297 . . . . . . . . 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 ) ) ) )
175172, 84, 174syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( Z  X.  {
( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) } )  ~~>  ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
17679uztrn2 10459 . . . . . . . . . . 11  |-  ( ( N  e.  Z  /\  n  e.  ( ZZ>= `  N ) )  ->  n  e.  Z )
1778, 176sylan 458 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  n  e.  Z
)
178177, 165syl 16 . . . . . . . . 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
) ) ) ) )
179160abscld 12193 . . . . . . . . . 10  |-  ( ( ( ph  /\  ps )  /\  n  e.  Z
)  ->  ( abs `  ( ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) )  -  (
( ( F `  n ) `  C
)  -  ( ( F `  N ) `
 C ) ) ) )  e.  RR )
180177, 179syldan 457 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( abs `  (
( ( ( F `
 n ) `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( ( F `  n
) `  C )  -  ( ( F `
 N ) `  C ) ) ) )  e.  RR )
181178, 180eqeltrd 2478 . . . . . . . 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 )
182 ovex 6065 . . . . . . . . . . 11  |-  ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) )  e.  _V
183182fvconst2 5906 . . . . . . . . . 10  |-  ( n  e.  Z  ->  (
( Z  X.  {
( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) } ) `  n
)  =  ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
184177, 183syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( Z  X.  { ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) } ) `
 n )  =  ( ( ( R  /  2 )  / 
2 )  x.  ( abs `  ( Y  -  C ) ) ) )
185171adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( R  /  2 )  /  2 )  x.  ( abs `  ( Y  -  C )
) )  e.  RR )
186184, 185eqeltrd 2478 . . . . . . . 8  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( Z  X.  { ( ( ( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) } ) `
 n )  e.  RR )
187177, 106syldan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  n ) : X --> CC )
188 ffn 5550 . . . . . . . . . . . . . 14  |-  ( ( F `  n ) : X --> CC  ->  ( F `  n )  Fn  X )
189187, 188syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  n )  Fn  X
)
19055adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  N ) : X --> CC )
191 ffn 5550 . . . . . . . . . . . . . 14  |-  ( ( F `  N ) : X --> CC  ->  ( F `  N )  Fn  X )
192190, 191syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  N )  Fn  X
)
193 ulmscl 20248 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  Z  |->  ( S  _D  ( F `
 k ) ) ) ( ~~> u `  X ) H  ->  X  e.  _V )
19419, 193syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  e.  _V )
195194ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  X  e.  _V )
1963adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  Y  e.  X
)
197 fnfvof 6276 . . . . . . . . . . . . 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 )
) )
198189, 192, 195, 196, 197syl22anc 1185 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( F `  n )  o F  -  ( F `  N )
) `  Y )  =  ( ( ( F `  n ) `
 Y )  -  ( ( F `  N ) `  Y
) ) )
1995adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  C  e.  X
)
200 fnfvof 6276 . . . . . . . . . . . . 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 )
) )
201189, 192, 195, 199, 200syl22anc 1185 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( ( F `  n )  o F  -  ( F `  N )
) `  C )  =  ( ( ( F `  n ) `
 C )  -  ( ( F `  N ) `  C
) ) )
202198, 201oveq12d 6058 . . . . . . . . . . 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
) ) ) )
203202fveq2d 5691 . . . . . . . . . 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 ) ) ) ) )
20430, 3sseldd 3309 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ps )  ->  Y  e.  S )
20530, 5sseldd 3309 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ps )  ->  C  e.  S )
206204, 205ovresd 6173 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S
) ) C )  =  ( Y ( abs  o.  -  ) C ) )
207 eqid 2404 . . . . . . . . . . . . . . . . . 18  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
208207cnmetdval 18758 . . . . . . . . . . . . . . . . 17  |-  ( ( Y  e.  CC  /\  C  e.  CC )  ->  ( Y ( abs 
o.  -  ) C
)  =  ( abs `  ( Y  -  C
) ) )
20936, 37, 208syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  ( Y ( abs 
o.  -  ) C
)  =  ( abs `  ( Y  -  C
) ) )
210206, 209eqtrd 2436 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S
) ) C )  =  ( abs `  ( Y  -  C )
) )
211 ulmdvlem1.a . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  <  U )
212210, 211eqbrtrd 4192 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S
) ) C )  <  U )
213 cnxmet 18760 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
214 xmetres2 18344 . . . . . . . . . . . . . . . 16  |-  ( ( ( abs  o.  -  )  e.  ( * Met `  CC )  /\  S  C_  CC )  -> 
( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S ) )
215213, 34, 214sylancr 645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ( ( abs  o.  -  )  |`  ( S  X.  S ) )  e.  ( * Met `  S ) )
216 ulmdvlem1.u . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  U  e.  RR+ )
217216rpxrd 10605 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  U  e.  RR* )
218 elbl3 18375 . . . . . . . . . . . . . . 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
) )
219215, 217, 205, 204, 218syl22anc 1185 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  ( Y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )  <->  ( Y ( ( abs  o.  -  )  |`  ( S  X.  S ) ) C )  <  U ) )
220212, 219mpbird 224 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  Y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
221220adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  Y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
222 blcntr 18396 . . . . . . . . . . . . . 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 ) )
223215, 205, 216, 222syl3anc 1184 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  C  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
224223adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  C  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )
225221, 224jca 519 . . . . . . . . . . 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 ) ) )
22631ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  S  e.  { RR ,  CC } )
227 eqid 2404 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  |`  ( S  X.  S
) )  =  ( ( abs  o.  -  )  |`  ( S  X.  S ) )
22830adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  X  C_  S
)
229187ffvelrnda 5829 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  n
) `  y )  e.  CC )
230190ffvelrnda 5829 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  N
) `  y )  e.  CC )
231229, 230subcld 9367 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( ( F `  n ) `  y
)  -  ( ( F `  N ) `
 y ) )  e.  CC )
232 eqid 2404 . . . . . . . . . . . . . 14  |-  ( y  e.  X  |->  ( ( ( F `  n
) `  y )  -  ( ( F `
 N ) `  y ) ) )  =  ( y  e.  X  |->  ( ( ( F `  n ) `
 y )  -  ( ( F `  N ) `  y
) ) )
233231, 232fmptd 5852 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( y  e.  X  |->  ( ( ( F `  n ) `
 y )  -  ( ( F `  N ) `  y
) ) ) : X --> CC )
234 fvex 5701 . . . . . . . . . . . . . . . 16  |-  ( ( F `  n ) `
 y )  e. 
_V
235234a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  n
) `  y )  e.  _V )
236 fvex 5701 . . . . . . . . . . . . . . . 16  |-  ( ( F `  N ) `
 y )  e. 
_V
237236a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( F `  N
) `  y )  e.  _V )
238187feqmptd 5738 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  n )  =  ( y  e.  X  |->  ( ( F `  n
) `  y )
) )
239190feqmptd 5738 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( F `  N )  =  ( y  e.  X  |->  ( ( F `  N
) `  y )
) )
240195, 235, 237, 238, 239offval2 6281 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( F `
 n )  o F  -  ( F `
 N ) )  =  ( y  e.  X  |->  ( ( ( F `  n ) `
 y )  -  ( ( F `  N ) `  y
) ) ) )
241240feq1d 5539 . . . . . . . . . . . . 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 ) )
242233, 241mpbird 224 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( F `
 n )  o F  -  ( F `
 N ) ) : X --> CC )
243205adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  C  e.  S
)
244217adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  U  e.  RR* )
245 eqid 2404 . . . . . . . . . . . 12  |-  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )  =  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )
246 ulmdvlem1.b . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  ( C ( ball `  ( ( abs  o.  -  )  |`  ( S  X.  S ) ) ) U )  C_  X )
247246adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( C (
ball `  ( ( abs  o.  -  )  |`  ( S  X.  S
) ) ) U )  C_  X )
248240oveq2d 6056 . . . . . . . . . . . . . . . 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 )
) ) ) )
249 fvex 5701 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  _D  ( F `
 n ) ) `
 y )  e. 
_V
250249a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  n )
) `  y )  e.  _V )
251238oveq2d 6056 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) )  =  ( S  _D  ( y  e.  X  |->  ( ( F `
 n ) `  y ) ) ) )
25298oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  n  ->  ( S  _D  ( F `  k ) )  =  ( S  _D  ( F `  n )
) )
253 ovex 6065 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S  _D  ( F `  n ) )  e. 
_V
254252, 11, 253fvmpt 5765 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  Z  ->  (
( k  e.  Z  |->  ( S  _D  ( F `  k )
) ) `  n
)  =  ( S  _D  ( F `  n ) ) )
255177, 254syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 n )  =  ( S  _D  ( F `  n )
) )
25621ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) : Z --> ( CC  ^m  X ) )
257256, 177ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( k  e.  Z  |->  ( S  _D  ( F `  k ) ) ) `
 n )  e.  ( CC  ^m  X
) )
258255, 257eqeltrrd 2479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) )  e.  ( CC 
^m  X ) )
259 elmapi 6997 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( S  _D  ( F `
 n ) )  e.  ( CC  ^m  X )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
260258, 259syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) ) : X --> CC )
261260feqmptd 5738 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  n ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `
 n ) ) `
 y ) ) )
262251, 261eqtr3d 2438 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( y  e.  X  |->  ( ( F `  n ) `  y
) ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `  n ) ) `  y ) ) )
263 fvex 5701 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  _D  ( F `
 N ) ) `
 y )  e. 
_V
264263a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  N )
) `  y )  e.  _V )
265239oveq2d 6056 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  N ) )  =  ( S  _D  ( y  e.  X  |->  ( ( F `
 N ) `  y ) ) ) )
26626adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  N ) ) : X --> CC )
267266feqmptd 5738 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( F `  N ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `
 N ) ) `
 y ) ) )
268265, 267eqtr3d 2438 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( S  _D  ( y  e.  X  |->  ( ( F `  N ) `  y
) ) )  =  ( y  e.  X  |->  ( ( S  _D  ( F `  N ) ) `  y ) ) )
269226, 229, 250, 262, 230, 264, 268dvmptsub 19806 . . . . . . . . . . . . . . . 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 )
) ) )
270248, 269eqtrd 2436 . . . . . . . . . . . . . . 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 ) ) ) )
271270dmeqd 5031 . . . . . . . . . . . . . 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 ) ) ) )
272 ovex 6065 . . . . . . . . . . . . . . 15  |-  ( ( ( S  _D  ( F `  n )
) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) )  e. 
_V
273 eqid 2404 . . . . . . . . . . . . . . 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 ) ) )
274272, 273dmmpti 5533 . . . . . . . . . . . . . 14  |-  dom  (
y  e.  X  |->  ( ( ( S  _D  ( F `  n ) ) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  =  X
275271, 274syl6eq 2452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  dom  ( S  _D  ( ( F `  n )  o F  -  ( F `  N ) ) )  =  X )
276247, 275sseqtr4d 3345 . . . . . . . . . . . 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 ) ) ) )
27767adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ps )  /\  n  e.  (
ZZ>= `  N ) )  ->  ( ( R  /  2 )  / 
2 )  e.  RR )
278247sselda 3308 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  ( C ( ball `  (
( abs  o.  -  )  |`  ( S  X.  S
) ) ) U ) )  ->  y  e.  X )
279270fveq1d 5689 . . . . . . . . . . . . . . . 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 ) )
280273fvmpt2 5771 . . . . . . . . . . . . . . . . 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 ) ) )
281272, 280mpan2 653 . . . . . . . . . . . . . . . 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 ) ) )
282279, 281sylan9eq 2456 . . . . . . . . . . . . . . 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 ) ) )
283282fveq2d 5691 . . . . . . . . . . . . . 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 )
) ) )
284272a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( ( S  _D  ( F `  n ) ) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) )  e. 
_V )
285226, 231, 284, 269dvmptcl 19798 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( ( S  _D  ( F `  n ) ) `  y )  -  ( ( S  _D  ( F `  N ) ) `  y ) )  e.  CC )
286285abscld 12193 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  e.  RR )
28767ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( R  /  2
)  /  2 )  e.  RR )
288260ffvelrnda 5829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  n )
) `  y )  e.  CC )
289266ffvelrnda 5829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  (
( S  _D  ( F `  N )
) `  y )  e.  CC )
290288, 289abssubd 12210 . . . . . . . . . . . . . . . 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 ) ) ) )
291 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 ) )
292 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  =  n  ->  ( F `  m )  =  ( F `  n ) )
293292oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  =  n  ->  ( S  _D  ( F `  m ) )  =  ( S  _D  ( F `  n )
) )
294293fveq1d 5689 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  =  n  ->  (
( S  _D  ( F `  m )
) `  x )  =  ( ( S  _D  ( F `  n ) ) `  x ) )
295294oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  n  ->  (
( ( S  _D  ( F `  N ) ) `  x )  -  ( ( S  _D  ( F `  m ) ) `  x ) )  =  ( ( ( S  _D  ( F `  N ) ) `  x )  -  (
( S  _D  ( F `  n )
) `  x )
) )
296295fveq2d 5691 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
297296breq1d 4182 . . . . . . . . . . . . . . . . . . . 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 ) ) )
298297ralbidv 2686 . . . . . . . . . . . . . . . . . . 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 ) ) )
299298rspccva 3011 . . . . . . . . . . . . . . . . . 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 ) )
300291, 299sylan 458 . . . . . . . . . . . . . . . . 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 ) )
301 fveq2 5687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( S  _D  ( F `  N )
) `  x )  =  ( ( S  _D  ( F `  N ) ) `  y ) )
302 fveq2 5687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
( S  _D  ( F `  n )
) `  x )  =  ( ( S  _D  ( F `  n ) ) `  y ) )
303301, 302oveq12d 6058 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
( ( S  _D  ( F `  N ) ) `  x )  -  ( ( S  _D  ( F `  n ) ) `  x ) )  =  ( ( ( S  _D  ( F `  N ) ) `  y )  -  (
( S  _D  ( F `  n )
) `  y )
) )
304303fveq2d 5691 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
305304breq1d 4182 . . . . . . . . . . . . . . . . . 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 ) ) )
306305rspccva 3011 . . . . . . . . . . . . . . . . 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 ) )
307300, 306sylan 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 N ) ) `
 y )  -  ( ( S  _D  ( F `  n ) ) `  y ) ) )  <  (
( R  /  2
)  /  2 ) )
308290, 307eqbrtrd 4192 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  <  (
( R  /  2
)  /  2 ) )
309286, 287, 308ltled 9177 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( ( S  _D  ( F `
 n ) ) `
 y )  -  ( ( S  _D  ( F `  N ) ) `  y ) ) )  <_  (
( R  /  2
)  /  2 ) )
310283, 309eqbrtrd 4192 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ps )  /\  n  e.  ( ZZ>= `  N )
)  /\  y  e.  X )  ->  ( abs `  ( ( S  _D  ( ( F `
 n )  o F  -  ( F `
 N ) ) ) `  y ) )  <_  ( ( R  /  2 )  / 
2 ) )
311278, 310syldan 457 . . . . . . . . . . . 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 ) )
312226, 227, 228, 242, 243, 244, 245, 276, 277, 311dvlip2 19832 . . . . . . . . . . 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 )
) ) )
313225, 312mpdan 650 . . . . . . . . . 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 )
) ) )
314203, 313eqbrtrrd 4194 . . . . . . . . 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 )
) ) )
315314, 178, 1843brtr4d 4202 . . . . . . . 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
) )
31678, 82, 169, 175, 181, 186, 315climle 12388 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( G `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) ) )  <_  ( (
( R  /  2
)  /  2 )  x.  ( abs `  ( Y  -  C )
) ) )
31775abscld 12193 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( G `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) ) )  e.  RR )
31838, 40absrpcld 12205 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  e.  RR+ )
319317, 67, 318ledivmul2d 10654 . . . . . . 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
) ) ) ) )
320316, 319mpbird 224 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( abs `  (
( ( G `  Y )  -  (
( F `  N
) `  Y )
)  -  ( ( G `  C )  -  ( ( F `
 N ) `  C ) ) ) )  /  ( abs `  ( Y  -  C
) ) )  <_ 
( ( R  / 
2 )  /  2
) )
32177, 320eqbrtrd 4192 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( ( ( F `  N
) `  Y )  -  ( ( F `
 N ) `  C ) )  / 
( Y  -  C
) ) ) )  <_  ( ( R  /  2 )  / 
2 ) )
322216rpred 10604 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  U  e.  RR )
323 ulmdvlem1.v . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  W  e.  RR+ )
324323rpred 10604 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  W  e.  RR )
325 ulmdvlem1.l . . . . . . 7  |-  ( (
ph  /\  ps )  ->  U  <  W )
326170, 322, 324, 211, 325lttrd 9187 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( abs `  ( Y  -  C )
)  <  W )
327 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 ) ) )
328326, 327mpd 15 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( ( F `  N ) `
 Y )  -  ( ( F `  N ) `  C
) )  /  ( Y  -  C )
)  -  ( ( S  _D  ( F `
 N ) ) `
 C ) ) )  <  ( ( R  /  2 )  /  2 ) )
32961, 63, 67, 67, 321, 328leltaddd 9603 . . . 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 ) ) )
33065recnd 9070 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( R  /  2
)  e.  CC )
3313302halvesd 10169 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ( R  /  2 )  / 
2 )  +  ( ( R  /  2
)  /  2 ) )  =  ( R  /  2 ) )
332329, 331breqtrd 4196 . . 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 ) )
33350, 64, 65, 66, 332lelttrd 9184 . 2  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( ( S  _D  ( F `  N ) ) `  C ) ) )  <  ( R  / 
2 ) )
334 ulmdvlem1.2 . 2  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( S  _D  ( F `  N ) ) `  C )  -  ( H `  C ) ) )  <  ( R  / 
2 ) )
33541, 45, 46, 48, 333, 334abs3lemd 12218 1  |-  ( (
ph  /\  ps )  ->  ( abs `  (
( ( ( G `
 Y )  -  ( G `  C ) )  /  ( Y  -  C ) )  -  ( H `  C ) ) )  <  R )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb