Theorem axlowdim 24990

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 11207	. . . 4 |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
2		0re 9651	. . . . 5 |- 0 e. RR
3	2, 2	axlowdimlem5 24975	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
4	1, 3	syl 17	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
5		1re 9650	. . . . 5 |- 1 e. RR
6	5, 2	axlowdimlem5 24975	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
7	1, 6	syl 17	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
8	2, 5	axlowdimlem5 24975	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
9	1, 8	syl 17	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
10		eqid 2422	. . . 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 24985	. . 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 2422	. . . . . 6 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
13		eqid 2422	. . . . . 6 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
14		eqid 2422	. . . . . 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 24987	. . . . 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 2422	. . . . . 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 24987	. . . . 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 2422	. . . . . 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 24987	. . . . 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 10976	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 e. ZZ )
21		peano2zm 10988	. . . . . . . . . . . . . . 15 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )
22	21	3ad2ant2 1027	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( N - 1 ) e. ZZ )
23		2m1e1 10732	. . . . . . . . . . . . . . 15 |- ( 2 - 1 ) = 1
24		2re 10687	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
25		3re 10691	. . . . . . . . . . . . . . . . . . . 20 |- 3 e. RR
26		2lt3 10785	. . . . . . . . . . . . . . . . . . . 20 |- 2 < 3
27	24, 25, 26	ltleii 9765	. . . . . . . . . . . . . . . . . . 19 |- 2 <_ 3
28		zre 10949	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. ZZ -> N e. RR )
29		letr 9735	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. RR /\ 3 e. RR /\ N e. RR ) -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
30	24, 25, 29	mp3an12 1350	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. RR -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
31	28, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
32	27, 31	mpani 680	. . . . . . . . . . . . . . . . . 18 |- ( N e. ZZ -> ( 3 <_ N -> 2 <_ N ) )
33	32	imp 430	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
34	33	3adant1 1023	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
35	28	3ad2ant2 1027	. . . . . . . . . . . . . . . . 17 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> N e. RR )
36		lesub1 10116	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR /\ N e. RR /\ 1 e. RR ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
37	24, 5, 36	mp3an13 1351	. . . . . . . . . . . . . . . . 17 |- ( N e. RR -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
38	35, 37	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
39	34, 38	mpbid 213	. . . . . . . . . . . . . . 15 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 - 1 ) <_ ( N - 1 ) )
40	23, 39	syl5eqbrr 4458	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 <_ ( N - 1 ) )
41	20, 22, 40	3jca 1185	. . . . . . . . . . . . 13 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
42		eluz2 11173	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
43		eluz2 11173	. . . . . . . . . . . . 13 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
44	41, 42, 43	3imtr4i 269	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ( ZZ>= ` 1 ) )
45		eluzfz1 11814	. . . . . . . . . . . 12 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
46	44, 45	syl 17	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
47	46	adantr 466	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> 1 e. ( 1 ... ( N - 1 ) ) )
48		eqeq1 2426	. . . . . . . . . . . 12 |- ( k = 1 -> ( k = 1 <-> 1 = 1 ) )
49		oveq1 6313	. . . . . . . . . . . . . . 15 |- ( k = 1 -> ( k + 1 ) = ( 1 + 1 ) )
50	49	opeq1d 4193	. . . . . . . . . . . . . 14 |- ( k = 1 -> <. ( k + 1 ) , 1 >. = <. ( 1 + 1 ) , 1 >. )
51	50	sneqd 4010	. . . . . . . . . . . . 13 |- ( k = 1 -> { <. ( k + 1 ) , 1 >. } = { <. ( 1 + 1 ) , 1 >. } )
52	49	sneqd 4010	. . . . . . . . . . . . . . 15 |- ( k = 1 -> { ( k + 1 ) } = { ( 1 + 1 ) } )
53	52	difeq2d 3583	. . . . . . . . . . . . . 14 |- ( k = 1 -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( 1 + 1 ) } ) )
54	53	xpeq1d 4876	. . . . . . . . . . . . 13 |- ( k = 1 -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) )
55	51, 54	uneq12d 3621	. . . . . . . . . . . 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 3936	. . . . . . . . . . 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 4662	. . . . . . . . . . . . 13 |- { <. 3 , -u 1 >. } e. _V
58		ovex 6334	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) e. _V
59		difexg 4572	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { 3 } ) e. _V )
60	58, 59	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { 3 } ) e. _V
61		snex 4662	. . . . . . . . . . . . . 14 |- { 0 } e. _V
62	60, 61	xpex 6610	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) e. _V
63	57, 62	unex 6604	. . . . . . . . . . . 12 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. _V
64		snex 4662	. . . . . . . . . . . . 13 |- { <. ( 1 + 1 ) , 1 >. } e. _V
65		difexg 4572	. . . . . . . . . . . . . . 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 6610	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) e. _V
68	64, 67	unex 6604	. . . . . . . . . . . 12 |- ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) e. _V
69	63, 68	ifex 3979	. . . . . . . . . . 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 5965	. . . . . . . . . 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 17	. . . . . . . . 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 2422	. . . . . . . . . 10 |- 1 = 1
73	72	iftruei 3918	. . . . . . . . 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 2479	. . . . . . . 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 4193	. . . . . . 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 11213	. . . . . . . . . . . . 13 |- 2 e. ( ZZ>= ` 1 )
77		fzss1 11845	. . . . . . . . . . . . 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 3460	. . . . . . . . . . 11 |- ( i e. ( 2 ... ( N - 1 ) ) -> i e. ( 1 ... ( N - 1 ) ) )
80	79	adantl 467	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> i e. ( 1 ... ( N - 1 ) ) )
81		eqeq1 2426	. . . . . . . . . . . 12 |- ( k = i -> ( k = 1 <-> i = 1 ) )
82		oveq1 6313	. . . . . . . . . . . . . . 15 |- ( k = i -> ( k + 1 ) = ( i + 1 ) )
83	82	opeq1d 4193	. . . . . . . . . . . . . 14 |- ( k = i -> <. ( k + 1 ) , 1 >. = <. ( i + 1 ) , 1 >. )
84	83	sneqd 4010	. . . . . . . . . . . . 13 |- ( k = i -> { <. ( k + 1 ) , 1 >. } = { <. ( i + 1 ) , 1 >. } )
85	82	sneqd 4010	. . . . . . . . . . . . . . 15 |- ( k = i -> { ( k + 1 ) } = { ( i + 1 ) } )
86	85	difeq2d 3583	. . . . . . . . . . . . . 14 |- ( k = i -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( i + 1 ) } ) )
87	86	xpeq1d 4876	. . . . . . . . . . . . 13 |- ( k = i -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
88	84, 87	uneq12d 3621	. . . . . . . . . . . 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 3936	. . . . . . . . . . 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 4662	. . . . . . . . . . . . 13 |- { <. ( i + 1 ) , 1 >. } e. _V
91		difexg 4572	. . . . . . . . . . . . . . 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 6610	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) e. _V
94	90, 93	unex 6604	. . . . . . . . . . . 12 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) e. _V
95	63, 94	ifex 3979	. . . . . . . . . . 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 5965	. . . . . . . . . 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 17	. . . . . . . . 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 10784	. . . . . . . . . . . . . . . 16 |- 1 < 2
99	5, 24	ltnlei 9763	. . . . . . . . . . . . . . . 16 |- ( 1 < 2 <-> -. 2 <_ 1 )
100	98, 99	mpbi 211	. . . . . . . . . . . . . . 15 |- -. 2 <_ 1
101	100	intnanr 923	. . . . . . . . . . . . . 14 |- -. ( 2 <_ 1 /\ 1 <_ ( N - 1 ) )
102		eluzelz 11176	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
103	102, 21	syl 17	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ZZ )
104		1z 10975	. . . . . . . . . . . . . . . 16 |- 1 e. ZZ
105		2z 10977	. . . . . . . . . . . . . . . 16 |- 2 e. ZZ
106		elfz 11798	. . . . . . . . . . . . . . . 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 1350	. . . . . . . . . . . . . . 15 |- ( ( N - 1 ) e. ZZ -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
108	103, 107	syl 17	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 3 ) -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
109	101, 108	mtbiri 304	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) -> -. 1 e. ( 2 ... ( N - 1 ) ) )
110		eleq1 2495	. . . . . . . . . . . . . 14 |- ( i = 1 -> ( i e. ( 2 ... ( N - 1 ) ) <-> 1 e. ( 2 ... ( N - 1 ) ) ) )
111	110	notbid 295	. . . . . . . . . . . . 13 |- ( i = 1 -> ( -. i e. ( 2 ... ( N - 1 ) ) <-> -. 1 e. ( 2 ... ( N - 1 ) ) ) )
112	109, 111	syl5ibrcom 225	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( i = 1 -> -. i e. ( 2 ... ( N - 1 ) ) ) )
113	112	con2d 118	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> ( i e. ( 2 ... ( N - 1 ) ) -> -. i = 1 ) )
114	113	imp 430	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> -. i = 1 )
115	114	iffalsed 3922	. . . . . . . . 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 2463	. . . . . . . 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 4193	. . . . . . 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 4436	. . . . . 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 4193	. . . . . . 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 4193	. . . . . . 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 4436	. . . . . 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 17	. . . . . . . . . 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 2479	. . . . . . . . 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 4193	. . . . . . . 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 466	. . . . . . 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 4193	. . . . . . 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 4436	. . . . . 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 1335	. . . . 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 1188	. . . 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 2836	. . 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 24976	. . . 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 17	. . 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 4188	. . . . . . . 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 4188	. . . . . . . 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 4436	. . . . . . 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 1339	. . . . . 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 2861	. . . . 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 4426	. . . . . . 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 4188	. . . . . . . 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 4435	. . . . . . 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 4187	. . . . . . . 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 4435	. . . . . . 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 1334	. . . . . 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 295	. . . . 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 1338	. . . 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 4188	. . . . . . . 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 4188	. . . . . . . 8 |- ( y = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X.