Metamath Proof Explorer

Theorem poimirlem29

Description: Lemma for poimir connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses 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. ( ( R |`t 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 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. ( R |`t I ) ( C e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimir.i 
 |-  I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
3 poimir.r 
 |-  R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
4 poimir.1 
 |-  ( ph -> F e. ( ( R |`t I ) Cn R ) )
5 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 )
6 poimirlem30.2 
 |-  ( ph -> G : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
7 poimirlem30.3 
 |-  ( ( ph /\ k e. NN ) -> ran ( 1st ` ( G ` k ) ) C_ ( 0 ..^ k ) )
8 poimirlem30.4 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> E. j e. ( 0 ... N ) 0 r X )
9 fzfi 
 |-  ( 1 ... N ) e. Fin
10 retop 
 |-  ( topGen ` ran (,) ) e. Top
11 10 fconst6 
 |-  ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top
12 pttop 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top ) -> ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) e. Top )
13 9 11 12 mp2an 
 |-  ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) e. Top
14 3 13 eqeltri 
 |-  R e. Top
15 ovex 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) e. _V
16 2 15 eqeltri 
 |-  I e. _V
17 elrest 
 |-  ( ( R e. Top /\ I e. _V ) -> ( v e. ( R |`t I ) <-> E. z e. R v = ( z i^i I ) ) )
18 14 16 17 mp2an 
 |-  ( v e. ( R |`t I ) <-> E. z e. R v = ( z i^i I ) )
19 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
20 3 19 ptrecube 
 |-  ( ( 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 )
21 20 ex 
 |-  ( 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 ) )
22 inss1 
 |-  ( z i^i I ) C_ z
23 sseq1 
 |-  ( v = ( z i^i I ) -> ( v C_ z <-> ( z i^i I ) C_ z ) )
24 22 23 mpbiri 
 |-  ( v = ( z i^i I ) -> v C_ z )
25 24 sseld 
 |-  ( v = ( z i^i I ) -> ( C e. v -> C e. z ) )
26 ssrin 
 |-  ( 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 ) )
27 sseq2 
 |-  ( 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 ) ) )
28 26 27 syl5ibr 
 |-  ( 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 ) )
29 28 reximdv 
 |-  ( 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 ) )
30 25 29 imim12d 
 |-  ( 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 ) ) )
31 21 30 syl5com 
 |-  ( 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 ) ) )
32 31 rexlimiv 
 |-  ( 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 ) )
33 18 32 sylbi 
 |-  ( v e. ( R |`t 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 ) )
34 33 imp 
 |-  ( ( v e. ( R |`t 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 )
35 34 adantl 
 |-  ( ( ph /\ ( v e. ( R |`t 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 )
36 resttop 
 |-  ( ( R e. Top /\ I e. _V ) -> ( R |`t I ) e. Top )
37 14 16 36 mp2an 
 |-  ( R |`t I ) e. Top
38 reex 
 |-  RR e. _V
39 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
40 mapss 
 |-  ( ( RR e. _V /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) ) )
41 38 39 40 mp2an 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) )
42 2 41 eqsstri 
 |-  I C_ ( RR ^m ( 1 ... N ) )
43 ovex 
 |-  ( 1 ... N ) e. _V
44 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
45 3 44 ptuniconst 
 |-  ( ( ( 1 ... N ) e. _V /\ ( topGen ` ran (,) ) e. Top ) -> ( RR ^m ( 1 ... N ) ) = U. R )
46 43 10 45 mp2an 
 |-  ( RR ^m ( 1 ... N ) ) = U. R
47 46 restuni 
 |-  ( ( R e. Top /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> I = U. ( R |`t I ) )
48 14 42 47 mp2an 
 |-  I = U. ( R |`t I )
49 48 eltopss 
 |-  ( ( ( R |`t I ) e. Top /\ v e. ( R |`t I ) ) -> v C_ I )
50 37 49 mpan 
 |-  ( v e. ( R |`t I ) -> v C_ I )
51 50 sselda 
 |-  ( ( v e. ( R |`t I ) /\ C e. v ) -> C e. I )
52 2rp 
 |-  2 e. RR+
53 rpdivcl 
 |-  ( ( 2 e. RR+ /\ c e. RR+ ) -> ( 2 / c ) e. RR+ )
54 52 53 mpan 
 |-  ( c e. RR+ -> ( 2 / c ) e. RR+ )
55 54 rpred 
 |-  ( c e. RR+ -> ( 2 / c ) e. RR )
56 ceicl 
 |-  ( ( 2 / c ) e. RR -> -u ( |_ ` -u ( 2 / c ) ) e. ZZ )
57 55 56 syl 
 |-  ( c e. RR+ -> -u ( |_ ` -u ( 2 / c ) ) e. ZZ )
58 0red 
 |-  ( c e. RR+ -> 0 e. RR )
59 57 zred 
 |-  ( c e. RR+ -> -u ( |_ ` -u ( 2 / c ) ) e. RR )
60 54 rpgt0d 
 |-  ( c e. RR+ -> 0 < ( 2 / c ) )
61 ceige 
 |-  ( ( 2 / c ) e. RR -> ( 2 / c ) <_ -u ( |_ ` -u ( 2 / c ) ) )
62 55 61 syl 
 |-  ( c e. RR+ -> ( 2 / c ) <_ -u ( |_ ` -u ( 2 / c ) ) )
63 58 55 59 60 62 ltletrd 
 |-  ( c e. RR+ -> 0 < -u ( |_ ` -u ( 2 / c ) ) )
64 elnnz 
 |-  ( -u ( |_ ` -u ( 2 / c ) ) e. NN <-> ( -u ( |_ ` -u ( 2 / c ) ) e. ZZ /\ 0 < -u ( |_ ` -u ( 2 / c ) ) ) )
65 57 63 64 sylanbrc 
 |-  ( c e. RR+ -> -u ( |_ ` -u ( 2 / c ) ) e. NN )
66 fveq2 
 |-  ( i = -u ( |_ ` -u ( 2 / c ) ) -> ( ZZ>= ` i ) = ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) )
67 oveq2 
 |-  ( i = -u ( |_ ` -u ( 2 / c ) ) -> ( 1 / i ) = ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) )
68 67 oveq2d 
 |-  ( 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 ) ) ) ) )
69 68 eleq2d 
 |-  ( 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 ) ) ) ) ) )
70 69 ralbidv 
 |-  ( 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 ) ) ) ) ) )
71 66 70 rexeqbidv 
 |-  ( 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 ) ) ) ) ) )
72 71 rspcv 
 |-  ( -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 ) ) ) ) ) )
73 65 72 syl 
 |-  ( 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 ) ) ) ) ) )
74 73 adantl 
 |-  ( ( ( 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 ) ) ) ) ) )
75 uznnssnn 
 |-  ( -u ( |_ ` -u ( 2 / c ) ) e. NN -> ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) C_ NN )
76 65 75 syl 
 |-  ( c e. RR+ -> ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) C_ NN )
77 76 sseld 
 |-  ( c e. RR+ -> ( k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) -> k e. NN ) )
78 77 adantl 
 |-  ( ( ( ph /\ C e. I ) /\ c e. RR+ ) -> ( k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) -> k e. NN ) )
79 78 imdistani 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) )
80 65 nnrpd 
 |-  ( c e. RR+ -> -u ( |_ ` -u ( 2 / c ) ) e. RR+ )
81 54 80 lerecd 
 |-  ( c e. RR+ -> ( ( 2 / c ) <_ -u ( |_ ` -u ( 2 / c ) ) <-> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) <_ ( 1 / ( 2 / c ) ) ) )
82 62 81 mpbid 
 |-  ( c e. RR+ -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) <_ ( 1 / ( 2 / c ) ) )
83 rpcn 
 |-  ( c e. RR+ -> c e. CC )
84 rpne0 
 |-  ( c e. RR+ -> c =/= 0 )
85 2cn 
 |-  2 e. CC
86 2ne0 
 |-  2 =/= 0
87 recdiv 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( c e. CC /\ c =/= 0 ) ) -> ( 1 / ( 2 / c ) ) = ( c / 2 ) )
88 85 86 87 mpanl12 
 |-  ( ( c e. CC /\ c =/= 0 ) -> ( 1 / ( 2 / c ) ) = ( c / 2 ) )
89 83 84 88 syl2anc 
 |-  ( c e. RR+ -> ( 1 / ( 2 / c ) ) = ( c / 2 ) )
90 82 89 breqtrd 
 |-  ( c e. RR+ -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) <_ ( c / 2 ) )
91 90 ad4antlr 
 |-  ( ( ( ( ( ( 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 ) )
92 elmapi 
 |-  ( C e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) -> C : ( 1 ... N ) --> ( 0 [,] 1 ) )
93 92 2 eleq2s 
 |-  ( C e. I -> C : ( 1 ... N ) --> ( 0 [,] 1 ) )
94 93 ad4antlr 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> C : ( 1 ... N ) --> ( 0 [,] 1 ) )
95 94 ffvelrnda 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. ( 0 [,] 1 ) )
96 39 95 sseldi 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. RR )
97 simp-4l 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ph )
98 simplr 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> k e. NN )
99 97 98 jca 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ph /\ k e. NN ) )
100 6 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
101 xp1st 
 |-  ( ( 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 ) ) )
102 elmapi 
 |-  ( ( 1st ` ( G ` k ) ) e. ( NN0 ^m ( 1 ... N ) ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> NN0 )
103 100 101 102 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> NN0 )
104 103 ffvelrnda 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( 1st ` ( G ` k ) ) ` m ) e. NN0 )
105 104 nn0red 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( 1st ` ( G ` k ) ) ` m ) e. RR )
106 simplr 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> k e. NN )
107 105 106 nndivred 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. RR )
108 99 107 sylan 
 |-  ( ( ( ( ( ( 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 )
109 96 108 resubcld 
 |-  ( ( ( ( ( ( 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 )
110 109 recnd 
 |-  ( ( ( ( ( ( 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 )
111 110 abscld 
 |-  ( ( ( ( ( ( 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 )
112 65 nnrecred 
 |-  ( c e. RR+ -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) e. RR )
113 112 ad4antlr 
 |-  ( ( ( ( ( ( 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 )
114 rphalfcl 
 |-  ( c e. RR+ -> ( c / 2 ) e. RR+ )
115 114 rpred 
 |-  ( c e. RR+ -> ( c / 2 ) e. RR )
116 115 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( c / 2 ) e. RR )
117 ltletr 
 |-  ( ( ( 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 ) ) )
118 111 113 116 117 syl3anc 
 |-  ( ( ( ( ( ( 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 ) ) )
119 91 118 mpan2d 
 |-  ( ( ( ( ( ( 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 ) ) )
120 79 119 sylanl1 
 |-  ( ( ( ( ( ( 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 ) ) )
121 simpl 
 |-  ( ( ph /\ C e. I ) -> ph )
122 76 sselda 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> k e. NN )
123 121 122 anim12i 
 |-  ( ( ( ph /\ C e. I ) /\ ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) ) -> ( ph /\ k e. NN ) )
124 123 anassrs 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( ph /\ k e. NN ) )
125 1re 
 |-  1 e. RR
126 snssi 
 |-  ( 1 e. RR -> { 1 } C_ RR )
127 125 126 ax-mp 
 |-  { 1 } C_ RR
128 0re 
 |-  0 e. RR
129 snssi 
 |-  ( 0 e. RR -> { 0 } C_ RR )
130 128 129 ax-mp 
 |-  { 0 } C_ RR
131 127 130 unssi 
 |-  ( { 1 } u. { 0 } ) C_ RR
132 1ex 
 |-  1 e. _V
133 132 fconst 
 |-  ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) : ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) --> { 1 }
134 c0ex 
 |-  0 e. _V
135 134 fconst 
 |-  ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) --> { 0 }
136 133 135 pm3.2i 
 |-  ( ( ( ( 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 } )
137 xp2nd 
 |-  ( ( 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 ) } )
138 100 137 syl 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( G ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
139 fvex 
 |-  ( 2nd ` ( G ` k ) ) e. _V
140 f1oeq1 
 |-  ( f = ( 2nd ` ( G ` k ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
141 139 140 elab 
 |-  ( ( 2nd ` ( G ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
142 138 141 sylib 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
143 dff1o3 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( G ` k ) ) ) )
144 143 simprbi 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( G ` k ) ) )
145 imain 
 |-  ( 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 ) ) ) )
146 142 144 145 3syl 
 |-  ( ( 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 ) ) ) )
147 elfznn0 
 |-  ( j e. ( 0 ... N ) -> j e. NN0 )
148 147 nn0red 
 |-  ( j e. ( 0 ... N ) -> j e. RR )
149 148 ltp1d 
 |-  ( j e. ( 0 ... N ) -> j < ( j + 1 ) )
150 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
151 149 150 syl 
 |-  ( j e. ( 0 ... N ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
152 151 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( 2nd ` ( G ` k ) ) " (/) ) )
153 ima0 
 |-  ( ( 2nd ` ( G ` k ) ) " (/) ) = (/)
154 152 153 eqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
155 146 154 sylan9req 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) i^i ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) = (/) )
156 fun 
 |-  ( ( ( ( ( ( 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 } ) )
157 136 155 156 sylancr 
 |-  ( ( ( 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 } ) )
158 imaundi 
 |-  ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) u. ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) )
159 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
160 147 159 syl 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. NN )
161 nnuz 
 |-  NN = ( ZZ>= ` 1 )
162 160 161 eleqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
163 elfzuz3 
 |-  ( j e. ( 0 ... N ) -> N e. ( ZZ>= ` j ) )
164 fzsplit2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` j ) ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
165 162 163 164 syl2anc 
 |-  ( j e. ( 0 ... N ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
166 165 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) )
167 f1ofo 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
168 foima 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
169 142 167 168 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2nd ` ( G ` k ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
170 166 169 sylan9req 
 |-  ( ( j e. ( 0 ... N ) /\ ( ph /\ k e. NN ) ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
171 170 ancoms 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
172 158 171 eqtr3id 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) u. ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
173 172 feq2d 
 |-  ( ( ( 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 } ) ) )
174 157 173 mpbid 
 |-  ( ( ( 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 } ) )
175 174 ffvelrnda 
 |-  ( ( ( ( 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 } ) )
176 131 175 sseldi 
 |-  ( ( ( ( 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 )
177 simpllr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> k e. NN )
178 176 177 nndivred 
 |-  ( ( ( ( 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 )
179 178 recnd 
 |-  ( ( ( ( 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 )
180 179 absnegd 
 |-  ( ( ( ( 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 ) ) )
181 124 180 sylanl1 
 |-  ( ( ( ( ( ( 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 ) ) )
182 124 175 sylanl1 
 |-  ( ( ( ( ( ( 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 } ) )
183 elun 
 |-  ( ( ( ( ( ( 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 } ) )
184 182 183 sylib 
 |-  ( ( ( ( ( ( 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 } ) )
185 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
186 nnrp 
 |-  ( k e. NN -> k e. RR+ )
187 186 rpreccld 
 |-  ( k e. NN -> ( 1 / k ) e. RR+ )
188 187 rpge0d 
 |-  ( k e. NN -> 0 <_ ( 1 / k ) )
189 185 188 absidd 
 |-  ( k e. NN -> ( abs ` ( 1 / k ) ) = ( 1 / k ) )
190 122 189 syl 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( abs ` ( 1 / k ) ) = ( 1 / k ) )
191 122 nnrecred 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( 1 / k ) e. RR )
192 112 adantr 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) e. RR )
193 115 adantr 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( c / 2 ) e. RR )
194 eluzle 
 |-  ( k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) -> -u ( |_ ` -u ( 2 / c ) ) <_ k )
195 194 adantl 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> -u ( |_ ` -u ( 2 / c ) ) <_ k )
196 65 adantr 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> -u ( |_ ` -u ( 2 / c ) ) e. NN )
197 196 nnrpd 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> -u ( |_ ` -u ( 2 / c ) ) e. RR+ )
198 122 nnrpd 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> k e. RR+ )
199 197 198 lerecd 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( -u ( |_ ` -u ( 2 / c ) ) <_ k <-> ( 1 / k ) <_ ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) )
200 195 199 mpbid 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( 1 / k ) <_ ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) )
201 90 adantr 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) <_ ( c / 2 ) )
202 191 192 193 200 201 letrd 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( 1 / k ) <_ ( c / 2 ) )
203 190 202 eqbrtrd 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( abs ` ( 1 / k ) ) <_ ( c / 2 ) )
204 elsni 
 |-  ( ( ( ( ( ( 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 )
205 204 fvoveq1d 
 |-  ( ( ( ( ( ( 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 ) ) )
206 205 breq1d 
 |-  ( ( ( ( ( ( 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 ) ) )
207 203 206 syl5ibrcom 
 |-  ( ( 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 ) ) )
208 114 rpge0d 
 |-  ( c e. RR+ -> 0 <_ ( c / 2 ) )
209 nncn 
 |-  ( k e. NN -> k e. CC )
210 nnne0 
 |-  ( k e. NN -> k =/= 0 )
211 209 210 div0d 
 |-  ( k e. NN -> ( 0 / k ) = 0 )
212 211 abs00bd 
 |-  ( k e. NN -> ( abs ` ( 0 / k ) ) = 0 )
213 212 breq1d 
 |-  ( k e. NN -> ( ( abs ` ( 0 / k ) ) <_ ( c / 2 ) <-> 0 <_ ( c / 2 ) ) )
214 213 biimparc 
 |-  ( ( 0 <_ ( c / 2 ) /\ k e. NN ) -> ( abs ` ( 0 / k ) ) <_ ( c / 2 ) )
215 208 214 sylan 
 |-  ( ( c e. RR+ /\ k e. NN ) -> ( abs ` ( 0 / k ) ) <_ ( c / 2 ) )
216 122 215 syldan 
 |-  ( ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( abs ` ( 0 / k ) ) <_ ( c / 2 ) )
217 elsni 
 |-  ( ( ( ( ( ( 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 )
218 217 fvoveq1d 
 |-  ( ( ( ( ( ( 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 ) ) )
219 218 breq1d 
 |-  ( ( ( ( ( ( 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 ) ) )
220 216 219 syl5ibrcom 
 |-  ( ( 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 ) ) )
221 207 220 jaod 
 |-  ( ( 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 ) ) )
222 221 adantll 
 |-  ( ( ( ( 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 ) ) )
223 222 ad2antrr 
 |-  ( ( ( ( ( ( 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 ) ) )
224 184 223 mpd 
 |-  ( ( ( ( ( ( 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 ) )
225 181 224 eqbrtrd 
 |-  ( ( ( ( ( ( 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 ) )
226 79 111 sylanl1 
 |-  ( ( ( ( ( ( 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 )
227 simpll 
 |-  ( ( ( ph /\ C e. I ) /\ c e. RR+ ) -> ph )
228 227 anim1i 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) -> ( ph /\ k e. NN ) )
229 178 renegcld 
 |-  ( ( ( ( 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 )
230 228 229 sylanl1 
 |-  ( ( ( ( ( ( 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 )
231 230 recnd 
 |-  ( ( ( ( ( ( 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 )
232 231 abscld 
 |-  ( ( ( ( ( ( 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 )
233 79 232 sylanl1 
 |-  ( ( ( ( ( ( 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 )
234 115 115 jca 
 |-  ( c e. RR+ -> ( ( c / 2 ) e. RR /\ ( c / 2 ) e. RR ) )
235 234 ad4antlr 
 |-  ( ( ( ( ( ( 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 ) )
236 ltleadd 
 |-  ( ( ( ( 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 ) ) ) )
237 226 233 235 236 syl21anc 
 |-  ( ( ( ( ( ( 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 ) ) ) )
238 225 237 mpan2d 
 |-  ( ( ( ( ( ( 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 ) ) ) )
239 110 231 abstrid 
 |-  ( ( ( ( ( ( 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 ) ) ) )
240 109 230 readdcld 
 |-  ( ( ( ( ( ( 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 )
241 240 recnd 
 |-  ( ( ( ( ( ( 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 )
242 241 abscld 
 |-  ( ( ( ( ( ( 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 )
243 111 232 readdcld 
 |-  ( ( ( ( ( ( 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 )
244 115 115 readdcld 
 |-  ( c e. RR+ -> ( ( c / 2 ) + ( c / 2 ) ) e. RR )
245 244 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( c / 2 ) + ( c / 2 ) ) e. RR )
246 lelttr 
 |-  ( ( ( 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 ) ) ) )
247 242 243 245 246 syl3anc 
 |-  ( ( ( ( ( ( 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 ) ) ) )
248 239 247 mpand 
 |-  ( ( ( ( ( ( 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 ) ) ) )
249 79 248 sylanl1 
 |-  ( ( ( ( ( ( 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 ) ) ) + ( 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 ) ) ) )
250 120 238 249 3syld 
 |-  ( ( ( ( ( ( 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 ) ) + -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) ) < ( ( c / 2 ) + ( c / 2 ) ) ) )
251 105 adantlr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( 1st ` ( G ` k ) ) ` m ) e. RR )
252 251 176 readdcld 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) e. RR )
253 252 177 nndivred 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) e. RR )
254 124 253 sylanl1 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) e. RR )
255 250 254 jctild 
 |-  ( ( ( ( ( ( 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 ) ) ) -> ( ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) ) + -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) ) < ( ( c / 2 ) + ( c / 2 ) ) ) ) )
256 255 adantld 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) ) + -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) ) < ( ( c / 2 ) + ( c / 2 ) ) ) ) )
257 79 adantr 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) )
258 93 ad3antlr 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) -> C : ( 1 ... N ) --> ( 0 [,] 1 ) )
259 258 ffvelrnda 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. ( 0 [,] 1 ) )
260 39 259 sseldi 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. RR )
261 80 rpreccld 
 |-  ( c e. RR+ -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) e. RR+ )
262 261 rpxrd 
 |-  ( c e. RR+ -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) e. RR* )
263 262 ad3antlr 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) e. RR* )
264 19 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
265 elbl 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( C ` m ) e. RR /\ ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) e. RR* ) -> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) <-> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) ) )
266 264 265 mp3an1 
 |-  ( ( ( C ` m ) e. RR /\ ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) e. RR* ) -> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) <-> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) ) )
267 260 263 266 syl2anc 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ 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 ) ) ) ) <-> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) ) )
268 elmapfn 
 |-  ( ( 1st ` ( G ` k ) ) e. ( NN0 ^m ( 1 ... N ) ) -> ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) )
269 100 101 268 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) )
270 vex 
 |-  k e. _V
271 fnconstg 
 |-  ( k e. _V -> ( ( 1 ... N ) X. { k } ) Fn ( 1 ... N ) )
272 270 271 mp1i 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 ... N ) X. { k } ) Fn ( 1 ... N ) )
273 fzfid 
 |-  ( ( ph /\ k e. NN ) -> ( 1 ... N ) e. Fin )
274 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
275 eqidd 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( 1st ` ( G ` k ) ) ` m ) = ( ( 1st ` ( G ` k ) ) ` m ) )
276 270 fvconst2 
 |-  ( m e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { k } ) ` m ) = k )
277 276 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { k } ) ` m ) = k )
278 269 272 273 273 274 275 277 ofval 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) = ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) )
279 278 oveq2d 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) = ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) )
280 227 279 sylanl1 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) = ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) )
281 227 107 sylanl1 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. RR )
282 19 remetdval 
 |-  ( ( ( C ` m ) e. RR /\ ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. RR ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) = ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) )
283 260 281 282 syl2anc 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) = ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) )
284 280 283 eqtrd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) = ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) )
285 284 breq1d 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) <-> ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) )
286 285 anbi2d 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) <-> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) ) )
287 267 286 bitrd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ 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 ) ) ) ) <-> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) ) )
288 257 287 sylan 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) /\ 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 ) ) ) ) <-> ( ( ( ( 1st ` ( G ` k ) ) oF / ( ( 1 ... N ) X. { k } ) ) ` m ) e. RR /\ ( abs ` ( ( C ` m ) - ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) ) ) < ( 1 / -u ( |_ ` -u ( 2 / c ) ) ) ) ) )
289 rpxr 
 |-  ( c e. RR+ -> c e. RR* )
290 289 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> c e. RR* )
291 elbl 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( C ` m ) e. RR /\ c e. RR* ) -> ( ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) <-> ( ( ( ( ( 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 } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) < c ) ) )
292 264 291 mp3an1 
 |-  ( ( ( C ` m ) e. RR /\ c e. RR* ) -> ( ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) <-> ( ( ( ( ( 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 } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) < c ) ) )
293 96 290 292 syl2anc 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) <-> ( ( ( ( ( 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 } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) < c ) ) )
294 elun 
 |-  ( z e. ( { 1 } u. { 0 } ) <-> ( z e. { 1 } \/ z e. { 0 } ) )
295 fzofzp1 
 |-  ( v e. ( 0 ..^ k ) -> ( v + 1 ) e. ( 0 ... k ) )
296 elsni 
 |-  ( z e. { 1 } -> z = 1 )
297 296 oveq2d 
 |-  ( z e. { 1 } -> ( v + z ) = ( v + 1 ) )
298 297 eleq1d 
 |-  ( z e. { 1 } -> ( ( v + z ) e. ( 0 ... k ) <-> ( v + 1 ) e. ( 0 ... k ) ) )
299 295 298 syl5ibrcom 
 |-  ( v e. ( 0 ..^ k ) -> ( z e. { 1 } -> ( v + z ) e. ( 0 ... k ) ) )
300 elfzonn0 
 |-  ( v e. ( 0 ..^ k ) -> v e. NN0 )
301 300 nn0cnd 
 |-  ( v e. ( 0 ..^ k ) -> v e. CC )
302 301 addid1d 
 |-  ( v e. ( 0 ..^ k ) -> ( v + 0 ) = v )
303 elfzofz 
 |-  ( v e. ( 0 ..^ k ) -> v e. ( 0 ... k ) )
304 302 303 eqeltrd 
 |-  ( v e. ( 0 ..^ k ) -> ( v + 0 ) e. ( 0 ... k ) )
305 elsni 
 |-  ( z e. { 0 } -> z = 0 )
306 305 oveq2d 
 |-  ( z e. { 0 } -> ( v + z ) = ( v + 0 ) )
307 306 eleq1d 
 |-  ( z e. { 0 } -> ( ( v + z ) e. ( 0 ... k ) <-> ( v + 0 ) e. ( 0 ... k ) ) )
308 304 307 syl5ibrcom 
 |-  ( v e. ( 0 ..^ k ) -> ( z e. { 0 } -> ( v + z ) e. ( 0 ... k ) ) )
309 299 308 jaod 
 |-  ( v e. ( 0 ..^ k ) -> ( ( z e. { 1 } \/ z e. { 0 } ) -> ( v + z ) e. ( 0 ... k ) ) )
310 294 309 syl5bi 
 |-  ( v e. ( 0 ..^ k ) -> ( z e. ( { 1 } u. { 0 } ) -> ( v + z ) e. ( 0 ... k ) ) )
311 310 imp 
 |-  ( ( v e. ( 0 ..^ k ) /\ z e. ( { 1 } u. { 0 } ) ) -> ( v + z ) e. ( 0 ... k ) )
312 311 adantl 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ ( v e. ( 0 ..^ k ) /\ z e. ( { 1 } u. { 0 } ) ) ) -> ( v + z ) e. ( 0 ... k ) )
313 dffn3 
 |-  ( ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) <-> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ran ( 1st ` ( G ` k ) ) )
314 269 313 sylib 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ran ( 1st ` ( G ` k ) ) )
315 314 7 fssd 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ( 0 ..^ k ) )
316 315 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ( 0 ..^ k ) )
317 fzfid 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( 1 ... N ) e. Fin )
318 312 316 174 317 317 274 off 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... k ) )
319 318 ffnd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) Fn ( 1 ... N ) )
320 270 271 mp1i 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 1 ... N ) X. { k } ) Fn ( 1 ... N ) )
321 269 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) )
322 174 ffnd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
323 eqidd 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( 1st ` ( G ` k ) ) ` m ) = ( ( 1st ` ( G ` k ) ) ` m ) )
324 eqidd 
 |-  ( ( ( ( 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 ) = ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) )
325 321 322 317 317 274 323 324 ofval 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` m ) = ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) )
326 276 adantl 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { k } ) ` m ) = k )
327 319 320 317 317 274 325 326 ofval 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 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 } ) ) ` m ) = ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) )
328 327 eleq1d 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( 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 } ) ) ` m ) e. RR <-> ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) e. RR ) )
329 228 328 sylanl1 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( 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 } ) ) ` m ) e. RR <-> ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) e. RR ) )
330 327 adantl3r 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 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 } ) ) ` m ) = ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) )
331 330 oveq2d 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) = ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) ) )
332 93 ad3antlr 
 |-  ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> C : ( 1 ... N ) --> ( 0 [,] 1 ) )
333 332 ffvelrnda 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. ( 0 [,] 1 ) )
334 39 333 sseldi 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. RR )
335 253 adantl3r 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) e. RR )
336 19 remetdval 
 |-  ( ( ( C ` m ) e. RR /\ ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) e. RR ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) ) ) )
337 334 335 336 syl2anc 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) ) ) )
338 251 recnd 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( 1st ` ( G ` k ) ) ` m ) e. CC )
339 176 recnd 
 |-  ( ( ( ( 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. CC )
340 209 ad3antlr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> k e. CC )
341 210 ad3antlr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> k =/= 0 )
342 338 339 340 341 divdird 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) = ( ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) + ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) )
343 107 recnd 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. CC )
344 343 adantlr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. CC )
345 344 179 subnegd 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) - -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) = ( ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) + ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) )
346 342 345 eqtr4d 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) = ( ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) - -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) )
347 346 oveq2d 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) - ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) ) = ( ( 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 ) ) ) )
348 347 adantl3r 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) - ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) ) = ( ( 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 ) ) ) )
349 334 recnd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. CC )
350 107 adantllr 
 |-  ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. RR )
351 350 adantlr 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. RR )
352 351 recnd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( 1st ` ( G ` k ) ) ` m ) / k ) e. CC )
353 179 adantl3r 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ 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 )
354 353 negcld 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ 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 )
355 349 352 354 subsubd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ 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 ) ) ) = ( ( ( 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 ) ) )
356 348 355 eqtrd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) - ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) ) / k ) ) = ( ( ( 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 ) ) )
357 356 fveq2d 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( abs ` ( ( C ` m ) - ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) ) + -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) ) )
358 331 337 357 3eqtrd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) = ( 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 ) ) ) )
359 358 adantl3r 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) = ( 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 ) ) ) )
360 83 2halvesd 
 |-  ( c e. RR+ -> ( ( c / 2 ) + ( c / 2 ) ) = c )
361 360 eqcomd 
 |-  ( c e. RR+ -> c = ( ( c / 2 ) + ( c / 2 ) ) )
362 361 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> c = ( ( c / 2 ) + ( c / 2 ) ) )
363 359 362 breq12d 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) < c <-> ( 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 ) ) ) )
364 329 363 anbi12d 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( ( 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 } ) ) ` m ) e. RR /\ ( ( C ` m ) ( ( abs o. - ) |` ( RR X. RR ) ) ( ( ( ( 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 } ) ) ` m ) ) < c ) <-> ( ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) ) + -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) ) < ( ( c / 2 ) + ( c / 2 ) ) ) ) )
365 293 364 bitrd 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) <-> ( ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) ) + -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) ) < ( ( c / 2 ) + ( c / 2 ) ) ) ) )
366 79 365 sylanl1 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) <-> ( ( ( ( ( 1st ` ( G ` k ) ) ` m ) + ( ( ( ( ( 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 ) ) + -u ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` m ) / k ) ) ) < ( ( c / 2 ) + ( c / 2 ) ) ) ) )
367 256 288 366 3imtr4d 
 |-  ( ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) /\ 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 ) ) ) ) -> ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) ) )
368 367 ralimdva 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( 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 ) ) ) ) -> A. m e. ( 1 ... N ) ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) ) )
369 simplr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> k e. NN )
370 elfznn0 
 |-  ( v e. ( 0 ... k ) -> v e. NN0 )
371 370 nn0red 
 |-  ( v e. ( 0 ... k ) -> v e. RR )
372 nndivre 
 |-  ( ( v e. RR /\ k e. NN ) -> ( v / k ) e. RR )
373 371 372 sylan 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> ( v / k ) e. RR )
374 elfzle1 
 |-  ( v e. ( 0 ... k ) -> 0 <_ v )
375 371 374 jca 
 |-  ( v e. ( 0 ... k ) -> ( v e. RR /\ 0 <_ v ) )
376 186 rpregt0d 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
377 divge0 
 |-  ( ( ( v e. RR /\ 0 <_ v ) /\ ( k e. RR /\ 0 < k ) ) -> 0 <_ ( v / k ) )
378 375 376 377 syl2an 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> 0 <_ ( v / k ) )
379 elfzle2 
 |-  ( v e. ( 0 ... k ) -> v <_ k )
380 379 adantr 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> v <_ k )
381 371 adantr 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> v e. RR )
382 1red 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> 1 e. RR )
383 186 adantl 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> k e. RR+ )
384 381 382 383 ledivmuld 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> ( ( v / k ) <_ 1 <-> v <_ ( k x. 1 ) ) )
385 209 mulid1d 
 |-  ( k e. NN -> ( k x. 1 ) = k )
386 385 breq2d 
 |-  ( k e. NN -> ( v <_ ( k x. 1 ) <-> v <_ k ) )
387 386 adantl 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> ( v <_ ( k x. 1 ) <-> v <_ k ) )
388 384 387 bitrd 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> ( ( v / k ) <_ 1 <-> v <_ k ) )
389 380 388 mpbird 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> ( v / k ) <_ 1 )
390 elicc01 
 |-  ( ( v / k ) e. ( 0 [,] 1 ) <-> ( ( v / k ) e. RR /\ 0 <_ ( v / k ) /\ ( v / k ) <_ 1 ) )
391 373 378 389 390 syl3anbrc 
 |-  ( ( v e. ( 0 ... k ) /\ k e. NN ) -> ( v / k ) e. ( 0 [,] 1 ) )
392 391 ancoms 
 |-  ( ( k e. NN /\ v e. ( 0 ... k ) ) -> ( v / k ) e. ( 0 [,] 1 ) )
393 elsni 
 |-  ( z e. { k } -> z = k )
394 393 oveq2d 
 |-  ( z e. { k } -> ( v / z ) = ( v / k ) )
395 394 eleq1d 
 |-  ( z e. { k } -> ( ( v / z ) e. ( 0 [,] 1 ) <-> ( v / k ) e. ( 0 [,] 1 ) ) )
396 392 395 syl5ibrcom 
 |-  ( ( k e. NN /\ v e. ( 0 ... k ) ) -> ( z e. { k } -> ( v / z ) e. ( 0 [,] 1 ) ) )
397 396 impr 
 |-  ( ( k e. NN /\ ( v e. ( 0 ... k ) /\ z e. { k } ) ) -> ( v / z ) e. ( 0 [,] 1 ) )
398 369 397 sylan 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ ( v e. ( 0 ... k ) /\ z e. { k } ) ) -> ( v / z ) e. ( 0 [,] 1 ) )
399 270 fconst 
 |-  ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k }
400 399 a1i 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k } )
401 398 318 400 317 317 274 off 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( 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 } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
402 401 ffnd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( 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 } ) ) Fn ( 1 ... N ) )
403 124 402 sylan 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( 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 } ) ) Fn ( 1 ... N ) )
404 368 403 jctild 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( 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 ) ) ) ) -> ( ( ( ( 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 } ) ) Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) ) ) )
405 2 eleq2i 
 |-  ( ( ( ( 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 } ) ) e. I <-> ( ( ( 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 } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) )
406 ovex 
 |-  ( 0 [,] 1 ) e. _V
407 406 43 elmap 
 |-  ( ( ( ( 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 } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) <-> ( ( ( 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 } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
408 405 407 bitri 
 |-  ( ( ( ( 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 } ) ) e. I <-> ( ( ( 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 } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
409 401 408 sylibr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( 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 } ) ) e. I )
410 124 409 sylan 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( 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 } ) ) e. I )
411 404 410 jctird 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( 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 ) ) ) ) -> ( ( ( ( ( 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 } ) ) Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) ) /\ ( ( ( 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 } ) ) e. I ) ) )
412 elin 
 |-  ( ( ( ( 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 } ) ) e. ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) <-> ( ( ( ( 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 } ) ) e. X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) /\ ( ( ( 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 } ) ) e. I ) )
413 ovex 
 |-  ( ( ( 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 } ) ) e. _V
414 413 elixp 
 |-  ( ( ( ( 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 } ) ) e. X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) <-> ( ( ( ( 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 } ) ) Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) ) )
415 414 anbi1i 
 |-  ( ( ( ( ( 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 } ) ) e. X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) /\ ( ( ( 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 } ) ) e. I ) <-> ( ( ( ( ( 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 } ) ) Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) ) /\ ( ( ( 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 } ) ) e. I ) )
416 412 415 bitri 
 |-  ( ( ( ( 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 } ) ) e. ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) <-> ( ( ( ( ( 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 } ) ) Fn ( 1 ... N ) /\ A. m e. ( 1 ... N ) ( ( ( ( 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 } ) ) ` m ) e. ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) ) /\ ( ( ( 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 } ) ) e. I ) )
417 411 416 syl6ibr 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( 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 ) ) ) ) -> ( ( ( 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 } ) ) e. ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) ) )
418 ssel 
 |-  ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> ( ( ( ( 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 } ) ) e. ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) -> ( ( ( 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 } ) ) e. v ) )
419 418 com12 
 |-  ( ( ( ( 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 } ) ) e. ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) -> ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> ( ( ( 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 } ) ) e. v ) )
420 417 419 syl6 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( 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 ) ) ) ) -> ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> ( ( ( 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 } ) ) e. v ) ) )
421 420 impd 
 |-  ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( 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 ) ) ) ) /\ ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v ) -> ( ( ( 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 } ) ) e. v ) )
422 421 ralrimdva 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ 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 ) ) ) ) /\ ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v ) -> A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v ) )
423 422 expd 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ 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 ) ) ) ) -> ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v ) ) )
424 8 3exp2 
 |-  ( ph -> ( k e. NN -> ( n e. ( 1 ... N ) -> ( r e. { <_ , `' <_ } -> E. j e. ( 0 ... N ) 0 r X ) ) ) )
425 424 imp43 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> E. j e. ( 0 ... N ) 0 r X )
426 r19.29 
 |-  ( ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v /\ E. j e. ( 0 ... N ) 0 r X ) -> E. j e. ( 0 ... N ) ( ( ( ( 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 } ) ) e. v /\ 0 r X ) )
427 fveq2 
 |-  ( z = ( ( ( 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 } ) ) -> ( F ` z ) = ( 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 } ) ) ) )
428 427 fveq1d 
 |-  ( z = ( ( ( 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 } ) ) -> ( ( F ` z ) ` n ) = ( ( 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 ) )
429 428 5 eqtr4di 
 |-  ( z = ( ( ( 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 } ) ) -> ( ( F ` z ) ` n ) = X )
430 429 breq2d 
 |-  ( z = ( ( ( 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 } ) ) -> ( 0 r ( ( F ` z ) ` n ) <-> 0 r X ) )
431 430 rspcev 
 |-  ( ( ( ( ( 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 } ) ) e. v /\ 0 r X ) -> E. z e. v 0 r ( ( F ` z ) ` n ) )
432 431 rexlimivw 
 |-  ( E. j e. ( 0 ... N ) ( ( ( ( 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 } ) ) e. v /\ 0 r X ) -> E. z e. v 0 r ( ( F ` z ) ` n ) )
433 426 432 syl 
 |-  ( ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v /\ E. j e. ( 0 ... N ) 0 r X ) -> E. z e. v 0 r ( ( F ` z ) ` n ) )
434 433 expcom 
 |-  ( E. j e. ( 0 ... N ) 0 r X -> ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v -> E. z e. v 0 r ( ( F ` z ) ` n ) ) )
435 425 434 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v -> E. z e. v 0 r ( ( F ` z ) ` n ) ) )
436 435 ralrimdvva 
 |-  ( ( ph /\ k e. NN ) -> ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
437 122 436 sylan2 
 |-  ( ( ph /\ ( c e. RR+ /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) ) -> ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
438 437 anassrs 
 |-  ( ( ( ph /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
439 438 adantllr 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. ( ZZ>= ` -u ( |_ ` -u ( 2 / c ) ) ) ) -> ( A. j e. ( 0 ... N ) ( ( ( 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 } ) ) e. v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
440 423 439 syl6d 
 |-  ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ 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 ) ) ) ) -> ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
441 440 rexlimdva 
 |-  ( ( ( ph /\ C e. I ) /\ c e. RR+ ) -> ( 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 ) ) ) ) -> ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
442 74 441 syld 
 |-  ( ( ( 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 ) ) -> ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
443 442 com23 
 |-  ( ( ( ph /\ C e. I ) /\ c e. RR+ ) -> ( ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v -> ( 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. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
444 443 impr 
 |-  ( ( ( ph /\ C e. I ) /\ ( c e. RR+ /\ ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v ) ) -> ( 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. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
445 51 444 sylanl2 
 |-  ( ( ( ph /\ ( v e. ( R |`t I ) /\ C e. v ) ) /\ ( c e. RR+ /\ ( X_ m e. ( 1 ... N ) ( ( C ` m ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) c ) i^i I ) C_ v ) ) -> ( 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. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
446 35 445 rexlimddv 
 |-  ( ( ph /\ ( v e. ( R |`t I ) /\ C e. v ) ) -> ( 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. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
447 446 expr 
 |-  ( ( ph /\ v e. ( R |`t I ) ) -> ( C e. v -> ( 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. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
448 447 com23 
 |-  ( ( ph /\ v e. ( R |`t I ) ) -> ( 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 ) ) -> ( C e. v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
449 r19.21v 
 |-  ( A. n e. ( 1 ... N ) ( C e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) <-> ( C e. v -> A. n e. ( 1 ... N ) A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
450 448 449 syl6ibr 
 |-  ( ( ph /\ v e. ( R |`t I ) ) -> ( 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 ) ( C e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
451 450 ralrimdva 
 |-  ( 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. v e. ( R |`t I ) A. n e. ( 1 ... N ) ( C e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )
452 ralcom 
 |-  ( A. v e. ( R |`t I ) A. n e. ( 1 ... N ) ( C e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) <-> A. n e. ( 1 ... N ) A. v e. ( R |`t I ) ( C e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) )
453 451 452 syl6ib 
 |-  ( 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. ( R |`t I ) ( C e. v -> A. r e. { <_ , `' <_ } E. z e. v 0 r ( ( F ` z ) ` n ) ) ) )