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	imbitrrid	|- ( 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	ffvelcdmda	|- ( ( ( ( ( ( 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	sselid	|- ( ( ( ( ( ( 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	ffvelcdmda	|- ( ( 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	ffvelcdmda	|- ( ( ( 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	ffvelcdmda	|- ( ( ( ( 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	sselid	|- ( ( ( ( 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	ffvelcdmda	|- ( ( ( ( ( ph /\ C e. I ) /\ c e. RR+ ) /\ k e. NN ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. ( 0 [,] 1 ) )
260	39 259	sselid	|- ( ( ( ( ( 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	addridd	|- ( 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	biimtrid	|- ( 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	ffvelcdmda	|- ( ( ( ( ( ph /\ C e. I ) /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ m e. ( 1 ... N ) ) -> ( C ` m ) e. ( 0 [,] 1 ) )
334	39 333	sselid	|- ( ( ( ( ( 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	mulridd	|- ( 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	imbitrrdi	|- ( ( ( ( ( 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	imbitrrdi	|- ( ( 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	imbitrdi	|- ( 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 ) ) ) )