Theorem axlowdim 24390

Description: The general lower dimension axiom. Take a dimension N greater than or equal to three. Then, there are three non-colinear points in N dimensional space that are equidistant from N - 1 distinct points. Derived from remarks in Tarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.)

Assertion

Ref	Expression
axlowdim	|- ( N e. ( ZZ>= ` 3 ) -> E. p E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. z e. ( EE ` N ) ( p : ( 1 ... ( N - 1 ) ) -1-1-> ( EE ` N ) /\ A. i e. ( 2 ... ( N - 1 ) ) ( <. ( p ` 1 ) , x >.Cgr <. ( p ` i ) , x >. /\ <. ( p ` 1 ) , y >.Cgr <. ( p ` i ) , y >. /\ <. ( p ` 1 ) , z >.Cgr <. ( p ` i ) , z >. ) /\ -. ( x Btwn <. y , z >. \/ y Btwn <. z , x >. \/ z Btwn <. x , y >. ) ) )

Distinct variable group:   i, N, p, x, y, z

Proof of Theorem axlowdim

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		uzuzle23 11146	. . . 4 |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
2		0re 9613	. . . . 5 |- 0 e. RR
3	2, 2	axlowdimlem5 24375	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
4	1, 3	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
5		1re 9612	. . . . 5 |- 1 e. RR
6	5, 2	axlowdimlem5 24375	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
7	1, 6	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
8	2, 5	axlowdimlem5 24375	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
9	1, 8	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
10		eqid 2457	. . . 4 |- ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) = ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) )
11	10	axlowdimlem15 24385	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) : ( 1 ... ( N - 1 ) ) -1-1-> ( EE ` N ) )
12		eqid 2457	. . . . . 6 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
13		eqid 2457	. . . . . 6 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
14		eqid 2457	. . . . . 6 |- ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
15	12, 13, 14, 2, 2	axlowdimlem17 24387	. . . . 5 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
16		eqid 2457	. . . . . 6 |- ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
17	12, 13, 16, 5, 2	axlowdimlem17 24387	. . . . 5 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
18		eqid 2457	. . . . . 6 |- ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) )
19	12, 13, 18, 2, 5	axlowdimlem17 24387	. . . . 5 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
20		1zzd 10916	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 e. ZZ )
21		peano2zm 10928	. . . . . . . . . . . . . . 15 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )
22	21	3ad2ant2 1018	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( N - 1 ) e. ZZ )
23		2m1e1 10671	. . . . . . . . . . . . . . 15 |- ( 2 - 1 ) = 1
24		2re 10626	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
25		3re 10630	. . . . . . . . . . . . . . . . . . . 20 |- 3 e. RR
26		2lt3 10724	. . . . . . . . . . . . . . . . . . . 20 |- 2 < 3
27	24, 25, 26	ltleii 9724	. . . . . . . . . . . . . . . . . . 19 |- 2 <_ 3
28		zre 10889	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. ZZ -> N e. RR )
29		letr 9695	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. RR /\ 3 e. RR /\ N e. RR ) -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
30	24, 25, 29	mp3an12 1314	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. RR -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
31	28, 30	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
32	27, 31	mpani 676	. . . . . . . . . . . . . . . . . 18 |- ( N e. ZZ -> ( 3 <_ N -> 2 <_ N ) )
33	32	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
34	33	3adant1 1014	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
35	28	3ad2ant2 1018	. . . . . . . . . . . . . . . . 17 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> N e. RR )
36		lesub1 10067	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR /\ N e. RR /\ 1 e. RR ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
37	24, 5, 36	mp3an13 1315	. . . . . . . . . . . . . . . . 17 |- ( N e. RR -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
38	35, 37	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
39	34, 38	mpbid 210	. . . . . . . . . . . . . . 15 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 - 1 ) <_ ( N - 1 ) )
40	23, 39	syl5eqbrr 4490	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 <_ ( N - 1 ) )
41	20, 22, 40	3jca 1176	. . . . . . . . . . . . 13 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
42		eluz2 11112	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
43		eluz2 11112	. . . . . . . . . . . . 13 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
44	41, 42, 43	3imtr4i 266	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ( ZZ>= ` 1 ) )
45		eluzfz1 11718	. . . . . . . . . . . 12 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
46	44, 45	syl 16	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
47	46	adantr 465	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> 1 e. ( 1 ... ( N - 1 ) ) )
48		eqeq1 2461	. . . . . . . . . . . 12 |- ( k = 1 -> ( k = 1 <-> 1 = 1 ) )
49		oveq1 6303	. . . . . . . . . . . . . . 15 |- ( k = 1 -> ( k + 1 ) = ( 1 + 1 ) )
50	49	opeq1d 4225	. . . . . . . . . . . . . 14 |- ( k = 1 -> <. ( k + 1 ) , 1 >. = <. ( 1 + 1 ) , 1 >. )
51	50	sneqd 4044	. . . . . . . . . . . . 13 |- ( k = 1 -> { <. ( k + 1 ) , 1 >. } = { <. ( 1 + 1 ) , 1 >. } )
52	49	sneqd 4044	. . . . . . . . . . . . . . 15 |- ( k = 1 -> { ( k + 1 ) } = { ( 1 + 1 ) } )
53	52	difeq2d 3618	. . . . . . . . . . . . . 14 |- ( k = 1 -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( 1 + 1 ) } ) )
54	53	xpeq1d 5031	. . . . . . . . . . . . 13 |- ( k = 1 -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) )
55	51, 54	uneq12d 3655	. . . . . . . . . . . 12 |- ( k = 1 -> ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) = ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) )
56	48, 55	ifbieq2d 3969	. . . . . . . . . . 11 |- ( k = 1 -> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) = if ( 1 = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) ) )
57		snex 4697	. . . . . . . . . . . . 13 |- { <. 3 , -u 1 >. } e. _V
58		ovex 6324	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) e. _V
59		difexg 4604	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { 3 } ) e. _V )
60	58, 59	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { 3 } ) e. _V
61		snex 4697	. . . . . . . . . . . . . 14 |- { 0 } e. _V
62	60, 61	xpex 6603	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) e. _V
63	57, 62	unex 6597	. . . . . . . . . . . 12 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. _V
64		snex 4697	. . . . . . . . . . . . 13 |- { <. ( 1 + 1 ) , 1 >. } e. _V
65		difexg 4604	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { ( 1 + 1 ) } ) e. _V )
66	58, 65	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { ( 1 + 1 ) } ) e. _V
67	66, 61	xpex 6603	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) e. _V
68	64, 67	unex 6597	. . . . . . . . . . . 12 |- ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) e. _V
69	63, 68	ifex 4013	. . . . . . . . . . 11 |- if ( 1 = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) ) e. _V
70	56, 10, 69	fvmpt 5956	. . . . . . . . . 10 |- ( 1 e. ( 1 ... ( N - 1 ) ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) = if ( 1 = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) ) )
71	47, 70	syl 16	. . . . . . . . 9 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) = if ( 1 = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) ) )
72		eqid 2457	. . . . . . . . . 10 |- 1 = 1
73	72	iftruei 3951	. . . . . . . . 9 |- if ( 1 = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
74	71, 73	syl6eq 2514	. . . . . . . 8 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) )
75	74	opeq1d 4225	. . . . . . 7 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. = <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
76		2eluzge1 11152	. . . . . . . . . . . . 13 |- 2 e. ( ZZ>= ` 1 )
77		fzss1 11747	. . . . . . . . . . . . 13 |- ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) ) )
78	76, 77	ax-mp 5	. . . . . . . . . . . 12 |- ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) )
79	78	sseli 3495	. . . . . . . . . . 11 |- ( i e. ( 2 ... ( N - 1 ) ) -> i e. ( 1 ... ( N - 1 ) ) )
80	79	adantl 466	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> i e. ( 1 ... ( N - 1 ) ) )
81		eqeq1 2461	. . . . . . . . . . . 12 |- ( k = i -> ( k = 1 <-> i = 1 ) )
82		oveq1 6303	. . . . . . . . . . . . . . 15 |- ( k = i -> ( k + 1 ) = ( i + 1 ) )
83	82	opeq1d 4225	. . . . . . . . . . . . . 14 |- ( k = i -> <. ( k + 1 ) , 1 >. = <. ( i + 1 ) , 1 >. )
84	83	sneqd 4044	. . . . . . . . . . . . 13 |- ( k = i -> { <. ( k + 1 ) , 1 >. } = { <. ( i + 1 ) , 1 >. } )
85	82	sneqd 4044	. . . . . . . . . . . . . . 15 |- ( k = i -> { ( k + 1 ) } = { ( i + 1 ) } )
86	85	difeq2d 3618	. . . . . . . . . . . . . 14 |- ( k = i -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( i + 1 ) } ) )
87	86	xpeq1d 5031	. . . . . . . . . . . . 13 |- ( k = i -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
88	84, 87	uneq12d 3655	. . . . . . . . . . . 12 |- ( k = i -> ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) )
89	81, 88	ifbieq2d 3969	. . . . . . . . . . 11 |- ( k = i -> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) = if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) )
90		snex 4697	. . . . . . . . . . . . 13 |- { <. ( i + 1 ) , 1 >. } e. _V
91		difexg 4604	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { ( i + 1 ) } ) e. _V )
92	58, 91	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { ( i + 1 ) } ) e. _V
93	92, 61	xpex 6603	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) e. _V
94	90, 93	unex 6597	. . . . . . . . . . . 12 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) e. _V
95	63, 94	ifex 4013	. . . . . . . . . . 11 |- if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) e. _V
96	89, 10, 95	fvmpt 5956	. . . . . . . . . 10 |- ( i e. ( 1 ... ( N - 1 ) ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) = if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) )
97	80, 96	syl 16	. . . . . . . . 9 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) = if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) )
98		1lt2 10723	. . . . . . . . . . . . . . . 16 |- 1 < 2
99	5, 24	ltnlei 9722	. . . . . . . . . . . . . . . 16 |- ( 1 < 2 <-> -. 2 <_ 1 )
100	98, 99	mpbi 208	. . . . . . . . . . . . . . 15 |- -. 2 <_ 1
101	100	intnanr 915	. . . . . . . . . . . . . 14 |- -. ( 2 <_ 1 /\ 1 <_ ( N - 1 ) )
102		eluzelz 11115	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
103	102, 21	syl 16	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ZZ )
104		1z 10915	. . . . . . . . . . . . . . . 16 |- 1 e. ZZ
105		2z 10917	. . . . . . . . . . . . . . . 16 |- 2 e. ZZ
106		elfz 11703	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. ZZ /\ 2 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
107	104, 105, 106	mp3an12 1314	. . . . . . . . . . . . . . 15 |- ( ( N - 1 ) e. ZZ -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
108	103, 107	syl 16	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 3 ) -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
109	101, 108	mtbiri 303	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) -> -. 1 e. ( 2 ... ( N - 1 ) ) )
110		eleq1 2529	. . . . . . . . . . . . . 14 |- ( i = 1 -> ( i e. ( 2 ... ( N - 1 ) ) <-> 1 e. ( 2 ... ( N - 1 ) ) ) )
111	110	notbid 294	. . . . . . . . . . . . 13 |- ( i = 1 -> ( -. i e. ( 2 ... ( N - 1 ) ) <-> -. 1 e. ( 2 ... ( N - 1 ) ) ) )
112	109, 111	syl5ibrcom 222	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( i = 1 -> -. i e. ( 2 ... ( N - 1 ) ) ) )
113	112	con2d 115	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> ( i e. ( 2 ... ( N - 1 ) ) -> -. i = 1 ) )
114	113	imp 429	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> -. i = 1 )
115	114	iffalsed 3955	. . . . . . . . 9 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> if ( i = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) )
116	97, 115	eqtrd 2498	. . . . . . . 8 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) )
117	116	opeq1d 4225	. . . . . . 7 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. = <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
118	75, 117	breq12d 4469	. . . . . 6 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. <-> <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
119	74	opeq1d 4225	. . . . . . 7 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. = <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
120	116	opeq1d 4225	. . . . . . 7 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. = <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
121	119, 120	breq12d 4469	. . . . . 6 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. <-> <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
122	46, 70	syl 16	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` 3 ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) = if ( 1 = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) ) )
123	122, 73	syl6eq 2514	. . . . . . . . 9 |- ( N e. ( ZZ>= ` 3 ) -> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) )
124	123	opeq1d 4225	. . . . . . . 8 |- ( N e. ( ZZ>= ` 3 ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. = <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
125	124	adantr 465	. . . . . . 7 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. = <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
126	116	opeq1d 4225	. . . . . . 7 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. = <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
127	125, 126	breq12d 4469	. . . . . 6 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. <-> <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
128	118, 121, 127	3anbi123d 1299	. . . . 5 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) <-> ( <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) ) )
129	15, 17, 19, 128	mpbir3and 1179	. . . 4 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
130	129	ralrimiva 2871	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> A. i e. ( 2 ... ( N - 1 ) ) ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
131	14, 16, 18	axlowdimlem6 24376	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> -. ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. \/ ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. \/ ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
132	1, 131	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> -. ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. \/ ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. \/ ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
133		opeq2 4220	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , x >. = <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
134		opeq2 4220	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , x >. = <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
135	133, 134	breq12d 4469	. . . . . . 7 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , x >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , x >. <-> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
136	135	3anbi1d 1303	. . . . . 6 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , x >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , x >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , y >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , y >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , z >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , z >. ) <-> ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , y >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , y >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , z >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , z >. ) ) )
137	136	ralbidv 2896	. . . . 5 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( A. i e. ( 2 ... ( N - 1 ) ) ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , x >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , x >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , y >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , y >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , z >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , z >. ) <-> A. i e. ( 2 ... ( N - 1 ) ) ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , y >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , y >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , z >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , z >. ) ) )
138		breq1 4459	. . . . . . 7 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( x Btwn <. y , z >. <-> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. y , z >. ) )
139		opeq2 4220	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. z , x >. = <. z , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
140	139	breq2d 4468	. . . . . . 7 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( y Btwn <. z , x >. <-> y Btwn <. z , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. ) )
141		opeq1 4219	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. x , y >. = <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , y >. )
142	141	breq2d 4468	. . . . . . 7 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( z Btwn <. x , y >. <-> z Btwn <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , y >. ) )
143	138, 140, 142	3orbi123d 1298	. . . . . 6 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( ( x Btwn <. y , z >. \/ y Btwn <. z , x >. \/ z Btwn <. x , y >. ) <-> ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. y , z >. \/ y Btwn <. z , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. \/ z Btwn <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , y >. ) ) )
144	143	notbid 294	. . . . 5 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( -. ( x Btwn <. y , z >. \/ y Btwn <. z , x >. \/ z Btwn <. x , y >. ) <-> -. ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. y , z >. \/ y Btwn <. z , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. \/ z Btwn <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , y >. ) ) )
145	137, 144	3anbi23d 1302	. . . 4 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> ( ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) : ( 1 ... ( N - 1 ) ) -1-1-> ( EE ` N ) /\ A. i e. ( 2 ... ( N - 1 ) ) ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , x >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , x >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , y >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , y >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , z >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , z >. ) /\ -. ( x Btwn <. y , z >. \/ y Btwn <. z , x >. \/ z Btwn <. x , y >. ) ) <-> ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) : ( 1 ... ( N - 1 ) ) -1-1-> ( EE ` N ) /\ A. i e. ( 2 ... ( N - 1 ) ) ( <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , y >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , y >. /\ <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , z >.Cgr <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` i ) , z >. ) /\ -. ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) Btwn <. y , z >. \/ y Btwn <. z , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. \/ z Btwn <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , y >. ) ) ) )
146		opeq2 4220	. . . . . . . 8 |- ( y = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , y >. = <. ( ( k e. ( 1 ... ( N - 1 ) ) |-> if ( k = 1 , ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) , ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) ) ) ` 1 ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
147		opeq2 4220	. . . . . . . 8 |- ( y = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X.