Theorem axlowdim 25804

Description: The general lower dimensional 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", by Alfred Tarski and Steven Givant, Bull. 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 10025	. . . . . . . 8 |- 2 e. RR
2		3re 10027	. . . . . . . 8 |- 3 e. RR
3		2lt3 10099	. . . . . . . 8 |- 2 < 3
4	1, 2, 3	ltleii 9152	. . . . . . 7 |- 2 <_ 3
5		2z 10268	. . . . . . . 8 |- 2 e. ZZ
6		3nn 10090	. . . . . . . . 9 |- 3 e. NN
7	6	nnzi 10261	. . . . . . . 8 |- 3 e. ZZ
8		eluz 10455	. . . . . . . 8 |- ( ( 2 e. ZZ /\ 3 e. ZZ ) -> ( 3 e. ( ZZ>= ` 2 ) <-> 2 <_ 3 ) )
9	5, 7, 8	mp2an 654	. . . . . . 7 |- ( 3 e. ( ZZ>= ` 2 ) <-> 2 <_ 3 )
10	4, 9	mpbir 201	. . . . . 6 |- 3 e. ( ZZ>= ` 2 )
11		uzss 10462	. . . . . 6 |- ( 3 e. ( ZZ>= ` 2 ) -> ( ZZ>= ` 3 ) C_ ( ZZ>= ` 2 ) )
12	10, 11	ax-mp 8	. . . . 5 |- ( ZZ>= ` 3 ) C_ ( ZZ>= ` 2 )
13	12	sseli 3304	. . . 4 |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
14		0re 9047	. . . . 5 |- 0 e. RR
15	14, 14	axlowdimlem5 25789	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
16	13, 15	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
17		1re 9046	. . . . 5 |- 1 e. RR
18	17, 14	axlowdimlem5 25789	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
19	13, 18	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
20	14, 17	axlowdimlem5 25789	. . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
21	13, 20	syl 16	. . 3 |- ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
22		eqid 2404	. . . 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 } ) ) ) )
23	22	axlowdimlem15 25799	. . 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 ) )
24		eqid 2404	. . . . . 6 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
25		eqid 2404	. . . . . 6 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
26		eqid 2404	. . . . . 6 |- ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
27	24, 25, 26, 14, 14	axlowdimlem17 25801	. . . . 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 } ) ) >. )
28		eqid 2404	. . . . . 6 |- ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
29	24, 25, 28, 17, 14	axlowdimlem17 25801	. . . . 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 } ) ) >. )
30		eqid 2404	. . . . . 6 |- ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) = ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) )
31	24, 25, 30, 14, 17	axlowdimlem17 25801	. . . . 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 } ) ) >. )
32		1z 10267	. . . . . . . . . . . . . . 15 |- 1 e. ZZ
33	32	a1i 11	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 e. ZZ )
34		peano2zm 10276	. . . . . . . . . . . . . . 15 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )
35	34	3ad2ant2 979	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( N - 1 ) e. ZZ )
36		2m1e1 10051	. . . . . . . . . . . . . . 15 |- ( 2 - 1 ) = 1
37		zre 10242	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. ZZ -> N e. RR )
38		letr 9123	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. RR /\ 3 e. RR /\ N e. RR ) -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
39	1, 2, 38	mp3an12 1269	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. RR -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
40	37, 39	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> ( ( 2 <_ 3 /\ 3 <_ N ) -> 2 <_ N ) )
41	4, 40	mpani 658	. . . . . . . . . . . . . . . . . 18 |- ( N e. ZZ -> ( 3 <_ N -> 2 <_ N ) )
42	41	imp 419	. . . . . . . . . . . . . . . . 17 |- ( ( N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
43	42	3adant1 975	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 2 <_ N )
44	37	3ad2ant2 979	. . . . . . . . . . . . . . . . 17 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> N e. RR )
45		lesub1 9478	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR /\ N e. RR /\ 1 e. RR ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
46	1, 17, 45	mp3an13 1270	. . . . . . . . . . . . . . . . 17 |- ( N e. RR -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
47	44, 46	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 <_ N <-> ( 2 - 1 ) <_ ( N - 1 ) ) )
48	43, 47	mpbid 202	. . . . . . . . . . . . . . 15 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 2 - 1 ) <_ ( N - 1 ) )
49	36, 48	syl5eqbrr 4206	. . . . . . . . . . . . . 14 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 1 <_ ( N - 1 ) )
50	33, 35, 49	3jca 1134	. . . . . . . . . . . . 13 |- ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
51		eluz2 10450	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
52		eluz2 10450	. . . . . . . . . . . . 13 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 <_ ( N - 1 ) ) )
53	50, 51, 52	3imtr4i 258	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ( ZZ>= ` 1 ) )
54		eluzfz1 11020	. . . . . . . . . . . 12 |- ( ( N - 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
55	53, 54	syl 16	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ... ( N - 1 ) ) )
56	55	adantr 452	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> 1 e. ( 1 ... ( N - 1 ) ) )
57		eqeq1 2410	. . . . . . . . . . . 12 |- ( k = 1 -> ( k = 1 <-> 1 = 1 ) )
58		oveq1 6047	. . . . . . . . . . . . . . 15 |- ( k = 1 -> ( k + 1 ) = ( 1 + 1 ) )
59	58	opeq1d 3950	. . . . . . . . . . . . . 14 |- ( k = 1 -> <. ( k + 1 ) , 1 >. = <. ( 1 + 1 ) , 1 >. )
60	59	sneqd 3787	. . . . . . . . . . . . 13 |- ( k = 1 -> { <. ( k + 1 ) , 1 >. } = { <. ( 1 + 1 ) , 1 >. } )
61	58	sneqd 3787	. . . . . . . . . . . . . . 15 |- ( k = 1 -> { ( k + 1 ) } = { ( 1 + 1 ) } )
62	61	difeq2d 3425	. . . . . . . . . . . . . 14 |- ( k = 1 -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( 1 + 1 ) } ) )
63	62	xpeq1d 4860	. . . . . . . . . . . . 13 |- ( k = 1 -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) )
64	60, 63	uneq12d 3462	. . . . . . . . . . . 12 |- ( k = 1 -> ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) = ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) )
65	57, 64	ifbieq2d 3719	. . . . . . . . . . 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 } ) ) ) )
66		snex 4365	. . . . . . . . . . . . 13 |- { <. 3 , -u 1 >. } e. _V
67		ovex 6065	. . . . . . . . . . . . . . 15 |- ( 1 ... N ) e. _V
68		difexg 4311	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { 3 } ) e. _V )
69	67, 68	ax-mp 8	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { 3 } ) e. _V
70		snex 4365	. . . . . . . . . . . . . 14 |- { 0 } e. _V
71	69, 70	xpex 4949	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) e. _V
72	66, 71	unex 4666	. . . . . . . . . . . 12 |- ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) e. _V
73		snex 4365	. . . . . . . . . . . . 13 |- { <. ( 1 + 1 ) , 1 >. } e. _V
74		difexg 4311	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { ( 1 + 1 ) } ) e. _V )
75	67, 74	ax-mp 8	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { ( 1 + 1 ) } ) e. _V
76	75, 70	xpex 4949	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) e. _V
77	73, 76	unex 4666	. . . . . . . . . . . 12 |- ( { <. ( 1 + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( 1 + 1 ) } ) X. { 0 } ) ) e. _V
78	72, 77	ifex 3757	. . . . . . . . . . 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
79	65, 22, 78	fvmpt 5765	. . . . . . . . . 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 } ) ) ) )
80	56, 79	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 } ) ) ) )
81		eqid 2404	. . . . . . . . . 10 |- 1 = 1
82		iftrue 3705	. . . . . . . . . 10 |- ( 1 = 1 -> 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 } ) ) )
83	81, 82	ax-mp 8	. . . . . . . . 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 } ) )
84	80, 83	syl6eq 2452	. . . . . . . 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 } ) ) )
85	84	opeq1d 3950	. . . . . . 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 } ) ) >. )
86		2nn 10089	. . . . . . . . . . . . . 14 |- 2 e. NN
87		nnuz 10477	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` 1 )
88	86, 87	eleqtri 2476	. . . . . . . . . . . . 13 |- 2 e. ( ZZ>= ` 1 )
89		fzss1 11047	. . . . . . . . . . . . 13 |- ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) ) )
90	88, 89	ax-mp 8	. . . . . . . . . . . 12 |- ( 2 ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) )
91	90	sseli 3304	. . . . . . . . . . 11 |- ( i e. ( 2 ... ( N - 1 ) ) -> i e. ( 1 ... ( N - 1 ) ) )
92	91	adantl 453	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> i e. ( 1 ... ( N - 1 ) ) )
93		eqeq1 2410	. . . . . . . . . . . 12 |- ( k = i -> ( k = 1 <-> i = 1 ) )
94		oveq1 6047	. . . . . . . . . . . . . . 15 |- ( k = i -> ( k + 1 ) = ( i + 1 ) )
95	94	opeq1d 3950	. . . . . . . . . . . . . 14 |- ( k = i -> <. ( k + 1 ) , 1 >. = <. ( i + 1 ) , 1 >. )
96	95	sneqd 3787	. . . . . . . . . . . . 13 |- ( k = i -> { <. ( k + 1 ) , 1 >. } = { <. ( i + 1 ) , 1 >. } )
97	94	sneqd 3787	. . . . . . . . . . . . . . 15 |- ( k = i -> { ( k + 1 ) } = { ( i + 1 ) } )
98	97	difeq2d 3425	. . . . . . . . . . . . . 14 |- ( k = i -> ( ( 1 ... N ) \ { ( k + 1 ) } ) = ( ( 1 ... N ) \ { ( i + 1 ) } ) )
99	98	xpeq1d 4860	. . . . . . . . . . . . 13 |- ( k = i -> ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) = ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) )
100	96, 99	uneq12d 3462	. . . . . . . . . . . 12 |- ( k = i -> ( { <. ( k + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( k + 1 ) } ) X. { 0 } ) ) = ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) )
101	93, 100	ifbieq2d 3719	. . . . . . . . . . 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 } ) ) ) )
102		snex 4365	. . . . . . . . . . . . 13 |- { <. ( i + 1 ) , 1 >. } e. _V
103		difexg 4311	. . . . . . . . . . . . . . 15 |- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { ( i + 1 ) } ) e. _V )
104	67, 103	ax-mp 8	. . . . . . . . . . . . . 14 |- ( ( 1 ... N ) \ { ( i + 1 ) } ) e. _V
105	104, 70	xpex 4949	. . . . . . . . . . . . 13 |- ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) e. _V
106	102, 105	unex 4666	. . . . . . . . . . . 12 |- ( { <. ( i + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( i + 1 ) } ) X. { 0 } ) ) e. _V
107	72, 106	ifex 3757	. . . . . . . . . . 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
108	101, 22, 107	fvmpt 5765	. . . . . . . . . 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 } ) ) ) )
109	92, 108	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 } ) ) ) )
110		1lt2 10098	. . . . . . . . . . . . . . . 16 |- 1 < 2
111	17, 1	ltnlei 9150	. . . . . . . . . . . . . . . 16 |- ( 1 < 2 <-> -. 2 <_ 1 )
112	110, 111	mpbi 200	. . . . . . . . . . . . . . 15 |- -. 2 <_ 1
113	112	intnanr 882	. . . . . . . . . . . . . 14 |- -. ( 2 <_ 1 /\ 1 <_ ( N - 1 ) )
114		eluzelz 10452	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
115	114, 34	syl 16	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ZZ )
116		elfz 11005	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. ZZ /\ 2 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
117	32, 5, 116	mp3an12 1269	. . . . . . . . . . . . . . 15 |- ( ( N - 1 ) e. ZZ -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
118	115, 117	syl 16	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 3 ) -> ( 1 e. ( 2 ... ( N - 1 ) ) <-> ( 2 <_ 1 /\ 1 <_ ( N - 1 ) ) ) )
119	113, 118	mtbiri 295	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 3 ) -> -. 1 e. ( 2 ... ( N - 1 ) ) )
120		eleq1 2464	. . . . . . . . . . . . . 14 |- ( i = 1 -> ( i e. ( 2 ... ( N - 1 ) ) <-> 1 e. ( 2 ... ( N - 1 ) ) ) )
121	120	notbid 286	. . . . . . . . . . . . 13 |- ( i = 1 -> ( -. i e. ( 2 ... ( N - 1 ) ) <-> -. 1 e. ( 2 ... ( N - 1 ) ) ) )
122	119, 121	syl5ibrcom 214	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 3 ) -> ( i = 1 -> -. i e. ( 2 ... ( N - 1 ) ) ) )
123	122	con2d 109	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 3 ) -> ( i e. ( 2 ... ( N - 1 ) ) -> -. i = 1 ) )
124	123	imp 419	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 3 ) /\ i e. ( 2 ... ( N - 1 ) ) ) -> -. i = 1 )
125		iffalse 3706	. . . . . . . . . 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 } ) ) )
126	124, 125	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 } ) ) )
127	109, 126	eqtrd 2436	. . . . . . . 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 } ) ) )
128	127	opeq1d 3950	. . . . . . 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 } ) ) >. )
129	85, 128	breq12d 4185	. . . . . 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 } ) ) >. ) )
130	84	opeq1d 3950	. . . . . . 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 } ) ) >. )
131	127	opeq1d 3950	. . . . . . 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 } ) ) >. )
132	130, 131	breq12d 4185	. . . . . 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 } ) ) >. ) )
133	55, 79	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 } ) ) ) )
134	133, 83	syl6eq 2452	. . . . . . . . 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 } ) ) )
135	134	opeq1d 3950	. . . . . . . 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 } ) ) >. )
136	135	adantr 452	. . . . . . 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 } ) ) >. )
137	127	opeq1d 3950	. . . . . . 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 } ) ) >. )
138	136, 137	breq12d 4185	. . . . . 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 } ) ) >. ) )
139	129, 132, 138	3anbi123d 1254	. . . . 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 } ) ) >. ) ) )
140	27, 29, 31, 139	mpbir3and 1137	. . . 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 } ) ) >. ) )
141	140	ralrimiva 2749	. . 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 } ) ) >. ) )
142	26, 28, 30	axlowdimlem6 25790	. . . 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 } ) ) >. ) )
143	13, 142	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 } ) ) >. ) )
144		opeq2 3945	. . . . . . . 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 } ) ) >. )
145		opeq2 3945	. . . . . . . 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 } ) ) >. )
146	144, 145	breq12d 4185	. . . . . . 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 } ) ) >. ) )
147	146	3anbi1d 1258	. . . . . 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 >. ) ) )
148	147	ralbidv 2686	. . . . 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 >. ) ) )
149		breq1 4175	. . . . . . 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 >. ) )
150		opeq2 3945	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. z , x >. = <. z , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >. )
151	150	breq2d 4184	. . . . . . 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 } ) ) >. ) )
152		opeq1 3944	. . . . . . . 8 |- ( x = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) -> <. x , y >. = <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , y >. )
153	152	breq2d 4184	. . . . . . 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 >. ) )
154	149, 151, 153	3orbi123d 1253	. . . . . 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 >. ) ) )
155	154	notbid 286	. . . . 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 >. ) ) )
156	148, 155	3anbi23d 1257	. . . 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