Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem29 Structured version   Visualization version   Unicode version

Theorem poimirlem29 31981
Description: Lemma for poimir 31985 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimir.i  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
poimir.r  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
poimir.1  |-  ( ph  ->  F  e.  ( ( Rt  I )  Cn  R
) )
poimirlem30.x  |-  X  =  ( ( F `  ( ( ( 1st `  ( G `  k
) )  oF  +  ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  n )
poimirlem30.2  |-  ( ph  ->  G : NN --> ( ( NN0  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
poimirlem30.3  |-  ( (
ph  /\  k  e.  NN )  ->  ran  ( 1st `  ( G `  k ) )  C_  ( 0..^ k ) )
poimirlem30.4  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
)  /\  r  e.  {  <_  ,  `'  <_  } ) )  ->  E. j  e.  ( 0 ... N
) 0 r X )
Assertion
Ref Expression
poimirlem29  |-  ( ph  ->  ( A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  ->  A. n  e.  (
1 ... N ) A. v  e.  ( Rt  I
) ( C  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
) ) )
Distinct variable groups:    f, i,
j, k, m, n, z    ph, j, m, n   
j, F, m, n   
j, N, m, n    ph, i, k    f, N, i, k    ph, z    f, F, k, z    z, N    C, i, k, m, n, z    i, r, v, j, k, m, n, z, ph    f, r, v    i, F, r, v    f, G, i, j, k, m, n, r, v, z    f, I, i, j, k, m, n, r, v, z    N, r, v    R, f, i, j, k, m, n, r, v, z   
f, X, i, m, r, v, z    C, f, j, v
Allowed substitution hints:    ph( f)    C( r)    X( j, k, n)

Proof of Theorem poimirlem29
Dummy variable  c is distinct from all other variables.
StepHypRef Expression
1 poimir.r . . . . . . . . . . . 12  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
2 fzfi 12192 . . . . . . . . . . . . 13  |-  ( 1 ... N )  e. 
Fin
3 retop 21794 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
43fconst6 5778 . . . . . . . . . . . . 13  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
5 pttop 20609 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top )  ->  ( Xt_ `  ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )  e.  Top )
62, 4, 5mp2an 679 . . . . . . . . . . . 12  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) )  e. 
Top
71, 6eqeltri 2527 . . . . . . . . . . 11  |-  R  e. 
Top
8 poimir.i . . . . . . . . . . . 12  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
9 ovex 6323 . . . . . . . . . . . 12  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  e. 
_V
108, 9eqeltri 2527 . . . . . . . . . . 11  |-  I  e. 
_V
11 elrest 15338 . . . . . . . . . . 11  |-  ( ( R  e.  Top  /\  I  e.  _V )  ->  ( v  e.  ( Rt  I )  <->  E. z  e.  R  v  =  ( z  i^i  I
) ) )
127, 10, 11mp2an 679 . . . . . . . . . 10  |-  ( v  e.  ( Rt  I )  <->  E. z  e.  R  v  =  ( z  i^i  I ) )
13 eqid 2453 . . . . . . . . . . . . . 14  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
141, 13ptrecube 31952 . . . . . . . . . . . . 13  |-  ( ( z  e.  R  /\  C  e.  z )  ->  E. c  e.  RR+  X_ m  e.  ( 1 ... N ) ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  C_  z )
1514ex 436 . . . . . . . . . . . 12  |-  ( z  e.  R  ->  ( C  e.  z  ->  E. c  e.  RR+  X_ m  e.  ( 1 ... N
) ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  C_  z )
)
16 inss1 3654 . . . . . . . . . . . . . . 15  |-  ( z  i^i  I )  C_  z
17 sseq1 3455 . . . . . . . . . . . . . . 15  |-  ( v  =  ( z  i^i  I )  ->  (
v  C_  z  <->  ( z  i^i  I )  C_  z
) )
1816, 17mpbiri 237 . . . . . . . . . . . . . 14  |-  ( v  =  ( z  i^i  I )  ->  v  C_  z )
1918sseld 3433 . . . . . . . . . . . . 13  |-  ( v  =  ( z  i^i  I )  ->  ( C  e.  v  ->  C  e.  z ) )
20 ssrin 3659 . . . . . . . . . . . . . . 15  |-  ( X_ m  e.  ( 1 ... N ) ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  C_  z  ->  (
X_ m  e.  ( 1 ... N ) ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) c )  i^i  I )  C_  (
z  i^i  I )
)
21 sseq2 3456 . . . . . . . . . . . . . . 15  |-  ( v  =  ( z  i^i  I )  ->  (
( X_ m  e.  ( 1 ... N ) ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) c )  i^i  I )  C_  v  <->  (
X_ m  e.  ( 1 ... N ) ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) c )  i^i  I )  C_  (
z  i^i  I )
) )
2220, 21syl5ibr 225 . . . . . . . . . . . . . 14  |-  ( v  =  ( z  i^i  I )  ->  ( X_ m  e.  ( 1 ... N ) ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  C_  z  ->  (
X_ m  e.  ( 1 ... N ) ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) c )  i^i  I )  C_  v
) )
2322reximdv 2863 . . . . . . . . . . . . 13  |-  ( v  =  ( z  i^i  I )  ->  ( E. c  e.  RR+  X_ m  e.  ( 1 ... N
) ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  C_  z  ->  E. c  e.  RR+  ( X_ m  e.  ( 1 ... N ) ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  i^i  I ) 
C_  v ) )
2419, 23imim12d 77 . . . . . . . . . . . 12  |-  ( v  =  ( z  i^i  I )  ->  (
( C  e.  z  ->  E. c  e.  RR+  X_ m  e.  ( 1 ... N ) ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  C_  z )  ->  ( C  e.  v  ->  E. c  e.  RR+  ( X_ m  e.  ( 1 ... N ) ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) c )  i^i  I )  C_  v
) ) )
2515, 24syl5com 31 . . . . . . . . . . 11  |-  ( z  e.  R  ->  (
v  =  ( z  i^i  I )  -> 
( C  e.  v  ->  E. c  e.  RR+  ( X_ m  e.  ( 1 ... N ) ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) c )  i^i  I )  C_  v
) ) )
2625rexlimiv 2875 . . . . . . . . . 10  |-  ( E. z  e.  R  v  =  ( z  i^i  I )  ->  ( C  e.  v  ->  E. c  e.  RR+  ( X_ m  e.  ( 1 ... N ) ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  i^i  I ) 
C_  v ) )
2712, 26sylbi 199 . . . . . . . . 9  |-  ( v  e.  ( Rt  I )  ->  ( C  e.  v  ->  E. c  e.  RR+  ( X_ m  e.  ( 1 ... N
) ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  i^i  I ) 
C_  v ) )
2827imp 431 . . . . . . . 8  |-  ( ( v  e.  ( Rt  I )  /\  C  e.  v )  ->  E. c  e.  RR+  ( X_ m  e.  ( 1 ... N
) ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  i^i  I ) 
C_  v )
2928adantl 468 . . . . . . 7  |-  ( (
ph  /\  ( v  e.  ( Rt  I )  /\  C  e.  v ) )  ->  E. c  e.  RR+  ( X_ m  e.  ( 1 ... N ) ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) c )  i^i  I ) 
C_  v )
30 resttop 20188 . . . . . . . . . . 11  |-  ( ( R  e.  Top  /\  I  e.  _V )  ->  ( Rt  I )  e.  Top )
317, 10, 30mp2an 679 . . . . . . . . . 10  |-  ( Rt  I )  e.  Top
32 reex 9635 . . . . . . . . . . . . . 14  |-  RR  e.  _V
33 unitssre 11786 . . . . . . . . . . . . . 14  |-  ( 0 [,] 1 )  C_  RR
34 mapss 7519 . . . . . . . . . . . . . 14  |-  ( ( RR  e.  _V  /\  ( 0 [,] 1
)  C_  RR )  ->  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) 
C_  ( RR  ^m  ( 1 ... N
) ) )
3532, 33, 34mp2an 679 . . . . . . . . . . . . 13  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
368, 35eqsstri 3464 . . . . . . . . . . . 12  |-  I  C_  ( RR  ^m  (
1 ... N ) )
37 ovex 6323 . . . . . . . . . . . . . 14  |-  ( 1 ... N )  e. 
_V
38 uniretop 21795 . . . . . . . . . . . . . . 15  |-  RR  =  U. ( topGen `  ran  (,) )
391, 38ptuniconst 20625 . . . . . . . . . . . . . 14  |-  ( ( ( 1 ... N
)  e.  _V  /\  ( topGen `  ran  (,) )  e.  Top )  ->  ( RR  ^m  ( 1 ... N ) )  = 
U. R )
4037, 3, 39mp2an 679 . . . . . . . . . . . . 13  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
4140restuni 20190 . . . . . . . . . . . 12  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
427, 36, 41mp2an 679 . . . . . . . . . . 11  |-  I  = 
U. ( Rt  I )
4342eltopss 19949 . . . . . . . . . 10  |-  ( ( ( Rt  I )  e.  Top  /\  v  e.  ( Rt  I ) )  ->  v  C_  I )
4431, 43mpan 677 . . . . . . . . 9  |-  ( v  e.  ( Rt  I )  ->  v  C_  I
)
4544sselda 3434 . . . . . . . 8  |-  ( ( v  e.  ( Rt  I )  /\  C  e.  v )  ->  C  e.  I )
46 2rp 11314 . . . . . . . . . . . . . . . . 17  |-  2  e.  RR+
47 rpdivcl 11332 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  e.  RR+  /\  c  e.  RR+ )  ->  (
2  /  c )  e.  RR+ )
4846, 47mpan 677 . . . . . . . . . . . . . . . 16  |-  ( c  e.  RR+  ->  ( 2  /  c )  e.  RR+ )
4948rpred 11348 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  ( 2  /  c )  e.  RR )
50 ceicl 12077 . . . . . . . . . . . . . . 15  |-  ( ( 2  /  c )  e.  RR  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  ZZ )
5149, 50syl 17 . . . . . . . . . . . . . 14  |-  ( c  e.  RR+  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  ZZ )
52 0red 9649 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  0  e.  RR )
5351zred 11047 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  RR )
5448rpgt0d 11351 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  0  < 
( 2  /  c
) )
55 ceige 12079 . . . . . . . . . . . . . . . 16  |-  ( ( 2  /  c )  e.  RR  ->  (
2  /  c )  <_  -u ( |_ `  -u ( 2  /  c
) ) )
5649, 55syl 17 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  ( 2  /  c )  <_  -u ( |_ `  -u (
2  /  c ) ) )
5752, 49, 53, 54, 56ltletrd 9800 . . . . . . . . . . . . . 14  |-  ( c  e.  RR+  ->  0  <  -u ( |_ `  -u (
2  /  c ) ) )
58 elnnz 10954 . . . . . . . . . . . . . 14  |-  ( -u ( |_ `  -u (
2  /  c ) )  e.  NN  <->  ( -u ( |_ `  -u ( 2  / 
c ) )  e.  ZZ  /\  0  <  -u ( |_ `  -u (
2  /  c ) ) ) )
5951, 57, 58sylanbrc 671 . . . . . . . . . . . . 13  |-  ( c  e.  RR+  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  NN )
60 fveq2 5870 . . . . . . . . . . . . . . 15  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  ( ZZ>=
`  i )  =  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )
61 oveq2 6303 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  (
1  /  i )  =  ( 1  /  -u ( |_ `  -u (
2  /  c ) ) ) )
6261oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  (
( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  =  ( ( C `  m ) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) ) )
6362eleq2d 2516 . . . . . . . . . . . . . . . 16  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  (
( ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  m )  e.  ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  <->  ( ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) `  m )  e.  ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) ) ) )
6463ralbidv 2829 . . . . . . . . . . . . . . 15  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  ( A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  <->  A. m  e.  ( 1 ... N
) ( ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) `  m )  e.  ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) ) ) )
6560, 64rexeqbidv 3004 . . . . . . . . . . . . . 14  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  ( E. k  e.  ( ZZ>=
`  i ) A. m  e.  ( 1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  <->  E. k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) A. m  e.  ( 1 ... N ) ( ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  m )  e.  ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) ) ) )
6665rspcv 3148 . . . . . . . . . . . . 13  |-  ( -u ( |_ `  -u (
2  /  c ) )  e.  NN  ->  ( A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) A. m  e.  ( 1 ... N
) ( ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) `  m )  e.  ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  ->  E. k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) A. m  e.  ( 1 ... N ) ( ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  m )  e.  ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) ) ) )
6759, 66syl 17 . . . . . . . . . . . 12  |-  ( c  e.  RR+  ->  ( A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  ->  E. k  e.  ( ZZ>=
`  -u ( |_ `  -u ( 2  /  c
) ) ) A. m  e.  ( 1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( C `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  /  -u ( |_ `  -u (
2  /  c ) ) ) ) ) )
6867adantl 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  ->  ( A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) A. m  e.  ( 1 ... N
) ( ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) `  m )  e.  ( ( C `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  ->  E. k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) A. m  e.  ( 1 ... N ) ( ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  m )  e.  ( ( C `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) ) ) )
69 uznnssnn 11213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -u ( |_ `  -u (
2  /  c ) )  e.  NN  ->  (
ZZ>= `  -u ( |_ `  -u ( 2  /  c
) ) )  C_  NN )
7059, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( ZZ>= `  -u ( |_ `  -u (
2  /  c ) ) )  C_  NN )
7170sseld 3433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  RR+  ->  ( k  e.  ( ZZ>= `  -u ( |_ `  -u ( 2  / 
c ) ) )  ->  k  e.  NN ) )
7271adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  ->  (
k  e.  ( ZZ>= `  -u ( |_ `  -u (
2  /  c ) ) )  ->  k  e.  NN ) )
7372imdistani 697 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>=
`  -u ( |_ `  -u ( 2  /  c
) ) ) )  ->  ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN ) )
7459nnrpd 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  e.  RR+  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  RR+ )
7548, 74lerecd 11367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  ( ( 2  /  c )  <_  -u ( |_ `  -u ( 2  /  c
) )  <->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( 1  /  (
2  /  c ) ) ) )
7656, 75mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( 1  /  (
2  /  c ) ) )
77 rpcn 11317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  c  e.  CC )
78 rpne0 11324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  c  =/=  0 )
79 2cn 10687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  2  e.  CC
80 2ne0 10709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  2  =/=  0
81 recdiv 10320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 2  e.  CC  /\  2  =/=  0 )  /\  ( c  e.  CC  /\  c  =/=  0 ) )  -> 
( 1  /  (
2  /  c ) )  =  ( c  /  2 ) )
8279, 80, 81mpanl12 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  CC  /\  c  =/=  0 )  -> 
( 1  /  (
2  /  c ) )  =  ( c  /  2 ) )
8377, 78, 82syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( 1  /  ( 2  / 
c ) )  =  ( c  /  2
) )
8476, 83breqtrd 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  RR+  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( c  /  2
) )
8584ad4antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
1  /  -u ( |_ `  -u ( 2  / 
c ) ) )  <_  ( c  / 
2 ) )
86 elmapi 7498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( C  e.  ( ( 0 [,] 1 )  ^m  ( 1 ... N
) )  ->  C : ( 1 ... N ) --> ( 0 [,] 1 ) )
8786, 8eleq2s 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( C  e.  I  ->  C : ( 1 ... N ) --> ( 0 [,] 1 ) )
8887ad4antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N ) )  ->  C :
( 1 ... N
) --> ( 0 [,] 1 ) )
8988ffvelrnda 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( C `  m )  e.  ( 0 [,] 1
) )
9033, 89sseldi 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( C `  m )  e.  RR )
91 simp-4l 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N ) )  ->  ph )
92 simplr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N ) )  ->  k  e.  NN )
9391, 92jca 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N ) )  ->  ( ph  /\  k  e.  NN ) )
94 poimirlem30.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  G : NN --> ( ( NN0  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
9594ffvelrnda 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  k  e.  NN )  ->  ( G `
 k )  e.  ( ( NN0  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } ) )
96 xp1st 6828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( G `  k )  e.  ( ( NN0 
^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  ( G `  k )
)  e.  ( NN0 
^m  ( 1 ... N ) ) )
97 elmapi 7498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 1st `  ( G `
 k ) )  e.  ( NN0  ^m  ( 1 ... N
) )  ->  ( 1st `  ( G `  k ) ) : ( 1 ... N
) --> NN0 )
9895, 96, 973syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( G `  k
) ) : ( 1 ... N ) --> NN0 )
9998ffvelrnda 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  (
( 1st `  ( G `  k )
) `  m )  e.  NN0 )
10099nn0red 10933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  (
( 1st `  ( G `  k )
) `  m )  e.  RR )
101 simplr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  k  e.  NN )
102100, 101nndivred 10665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( G `  k )
) `  m )  /  k )  e.  RR )
10393, 102sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( G `  k )
) `  m )  /  k )  e.  RR )
10490, 103resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) )  e.  RR )
105104recnd 9674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) )  e.  CC )
106105abscld 13510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  ( ( C `
 m )  -  ( ( ( 1st `  ( G `  k
) ) `  m
)  /  k ) ) )  e.  RR )
10759nnrecred 10662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  e.  RR )
108107ad4antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
1  /  -u ( |_ `  -u ( 2  / 
c ) ) )  e.  RR )
109 rphalfcl 11334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  ( c  /  2 )  e.  RR+ )
110109rpred 11348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( c  /  2 )  e.  RR )
111110ad4antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
c  /  2 )  e.  RR )
112 ltletr 9730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  e.  RR  /\  ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) )  e.  RR  /\  (
c  /  2 )  e.  RR )  -> 
( ( ( abs `  ( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  /\  ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) )  <_  ( c  / 
2 ) )  -> 
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( c  /  2 ) ) )
113106, 108, 111, 112syl3anc 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  /\  ( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) )  <_  ( c  / 
2 ) )  -> 
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( c  /  2 ) ) )
11485, 113mpan2d 681 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  -> 
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( c  /  2 ) ) )
11573, 114sylanl1 656 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  -> 
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( c  /  2 ) ) )
116 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  C  e.  I )  ->  ph )
11770sselda 3434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  k  e.  NN )
118116, 117anim12i 570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  C  e.  I )  /\  (
c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) ) )  ->  ( ph  /\  k  e.  NN ) )
119118anassrs 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>=
`  -u ( |_ `  -u ( 2  /  c
) ) ) )  ->  ( ph  /\  k  e.  NN )
)
120 1re 9647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  1  e.  RR
121 snssi 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 1  e.  RR  ->  { 1 }  C_  RR )
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  { 1 }  C_  RR
123 0re 9648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  0  e.  RR
124 snssi 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0  e.  RR  ->  { 0 }  C_  RR )
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  { 0 }  C_  RR
126122, 125unssi 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( { 1 }  u.  {
0 } )  C_  RR
127 1ex 9643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  1  e.  _V
128127fconst 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } ) : ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) ) --> { 1 }
129 c0ex 9642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  e.  _V
130129fconst 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) ) --> { 0 }
131128, 130pm3.2i 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } ) : ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) ) --> { 1 }  /\  (
( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) ) --> { 0 } )
132 xp2nd 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( G `  k )  e.  ( ( NN0 
^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  ( G `  k )
)  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
13395, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2nd `  ( G `  k
) )  e.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )
134 fvex 5880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 2nd `  ( G `  k
) )  e.  _V
135 f1oeq1 5810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( f  =  ( 2nd `  ( G `  k )
)  ->  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( G `  k )
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
136134, 135elab 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 2nd `  ( G `
 k ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  <-> 
( 2nd `  ( G `  k )
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
137133, 136sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2nd `  ( G `  k
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
138 dff1o3 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 2nd `  ( G `
 k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( G `  k
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( G `
 k ) ) ) )
139138simprbi 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2nd `  ( G `
 k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( G `
 k ) ) )
140 imain 5664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( Fun  `' ( 2nd `  ( G `  k )
)  ->  ( ( 2nd `  ( G `  k ) ) "
( ( 1 ... j )  i^i  (
( j  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  i^i  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) ) )
141137, 139, 1403syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2nd `  ( G `
 k ) )
" ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N
) ) )  =  ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  i^i  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) ) )
142 elfznn0 11894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( j  e.  ( 0 ... N )  ->  j  e.  NN0 )
143142nn0red 10933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
144143ltp1d 10544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( j  e.  ( 0 ... N )  ->  j  <  ( j  +  1 ) )
145 fzdisj 11833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( j  <  ( j  +  1 )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
146144, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( j  e.  ( 0 ... N )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
147146imaeq2d 5171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  ( G `  k )
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  ( ( 2nd `  ( G `  k
) ) " (/) ) )
148 ima0 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2nd `  ( G `
 k ) )
" (/) )  =  (/)
149147, 148syl6eq 2503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  ( G `  k )
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  (/) )
150141, 149sylan9req 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  i^i  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) )  =  (/) )
151 fun 5751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } ) : ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) ) --> { 1 }  /\  ( ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) ) --> { 0 } )  /\  ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  i^i  ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) ) )  =  (/) )  -> 
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) : ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  u.  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } ) )
152131, 150, 151sylancr 670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  u.  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } ) )
153 imaundi 5251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 2nd `  ( G `
 k ) )
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N
) ) )  =  ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  u.  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) )
154 nn0p1nn 10916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
155142, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  NN )
156 nnuz 11201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  NN  =  ( ZZ>= `  1 )
157155, 156syl6eleq 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
158 elfzuz3 11804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  j )
)
159 fzsplit2 11831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  j )
)  ->  ( 1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
160157, 158, 159syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( j  e.  ( 0 ... N )  ->  (
1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
161160imaeq2d 5171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  ( G `  k )
) " ( 1 ... N ) )  =  ( ( 2nd `  ( G `  k
) ) " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... N ) ) ) )
162 f1ofo 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 2nd `  ( G `
 k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( G `  k
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
163 foima 5803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 2nd `  ( G `
 k ) ) : ( 1 ... N ) -onto-> ( 1 ... N )  -> 
( ( 2nd `  ( G `  k )
) " ( 1 ... N ) )  =  ( 1 ... N ) )
164137, 162, 1633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2nd `  ( G `
 k ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
165161, 164sylan9req 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  ( 0 ... N )  /\  ( ph  /\  k  e.  NN ) )  -> 
( ( 2nd `  ( G `  k )
) " ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
166165ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( 2nd `  ( G `  k )
) " ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
167153, 166syl5eqr 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  u.  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
168167feq2d 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) : ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  u.  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } )  <->  ( (
( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  { 0 } ) ) )
169152, 168mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  { 0 } ) )
170169ffvelrnda 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  ( (
( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  ( { 1 }  u.  {
0 } ) )
171126, 170sseldi 3432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  ( (
( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  RR )
172 simpllr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  k  e.  NN )
173171, 172nndivred 10665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  ( (
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  /  k )  e.  RR )
174173recnd 9674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  ( (
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  /  k )  e.  CC )
175174absnegd 13523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  =  ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )
176119, 175sylanl1 656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  =  ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )
177119, 170sylanl1 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  ( { 1 }  u.  { 0 } ) )
178 elun 3576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  ( { 1 }  u.  { 0 } )  <->  ( (
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 1 }  \/  ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 0 } ) )
179177, 178sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 1 }  \/  ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 0 } ) )
180 nnrecre 10653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR )
181 nnrp 11318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN  ->  k  e.  RR+ )
182181rpreccld 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR+ )
183182rpge0d 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN  ->  0  <_  ( 1  /  k
) )
184180, 183absidd 13496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  NN  ->  ( abs `  ( 1  / 
k ) )  =  ( 1  /  k
) )
185117, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( abs `  ( 1  /  k
) )  =  ( 1  /  k ) )
186117nnrecred 10662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  k )  e.  RR )
187107adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  e.  RR )
188110adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( c  /  2 )  e.  RR )
189 eluzle 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  ( ZZ>= `  -u ( |_ `  -u ( 2  / 
c ) ) )  ->  -u ( |_ `  -u ( 2  /  c
) )  <_  k
)
190189adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  -u ( |_
`  -u ( 2  / 
c ) )  <_ 
k )
19159adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  -u ( |_
`  -u ( 2  / 
c ) )  e.  NN )
192191nnrpd 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  -u ( |_
`  -u ( 2  / 
c ) )  e.  RR+ )
193117nnrpd 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  k  e.  RR+ )
194192, 193lerecd 11367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( -u ( |_ `  -u ( 2  / 
c ) )  <_ 
k  <->  ( 1  / 
k )  <_  (
1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) ) )
195190, 194mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  k )  <_ 
( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) )
19684adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( c  /  2
) )
197186, 187, 188, 195, 196letrd 9797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  k )  <_ 
( c  /  2
) )
198185, 197eqbrtrd 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( abs `  ( 1  /  k
) )  <_  (
c  /  2 ) )
199 elsni 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 1 }  ->  ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  =  1 )
200199oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 1 }  ->  ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k )  =  ( 1  / 
k ) )
201200fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 1 }  ->  ( abs `  (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  =  ( abs `  ( 1  /  k
) ) )
202201breq1d 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 1 }  ->  ( ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 )  <->  ( abs `  ( 1  /  k
) )  <_  (
c  /  2 ) ) )
203198, 202syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( (
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 1 }  ->  ( abs `  (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) ) )
204109rpge0d 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  e.  RR+  ->  0  <_ 
( c  /  2
) )
205 nncn 10624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN  ->  k  e.  CC )
206 nnne0 10649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN  ->  k  =/=  0 )
207205, 206div0d 10389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN  ->  (
0  /  k )  =  0 )
208207abs00bd 13366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN  ->  ( abs `  ( 0  / 
k ) )  =  0 )
209208breq1d 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN  ->  (
( abs `  (
0  /  k ) )  <_  ( c  /  2 )  <->  0  <_  ( c  /  2 ) ) )
210209biimparc 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( 0  <_  ( c  /  2 )  /\  k  e.  NN )  ->  ( abs `  (
0  /  k ) )  <_  ( c  /  2 ) )
211204, 210sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  k  e.  NN )  ->  ( abs `  ( 0  / 
k ) )  <_ 
( c  /  2
) )
212117, 211syldan 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( abs `  ( 0  /  k
) )  <_  (
c  /  2 ) )
213 elsni 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 0 }  ->  ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  =  0 )
214213oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 0 }  ->  ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k )  =  ( 0  / 
k ) )
215214fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 0 }  ->  ( abs `  (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  =  ( abs `  ( 0  /  k
) ) )
216215breq1d 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 0 }  ->  ( ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 )  <->  ( abs `  ( 0  /  k
) )  <_  (
c  /  2 ) ) )
217212, 216syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( (
( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 0 }  ->  ( abs `  (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) ) )
218203, 217jaod 382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 1 }  \/  ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 0 } )  ->  ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) ) )
219218adantll 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>=
`  -u ( |_ `  -u ( 2  /  c
) ) ) )  ->  ( ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  e.  { 1 }  \/  ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 0 } )  ->  ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) ) )
220219ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 1 }  \/  ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  e.  { 0 } )  ->  ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) ) )
221179, 220mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) )
222176, 221eqbrtrd 4426 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) )
22373, 106sylanl1 656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  ( ( C `
 m )  -  ( ( ( 1st `  ( G `  k
) ) `  m
)  /  k ) ) )  e.  RR )
224 simpll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  ->  ph )
225224anim1i 572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  ->  ( ph  /\  k  e.  NN )
)
226173renegcld 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  -u ( ( ( ( ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  m )  /  k )  e.  RR )
227225, 226sylanl1 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  -u (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k )  e.  RR )
228227recnd 9674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  -u (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k )  e.  CC )
229228abscld 13510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  e.  RR )
23073, 229sylanl1 656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  e.  RR )
231110, 110jca 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  RR+  ->  ( ( c  /  2 )  e.  RR  /\  (
c  /  2 )  e.  RR ) )
232231ad4antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( c  /  2
)  e.  RR  /\  ( c  /  2
)  e.  RR ) )
233 ltleadd 10104 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  e.  RR  /\  ( abs `  -u (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  e.  RR )  /\  ( ( c  /  2 )  e.  RR  /\  ( c  /  2 )  e.  RR ) )  -> 
( ( ( abs `  ( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( c  /  2 )  /\  ( abs `  -u (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) )  ->  ( ( abs `  ( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) ) )
234223, 230, 232, 233syl21anc 1268 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( c  /  2 )  /\  ( abs `  -u (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  <_  ( c  /  2 ) )  ->  ( ( abs `  ( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) ) )
235222, 234mpan2d 681 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  <  ( c  /  2 )  -> 
( ( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) ) )
236105, 228abstrid 13530 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  ( ( ( C `  m )  -  ( ( ( 1st `  ( G `
 k ) ) `
 m )  / 
k ) )  + 
-u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <_  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) ) )
237104, 227readdcld 9675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) )  +  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  e.  RR )
238237recnd 9674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) )  +  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) )  e.  CC )
239238abscld 13510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  ( abs `  ( ( ( C `  m )  -  ( ( ( 1st `  ( G `
 k ) ) `
 m )  / 
k ) )  + 
-u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  e.  RR )
240106, 229readdcld 9675 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  e.  RR )
241110, 110readdcld 9675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( ( c  /  2 )  +  ( c  / 
2 ) )  e.  RR )
242241ad4antlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( c  /  2
)  +  ( c  /  2 ) )  e.  RR )
243 lelttr 9729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( abs `  (
( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) )  +  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  e.  RR  /\  ( ( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  e.  RR  /\  ( ( c  / 
2 )  +  ( c  /  2 ) )  e.  RR )  ->  ( ( ( abs `  ( ( ( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) )  +  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <_  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  /\  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) )  ->  ( abs `  ( ( ( C `
 m )  -  ( ( ( 1st `  ( G `  k
) ) `  m
)  /  k ) )  +  -u (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) ) )
244239, 240, 242, 243syl3anc 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( abs `  (
( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) )  +  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <_  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  /\  (
( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) )  ->  ( abs `  ( ( ( C `
 m )  -  ( ( ( 1st `  ( G `  k
) ) `  m
)  /  k ) )  +  -u (
( ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) ) )
245236, 244mpand 682 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( abs `  (
( C `  m
)  -  ( ( ( 1st `  ( G `  k )
) `  m )  /  k ) ) )  +  ( abs `  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) )  ->  ( abs `  (
( ( C `  m )  -  (
( ( 1st `  ( G `  k )
) `  m )  /  k ) )  +  -u ( ( ( ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) `  m
)  /  k ) ) )  <  (
( c  /  2
)  +  ( c  /  2 ) ) ) )
24673, 245sylanl1 656 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  C