Theorem axlowdim 23352

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		2re 10495	. . . . . . . 8 |- 2 e. RR
2		3re 10499	. . . . . . . 8 |- 3 e. RR
3		2lt3 10593	. . . . . . . 8 |- 2 < 3
4	1, 2, 3	ltleii 9601	. . . . . . 7 |- 2 <_ 3
5		2z 10782	. . . . . . . 8 |- 2 e. ZZ
6		3z 10783	. . . . . . . 8 |- 3 e. ZZ
7		eluz 10978	. . . . . . . 8 |- ( ( 2 e. ZZ /\ 3 e. ZZ ) -> ( 3 e. ( ZZ>= ` 2 ) <-> 2 <_ 3 ) )
8	5, 6, 7	mp2an 672	. . . . . . 7 |- ( 3 e. ( ZZ>= ` 2 ) <-> 2 <_ 3 )
9	4, 8	mpbir 209	. . . . . 6 |- 3 e. ( ZZ>= ` 2 )
10		uzss 10985	. . . . . 6 |- ( 3 e. ( ZZ>= ` 2 ) -> ( ZZ>= ` 3 ) C_ ( ZZ>= ` 2 ) )
11	9, 10	ax-mp 5	. . . . 5 |- ( ZZ>= ` 3 ) C_ ( ZZ>= ` 2 )
12	11	sseli 3453	. . . 4 |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
13		0re 9490	. . . . 5 |- 0 e. RR
14	13, 13	axlowdimlem5 23337	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
15	12, 14	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
16		1re 9489	. . . . 5 |- 1 e. RR
17	16, 13	axlowdimlem5 23337	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
18	12, 17	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
19	13, 16	axlowdimlem5 23337	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
20	12, 19	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
21		eqid 2451	. . . 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 } ) ) ) )
22	21	axlowdimlem15 23347	. . 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 ) )
23		eqid 2451	. . . . . 6 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
24		eqid 2451	. . . . . 6 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
25		eqid 2451	. . . . . 6 |- ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
26	23, 24, 25, 13, 13	axlowdimlem17 23349	. . . . 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 } ) ) >. )
27		eqid 2451	. . . . . 6 |- ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
28	23, 24, 27, 16, 13	axlowdimlem17 23349	. . . . 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 } ) ) >. )
29		eqid 2451	. . . . . 6 |- ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) )
30	23, 24, 29, 13, 16	axlowdimlem17 23349	. . . . 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 } ) ) >. )
31		1z 10780	. . . . . . . . . . . . . . 15 |- 1 e. ZZ
32	31	a1i 11	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 e. ZZ )
33		peano2zm 10792	. . . . . . . . . . . . . . 15 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )
34	33	3ad2ant2 1010	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( N - 1 ) e. ZZ )
35		2m1e1 10540	. . . . . . . . . . . . . . 15 |- ( 2 - 1 ) = 1
36		zre 10754	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. ZZ -> N e. RR )
37		letr 9572	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. RR /\ 3 e. RR /\ N e. RR ) -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
38	1, 2, 37	mp3an12 1305	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. RR -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
39	36, 38	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
40	4, 39	mpani 676	. . . . . . . . . . . . . . . . . 18 |- ( N e. ZZ -> ( 3 <_ N -> 2 <_ N ) )
41	40	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
42	41	3adant1 1006	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
43	36	3ad2ant2 1010	. . . . . . . . . . . . . . . . 17 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> N e. RR )
44		lesub1 9937	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR /\ N e. RR /\ 1 e. RR ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
45	1, 16, 44	mp3an13 1306	. . . . . . . . . . . . . . . . 17 |- ( N e. RR -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
46	43, 45	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
47	42, 46	mpbid 210	. . . . . . . . . . . . . . 15 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 - 1 ) <_ ( N - 1 ) )
48	35, 47	syl5eqbrr 4427	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 <_ ( N - 1 ) )
49	32, 34, 48	3jca 1168	. . . . . . . . . . . . 13 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
50		eluz2 10971	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
51		eluz2 10971	. . . . . . . . . . . . 13 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
52	49, 50, 51	3imtr4i 266	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ( ZZ>= ` 1 ) )
53		eluzfz1 11568	. . . . . . . . . . . 12 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
54	52, 53	syl 16	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
55	54	adantr 465	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> 1 e. ( 1 ... ( N - 1 ) ) )
56		eqeq1 2455	. . . . . . . . . . . 12 |- ( k = 1 -> ( k = 1 <-> 1 = 1 ) )
57		oveq1 6200	. . . . . . . . . . . . . . 15 |- ( k = 1 -> ( k + 1 ) = ( 1 + 1 ) )
58	57	opeq1d 4166	. . . . . . . . . . . . . 14 |- ( k = 1 -> <. ( k + 1 ) , 1 >. = <. ( 1 + 1 ) , 1 >. )
59	58	sneqd 3990	. . . . . . . . . . . . 13 |- ( k = 1 -> { <. ( k + 1 ) , 1 >. } = { <. ( 1 + 1 ) , 1 >. } )
60	57	sneqd 3990	. . . . . . . . . . . . . . 15 |- ( k = 1 -> { ( k + 1 ) } = { ( 1 + 1 ) } )
61	60	difeq2d 3575	. . . . . . . . . . . . . 14 |- ( k = 1 -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( 1 + 1 ) } ) )
62	61	xpeq1d 4964	. . . . . . . . . . . . 13 |- ( k = 1 -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) )
63	59, 62	uneq12d 3612	. . . . . . . . . . . 12 |- ( k = 1 -> ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) = ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) )
64	56, 63	ifbieq2d 3915	. . . . . . . . . . 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 } ) ) ) )
65		snex 4634	. . . . . . . . . . . . 13 |- { <. 3 , -u 1 >. } e. _V
66		ovex 6218	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) e. _V
67		difexg 4541	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { 3 } ) e. _V )
68	66, 67	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { 3 } ) e. _V
69		snex 4634	. . . . . . . . . . . . . 14 |- { 0 } e. _V
70	68, 69	xpex 6611	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) e. _V
71	65, 70	unex 6481	. . . . . . . . . . . 12 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. _V
72		snex 4634	. . . . . . . . . . . . 13 |- { <. ( 1 + 1 ) , 1 >. } e. _V
73		difexg 4541	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { ( 1 + 1 ) } ) e. _V )
74	66, 73	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { ( 1 + 1 ) } ) e. _V
75	74, 69	xpex 6611	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) e. _V
76	72, 75	unex 6481	. . . . . . . . . . . 12 |- ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) e. _V
77	71, 76	ifex 3959	. . . . . . . . . . 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
78	64, 21, 77	fvmpt 5876	. . . . . . . . . 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 } ) ) ) )
79	55, 78	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 } ) ) ) )
80		eqid 2451	. . . . . . . . . 10 |- 1 = 1
81	80	iftruei 3899	. . . . . . . . 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 } ) )
82	79, 81	syl6eq 2508	. . . . . . . 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 } ) ) )
83	82	opeq1d 4166	. . . . . . 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 } ) ) >. )
84		2nn 10583	. . . . . . . . . . . . . 14 |- 2 e. NN
85		nnuz 11000	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` 1 )
86	84, 85	eleqtri 2537	. . . . . . . . . . . . 13 |- 2 e. ( ZZ>= ` 1 )
87		fzss1 11607	. . . . . . . . . . . . 13 |- ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) ) )
88	86, 87	ax-mp 5	. . . . . . . . . . . 12 |- ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) )
89	88	sseli 3453	. . . . . . . . . . 11 |- ( i e. ( 2 ... ( N - 1 ) ) -> i e. ( 1 ... ( N - 1 ) ) )
90	89	adantl 466	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> i e. ( 1 ... ( N - 1 ) ) )
91		eqeq1 2455	. . . . . . . . . . . 12 |- ( k = i -> ( k = 1 <-> i = 1 ) )
92		oveq1 6200	. . . . . . . . . . . . . . 15 |- ( k = i -> ( k + 1 ) = ( i + 1 ) )
93	92	opeq1d 4166	. . . . . . . . . . . . . 14 |- ( k = i -> <. ( k + 1 ) , 1 >. = <. ( i + 1 ) , 1 >. )
94	93	sneqd 3990	. . . . . . . . . . . . 13 |- ( k = i -> { <. ( k + 1 ) , 1 >. } = { <. ( i + 1 ) , 1 >. } )
95	92	sneqd 3990	. . . . . . . . . . . . . . 15 |- ( k = i -> { ( k + 1 ) } = { ( i + 1 ) } )
96	95	difeq2d 3575	. . . . . . . . . . . . . 14 |- ( k = i -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( i + 1 ) } ) )
97	96	xpeq1d 4964	. . . . . . . . . . . . 13 |- ( k = i -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
98	94, 97	uneq12d 3612	. . . . . . . . . . . 12 |- ( k = i -> ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) )
99	91, 98	ifbieq2d 3915	. . . . . . . . . . 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 } ) ) ) )
100		snex 4634	. . . . . . . . . . . . 13 |- { <. ( i + 1 ) , 1 >. } e. _V
101		difexg 4541	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { ( i + 1 ) } ) e. _V )
102	66, 101	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { ( i + 1 ) } ) e. _V
103	102, 69	xpex 6611	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) e. _V
104	100, 103	unex 6481	. . . . . . . . . . . 12 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) e. _V
105	71, 104	ifex 3959	. . . . . . . . . . 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
106	99, 21, 105	fvmpt 5876	. . . . . . . . . 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 } ) ) ) )
107	90, 106	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 } ) ) ) )
108		1lt2 10592	. . . . . . . . . . . . . . . 16 |- 1 < 2
109	16, 1	ltnlei 9599	. . . . . . . . . . . . . . . 16 |- ( 1 < 2 <-> -. 2 <_ 1 )
110	108, 109	mpbi 208	. . . . . . . . . . . . . . 15 |- -. 2 <_ 1
111	110	intnanr 906	. . . . . . . . . . . . . 14 |- -. ( 2 <_ 1 /\ 1 <_ ( N - 1 ) )
112		eluzelz 10974	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
113	112, 33	syl 16	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ZZ )
114		elfz 11553	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. ZZ /\ 2 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
115	31, 5, 114	mp3an12 1305	. . . . . . . . . . . . . . 15 |- ( ( N - 1 ) e. ZZ -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
116	113, 115	syl 16	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 3 ) -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
117	111, 116	mtbiri 303	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) -> -. 1 e. ( 2 ... ( N - 1 ) ) )
118		eleq1 2523	. . . . . . . . . . . . . 14 |- ( i = 1 -> ( i e. ( 2 ... ( N - 1 ) ) <-> 1 e. ( 2 ... ( N - 1 ) ) ) )
119	118	notbid 294	. . . . . . . . . . . . 13 |- ( i = 1 -> ( -. i e. ( 2 ... ( N - 1 ) ) <-> -. 1 e. ( 2 ... ( N - 1 ) ) ) )
120	117, 119	syl5ibrcom 222	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( i = 1 -> -. i e. ( 2 ... ( N - 1 ) ) ) )
121	120	con2d 115	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> ( i e. ( 2 ... ( N - 1 ) ) -> -. i = 1 ) )
122	121	imp 429	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> -. i = 1 )
123		iffalse 3900	. . . . . . . . . 10 |- ( -. i = 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 } ) ) )
124	122, 123	syl 16	. . . . . . . . 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 } ) ) )
125	107, 124	eqtrd 2492	. . . . . . . 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 } ) ) )
126	125	opeq1d 4166	. . . . . . 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 } ) ) >. )
127	83, 126	breq12d 4406	. . . . . 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 } ) ) >. ) )
128	82	opeq1d 4166	. . . . . . 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 } ) ) >. )
129	125	opeq1d 4166	. . . . . . 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 } ) ) >. )
130	128, 129	breq12d 4406	. . . . . 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 } ) ) >. ) )
131	54, 78	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 } ) ) ) )
132	131, 81	syl6eq 2508	. . . . . . . . 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 } ) ) )
133	132	opeq1d 4166	. . . . . . . 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 } ) ) >. )
134	133	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 } ) ) >. )
135	125	opeq1d 4166	. . . . . . 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 } ) ) >. )
136	134, 135	breq12d 4406	. . . . . 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 } ) ) >. ) )
137	127, 130, 136	3anbi123d 1290	. . . . 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 } ) ) >. ) ) )
138	26, 28, 30, 137	mpbir3and 1171	. . . 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 } ) ) >. ) )
139	138	ralrimiva 2825	. . 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 } ) ) >. ) )
140	25, 27, 29	axlowdimlem6 23338	. . . 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 } ) ) >. ) )
141	12, 140	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 } ) ) >. ) )
142		opeq2 4161	. . . . . . . 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 } ) ) >. )
143		opeq2 4161	. . . . . . . 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 } ) ) >. )
144	142, 143	breq12d 4406	. . . . . . 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 } ) ) >. ) )
145	144	3anbi1d 1294	. . . . . 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 >. ) ) )
146	145	ralbidv 2841	. . . . 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 >. ) ) )
147		breq1 4396	. . . . . . 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 >. ) )
148		opeq2 4161	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. z , x >. = <. z , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
149	148	breq2d 4405	. . . . . . 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 } ) ) >. ) )
150		opeq1 4160	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. x , y >. = <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , y >. )
151	150	breq2d 4405	. . . . . . 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 >. ) )
152	147, 149, 151	3orbi123d 1289	. . . . . 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 >. ) ) )
153	152	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 >. ) ) )
154	146, 153	3anbi23d 1293	. . . 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 >. ) ) ) )
155		opeq2 4161	. . . . . . . 8 |- ( y = ( { <. 1 , 1 >. , <. 2 , 0