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

Theorem poimirlem29 31883
Description: Lemma for poimir 31887 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 12185 . . . . . . . . . . . . 13  |-  ( 1 ... N )  e. 
Fin
3 retop 21769 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
43fconst6 5787 . . . . . . . . . . . . 13  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
5 pttop 20584 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top )  ->  ( Xt_ `  ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )  e.  Top )
62, 4, 5mp2an 676 . . . . . . . . . . . 12  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) )  e. 
Top
71, 6eqeltri 2506 . . . . . . . . . . 11  |-  R  e. 
Top
8 poimir.i . . . . . . . . . . . 12  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
9 ovex 6330 . . . . . . . . . . . 12  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  e. 
_V
108, 9eqeltri 2506 . . . . . . . . . . 11  |-  I  e. 
_V
11 elrest 15314 . . . . . . . . . . 11  |-  ( ( R  e.  Top  /\  I  e.  _V )  ->  ( v  e.  ( Rt  I )  <->  E. z  e.  R  v  =  ( z  i^i  I
) ) )
127, 10, 11mp2an 676 . . . . . . . . . 10  |-  ( v  e.  ( Rt  I )  <->  E. z  e.  R  v  =  ( z  i^i  I ) )
13 eqid 2422 . . . . . . . . . . . . . 14  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
141, 13ptrecube 31854 . . . . . . . . . . . . 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 435 . . . . . . . . . . . 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 3682 . . . . . . . . . . . . . . 15  |-  ( z  i^i  I )  C_  z
17 sseq1 3485 . . . . . . . . . . . . . . 15  |-  ( v  =  ( z  i^i  I )  ->  (
v  C_  z  <->  ( z  i^i  I )  C_  z
) )
1816, 17mpbiri 236 . . . . . . . . . . . . . 14  |-  ( v  =  ( z  i^i  I )  ->  v  C_  z )
1918sseld 3463 . . . . . . . . . . . . 13  |-  ( v  =  ( z  i^i  I )  ->  ( C  e.  v  ->  C  e.  z ) )
20 ssrin 3687 . . . . . . . . . . . . . . 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 3486 . . . . . . . . . . . . . . 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 224 . . . . . . . . . . . . . 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 2899 . . . . . . . . . . . . 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 2911 . . . . . . . . . 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 198 . . . . . . . . 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 430 . . . . . . . 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 467 . . . . . . 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 20163 . . . . . . . . . . 11  |-  ( ( R  e.  Top  /\  I  e.  _V )  ->  ( Rt  I )  e.  Top )
317, 10, 30mp2an 676 . . . . . . . . . 10  |-  ( Rt  I )  e.  Top
32 reex 9631 . . . . . . . . . . . . . 14  |-  RR  e.  _V
33 unitssre 11780 . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . 13  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
368, 35eqsstri 3494 . . . . . . . . . . . 12  |-  I  C_  ( RR  ^m  (
1 ... N ) )
37 ovex 6330 . . . . . . . . . . . . . 14  |-  ( 1 ... N )  e. 
_V
38 uniretop 21770 . . . . . . . . . . . . . . 15  |-  RR  =  U. ( topGen `  ran  (,) )
391, 38ptuniconst 20600 . . . . . . . . . . . . . 14  |-  ( ( ( 1 ... N
)  e.  _V  /\  ( topGen `  ran  (,) )  e.  Top )  ->  ( RR  ^m  ( 1 ... N ) )  = 
U. R )
4037, 3, 39mp2an 676 . . . . . . . . . . . . 13  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
4140restuni 20165 . . . . . . . . . . . 12  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
427, 36, 41mp2an 676 . . . . . . . . . . 11  |-  I  = 
U. ( Rt  I )
4342eltopss 19924 . . . . . . . . . 10  |-  ( ( ( Rt  I )  e.  Top  /\  v  e.  ( Rt  I ) )  ->  v  C_  I )
4431, 43mpan 674 . . . . . . . . 9  |-  ( v  e.  ( Rt  I )  ->  v  C_  I
)
4544sselda 3464 . . . . . . . 8  |-  ( ( v  e.  ( Rt  I )  /\  C  e.  v )  ->  C  e.  I )
46 2rp 11308 . . . . . . . . . . . . . . . . 17  |-  2  e.  RR+
47 rpdivcl 11326 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  e.  RR+  /\  c  e.  RR+ )  ->  (
2  /  c )  e.  RR+ )
4846, 47mpan 674 . . . . . . . . . . . . . . . 16  |-  ( c  e.  RR+  ->  ( 2  /  c )  e.  RR+ )
4948rpred 11342 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  ( 2  /  c )  e.  RR )
50 ceicl 12070 . . . . . . . . . . . . . . 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 9645 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  0  e.  RR )
5351zred 11041 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  RR )
5448rpgt0d 11345 . . . . . . . . . . . . . . 15  |-  ( c  e.  RR+  ->  0  < 
( 2  /  c
) )
55 ceige 12072 . . . . . . . . . . . . . . . 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 9796 . . . . . . . . . . . . . 14  |-  ( c  e.  RR+  ->  0  <  -u ( |_ `  -u (
2  /  c ) ) )
58 elnnz 10948 . . . . . . . . . . . . . 14  |-  ( -u ( |_ `  -u (
2  /  c ) )  e.  NN  <->  ( -u ( |_ `  -u ( 2  / 
c ) )  e.  ZZ  /\  0  <  -u ( |_ `  -u (
2  /  c ) ) ) )
5951, 57, 58sylanbrc 668 . . . . . . . . . . . . 13  |-  ( c  e.  RR+  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  NN )
60 fveq2 5878 . . . . . . . . . . . . . . 15  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  ( ZZ>=
`  i )  =  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )
61 oveq2 6310 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  -u ( |_ `  -u ( 2  /  c
) )  ->  (
1  /  i )  =  ( 1  /  -u ( |_ `  -u (
2  /  c ) ) ) )
6261oveq2d 6318 . . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . 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 2864 . . . . . . . . . . . . . . 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 3040 . . . . . . . . . . . . . 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 3178 . . . . . . . . . . . . 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 467 . . . . . . . . . . 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 11207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  RR+  ->  ( k  e.  ( ZZ>= `  -u ( |_ `  -u ( 2  / 
c ) ) )  ->  k  e.  NN ) )
7271adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  ->  (
k  e.  ( ZZ>= `  -u ( |_ `  -u (
2  /  c ) ) )  ->  k  e.  NN ) )
7372imdistani 694 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  e.  RR+  ->  -u ( |_ `  -u ( 2  / 
c ) )  e.  RR+ )
7548, 74lerecd 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  ( ( 2  /  c )  <_  -u ( |_ `  -u ( 2  /  c
) )  <->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( 1  /  (
2  /  c ) ) ) )
7656, 75mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( 1  /  (
2  /  c ) ) )
77 rpcn 11311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  c  e.  CC )
78 rpne0 11318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  c  =/=  0 )
79 2cn 10681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  2  e.  CC
80 2ne0 10703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  2  =/=  0
81 recdiv 10314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 2  e.  CC  /\  2  =/=  0 )  /\  ( c  e.  CC  /\  c  =/=  0 ) )  -> 
( 1  /  (
2  /  c ) )  =  ( c  /  2 ) )
8279, 80, 81mpanl12 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  CC  /\  c  =/=  0 )  -> 
( 1  /  (
2  /  c ) )  =  ( c  /  2 ) )
8377, 78, 82syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( 1  /  ( 2  / 
c ) )  =  ( c  /  2
) )
8476, 83breqtrd 4445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  RR+  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( c  /  2
) )
8584ad4antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( C  e.  I  ->  C : ( 1 ... N ) --> ( 0 [,] 1 ) )
8887ad4antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N ) )  ->  C :
( 1 ... N
) --> ( 0 [,] 1 ) )
8988ffvelrnda 6034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N ) )  ->  ph )
92 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  /\  j  e.  ( 0 ... N ) )  ->  k  e.  NN )
9391, 92jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  k  e.  NN )  ->  ( G `
 k )  e.  ( ( NN0  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } ) )
96 xp1st 6834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  (
( 1st `  ( G `  k )
) `  m )  e.  NN0 )
10099nn0red 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  (
( 1st `  ( G `  k )
) `  m )  e.  RR )
101 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  k  e.  NN )
102100, 101nndivred 10659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( G `  k )
) `  m )  /  k )  e.  RR )
10393, 102sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  e.  RR )
108107ad4antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  e.  RR+  ->  ( c  /  2 )  e.  RR+ )
110109rpred 11342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( c  /  2 )  e.  RR )
111110ad4antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . . . . . . . . . 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 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  C  e.  I )  ->  ph )
11770sselda 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  k  e.  NN )
118116, 117anim12i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  C  e.  I )  /\  (
c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) ) )  ->  ( ph  /\  k  e.  NN ) )
119118anassrs 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  ( ZZ>=
`  -u ( |_ `  -u ( 2  /  c
) ) ) )  ->  ( ph  /\  k  e.  NN )
)
120 1re 9643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  1  e.  RR
121 snssi 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 1  e.  RR  ->  { 1 }  C_  RR )
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  { 1 }  C_  RR
123 0re 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  0  e.  RR
124 snssi 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 0  e.  RR  ->  { 0 }  C_  RR )
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  { 0 }  C_  RR
126122, 125unssi 3641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( { 1 }  u.  {
0 } )  C_  RR
127 1ex 9639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  1  e.  _V
128127fconst 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } ) : ( ( 2nd `  ( G `
 k ) )
" ( 1 ... j ) ) --> { 1 }
129 c0ex 9638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  0  e.  _V
130129fconst 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  ( G `
 k ) )
" ( ( j  +  1 ) ... N ) ) --> { 0 }
131128, 130pm3.2i 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 2nd `  ( G `  k
) )  e.  _V
135 f1oeq1 5819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2nd `  ( G `  k
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
138 dff1o3 5834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 2nd `  ( G `
 k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( G `  k
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( G `
 k ) ) ) )
139138simprbi 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2nd `  ( G `
 k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( G `
 k ) ) )
140 imain 5674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( j  e.  ( 0 ... N )  ->  j  e.  NN0 )
143142nn0red 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
144143ltp1d 10538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( j  e.  ( 0 ... N )  ->  j  <  ( j  +  1 ) )
145 fzdisj 11827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  ( G `  k )
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  ( ( 2nd `  ( G `  k
) ) " (/) ) )
148 ima0 5199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 2nd `  ( G `
 k ) )
" (/) )  =  (/)
149147, 148syl6eq 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  ( G `  k )
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  (/) )
150141, 149sylan9req 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  i^i  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) )  =  (/) )
151 fun 5760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 2nd `  ( G `
 k ) )
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N
) ) )  =  ( ( ( 2nd `  ( G `  k
) ) " (
1 ... j ) )  u.  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) )
154 nn0p1nn 10910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
155142, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  NN )
156 nnuz 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  NN  =  ( ZZ>= `  1 )
157155, 156syl6eleq 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
158 elfzuz3 11798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  j )
)
159 fzsplit2 11825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  j )
)  ->  ( 1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
160157, 158, 159syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( j  e.  ( 0 ... N )  ->  (
1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
161160imaeq2d 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  ( G `  k )
) " ( 1 ... N ) )  =  ( ( 2nd `  ( G `  k
) ) " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... N ) ) ) )
162 f1ofo 5835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 2nd `  ( G `
 k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( G `  k
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
163 foima 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  ( 0 ... N )  /\  ( ph  /\  k  e.  NN ) )  -> 
( ( 2nd `  ( G `  k )
) " ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
166165ancoms 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( 2nd `  ( G `  k )
) " ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
167153, 166syl5eqr 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 0 ... N
) )  ->  (
( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  u.  ( ( 2nd `  ( G `  k
) ) " (
( j  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
168167feq2d 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  k  e.  NN )  /\  j  e.  (
0 ... N ) )  /\  m  e.  ( 1 ... N ) )  ->  k  e.  NN )
173171, 172nndivred 10659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13499 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR )
181 nnrp 11312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN  ->  k  e.  RR+ )
182181rpreccld 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN  ->  (
1  /  k )  e.  RR+ )
183182rpge0d 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN  ->  0  <_  ( 1  /  k
) )
184180, 183absidd 13473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  k )  e.  RR )
187107adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  e.  RR )
188110adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( c  /  2 )  e.  RR )
189 eluzle 11172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  ( ZZ>= `  -u ( |_ `  -u ( 2  / 
c ) ) )  ->  -u ( |_ `  -u ( 2  /  c
) )  <_  k
)
190189adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  -u ( |_
`  -u ( 2  / 
c ) )  <_ 
k )
19159adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  -u ( |_
`  -u ( 2  / 
c ) )  e.  NN )
192191nnrpd 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  -u ( |_
`  -u ( 2  / 
c ) )  e.  RR+ )
193117nnrpd 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  k  e.  RR+ )
194192, 193lerecd 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  k )  <_ 
( 1  /  -u ( |_ `  -u ( 2  / 
c ) ) ) )
19684adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  -u ( |_ `  -u ( 2  /  c
) ) )  <_ 
( c  /  2
) )
197186, 187, 188, 195, 196letrd 9793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( 1  /  k )  <_ 
( c  /  2
) )
198185, 197eqbrtrd 4441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( abs `  ( 1  /  k
) )  <_  (
c  /  2 ) )
199 elsni 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  e.  RR+  ->  0  <_ 
( c  /  2
) )
205 nncn 10618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN  ->  k  e.  CC )
206 nnne0 10643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  NN  ->  k  =/=  0 )
207205, 206div0d 10383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  NN  ->  (
0  /  k )  =  0 )
208207abs00bd 13343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  NN  ->  ( abs `  ( 0  / 
k ) )  =  0 )
209208breq1d 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  NN  ->  (
( abs `  (
0  /  k ) )  <_  ( c  /  2 )  <->  0  <_  ( c  /  2 ) ) )
210209biimparc 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( 0  <_  ( c  /  2 )  /\  k  e.  NN )  ->  ( abs `  (
0  /  k ) )  <_  ( c  /  2 ) )
211204, 210sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( c  e.  RR+  /\  k  e.  NN )  ->  ( abs `  ( 0  / 
k ) )  <_ 
( c  /  2
) )
212117, 211syldan 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( c  e.  RR+  /\  k  e.  ( ZZ>= `  -u ( |_
`  -u ( 2  / 
c ) ) ) )  ->  ( abs `  ( 0  /  k
) )  <_  (
c  /  2 ) )
213 elsni 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4441 . . . . . . . . . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  ->  ph )
225224anim1i 570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  C  e.  I )  /\  c  e.  RR+ )  /\  k  e.  NN )  ->  ( ph  /\  k  e.  NN )
)
226173renegcld 10047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  e.  RR+  ->  ( ( c  /  2 )  e.  RR  /\  (
c  /  2 )  e.  RR ) )
232231ad4antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . . . . . . . . . . . . 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 13506 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  e.  RR+  ->  ( ( c  /  2 )  +  ( c  / 
2 ) )  e.  RR )
242241ad4antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 679 . . . . . . . . . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  C  e.  I