Metamath Proof Explorer

Theorem axlowdimlem6

Description: Lemma for axlowdim . Show that three points are non-colinear. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Hypotheses axlowdimlem6.1 
|- A = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
axlowdimlem6.2 
|- B = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
axlowdimlem6.3 
|- C = ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) )
Assertion axlowdimlem6 
|- ( N e. ( ZZ>= ` 2 ) -> -. ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem6.1 
 |-  A = ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
2 axlowdimlem6.2 
 |-  B = ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) )
3 axlowdimlem6.3 
 |-  C = ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) )
4 1zzd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. ZZ )
5 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
6 2nn 
 |-  2 e. NN
7 uznnssnn 
 |-  ( 2 e. NN -> ( ZZ>= ` 2 ) C_ NN )
8 6 7 ax-mp 
 |-  ( ZZ>= ` 2 ) C_ NN
9 nnuz 
 |-  NN = ( ZZ>= ` 1 )
10 8 9 sseqtri 
 |-  ( ZZ>= ` 2 ) C_ ( ZZ>= ` 1 )
11 10 sseli 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ( ZZ>= ` 1 ) )
12 eluzle 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 <_ N )
13 11 12 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 <_ N )
14 1re 
 |-  1 e. RR
15 14 leidi 
 |-  1 <_ 1
16 13 15 jctil 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 <_ 1 /\ 1 <_ N ) )
17 elfz4 
 |-  ( ( ( 1 e. ZZ /\ N e. ZZ /\ 1 e. ZZ ) /\ ( 1 <_ 1 /\ 1 <_ N ) ) -> 1 e. ( 1 ... N ) )
18 4 5 4 16 17 syl31anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. ( 1 ... N ) )
19 eluzel2 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. ZZ )
20 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
21 1le2 
 |-  1 <_ 2
22 20 21 jctil 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 <_ 2 /\ 2 <_ N ) )
23 elfz4 
 |-  ( ( ( 1 e. ZZ /\ N e. ZZ /\ 2 e. ZZ ) /\ ( 1 <_ 2 /\ 2 <_ N ) ) -> 2 e. ( 1 ... N ) )
24 4 5 19 22 23 syl31anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. ( 1 ... N ) )
25 ax-1ne0 
 |-  1 =/= 0
26 1t1e1 
 |-  ( 1 x. 1 ) = 1
27 0cn 
 |-  0 e. CC
28 27 mul01i 
 |-  ( 0 x. 0 ) = 0
29 26 28 neeq12i 
 |-  ( ( 1 x. 1 ) =/= ( 0 x. 0 ) <-> 1 =/= 0 )
30 25 29 mpbir 
 |-  ( 1 x. 1 ) =/= ( 0 x. 0 )
31 fveq2 
 |-  ( i = 1 -> ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) )
32 0re 
 |-  0 e. RR
33 14 32 axlowdimlem4 
 |-  { <. 1 , 1 >. , <. 2 , 0 >. } : ( 1 ... 2 ) --> RR
34 ffn 
 |-  ( { <. 1 , 1 >. , <. 2 , 0 >. } : ( 1 ... 2 ) --> RR -> { <. 1 , 1 >. , <. 2 , 0 >. } Fn ( 1 ... 2 ) )
35 33 34 ax-mp 
 |-  { <. 1 , 1 >. , <. 2 , 0 >. } Fn ( 1 ... 2 )
36 axlowdimlem1 
 |-  ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR
37 ffn 
 |-  ( ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR -> ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) )
38 36 37 ax-mp 
 |-  ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N )
39 axlowdimlem2 
 |-  ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/)
40 1z 
 |-  1 e. ZZ
41 2z 
 |-  2 e. ZZ
42 40 41 40 3pm3.2i 
 |-  ( 1 e. ZZ /\ 2 e. ZZ /\ 1 e. ZZ )
43 15 21 pm3.2i 
 |-  ( 1 <_ 1 /\ 1 <_ 2 )
44 elfz4 
 |-  ( ( ( 1 e. ZZ /\ 2 e. ZZ /\ 1 e. ZZ ) /\ ( 1 <_ 1 /\ 1 <_ 2 ) ) -> 1 e. ( 1 ... 2 ) )
45 42 43 44 mp2an 
 |-  1 e. ( 1 ... 2 )
46 39 45 pm3.2i 
 |-  ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 1 e. ( 1 ... 2 ) )
47 fvun1 
 |-  ( ( { <. 1 , 1 >. , <. 2 , 0 >. } Fn ( 1 ... 2 ) /\ ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) /\ ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 1 e. ( 1 ... 2 ) ) ) -> ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 1 ) )
48 35 38 46 47 mp3an 
 |-  ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 1 )
49 1ne2 
 |-  1 =/= 2
50 1ex 
 |-  1 e. _V
51 50 50 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 1 ) = 1 )
52 49 51 ax-mp 
 |-  ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 1 ) = 1
53 48 52 eqtri 
 |-  ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = 1
54 31 53 eqtrdi 
 |-  ( i = 1 -> ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = 1 )
55 fveq2 
 |-  ( i = 1 -> ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) )
56 32 32 axlowdimlem4 
 |-  { <. 1 , 0 >. , <. 2 , 0 >. } : ( 1 ... 2 ) --> RR
57 ffn 
 |-  ( { <. 1 , 0 >. , <. 2 , 0 >. } : ( 1 ... 2 ) --> RR -> { <. 1 , 0 >. , <. 2 , 0 >. } Fn ( 1 ... 2 ) )
58 56 57 ax-mp 
 |-  { <. 1 , 0 >. , <. 2 , 0 >. } Fn ( 1 ... 2 )
59 fvun1 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 0 >. } Fn ( 1 ... 2 ) /\ ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) /\ ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 1 e. ( 1 ... 2 ) ) ) -> ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 1 ) )
60 58 38 46 59 mp3an 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 1 )
61 32 elexi 
 |-  0 e. _V
62 50 61 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 1 ) = 0 )
63 49 62 ax-mp 
 |-  ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 1 ) = 0
64 60 63 eqtri 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = 0
65 55 64 eqtrdi 
 |-  ( i = 1 -> ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = 0 )
66 54 65 oveq12d 
 |-  ( i = 1 -> ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) = ( 1 - 0 ) )
67 1m0e1 
 |-  ( 1 - 0 ) = 1
68 66 67 eqtrdi 
 |-  ( i = 1 -> ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) = 1 )
69 68 oveq1d 
 |-  ( i = 1 -> ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( 1 x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) )
70 fveq2 
 |-  ( i = 1 -> ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) )
71 32 14 axlowdimlem4 
 |-  { <. 1 , 0 >. , <. 2 , 1 >. } : ( 1 ... 2 ) --> RR
72 ffn 
 |-  ( { <. 1 , 0 >. , <. 2 , 1 >. } : ( 1 ... 2 ) --> RR -> { <. 1 , 0 >. , <. 2 , 1 >. } Fn ( 1 ... 2 ) )
73 71 72 ax-mp 
 |-  { <. 1 , 0 >. , <. 2 , 1 >. } Fn ( 1 ... 2 )
74 fvun1 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 1 >. } Fn ( 1 ... 2 ) /\ ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) /\ ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 1 e. ( 1 ... 2 ) ) ) -> ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 1 ) )
75 73 38 46 74 mp3an 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 1 )
76 50 61 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 1 ) = 0 )
77 49 76 ax-mp 
 |-  ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 1 ) = 0
78 75 77 eqtri 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 1 ) = 0
79 70 78 eqtrdi 
 |-  ( i = 1 -> ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) = 0 )
80 79 65 oveq12d 
 |-  ( i = 1 -> ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) = ( 0 - 0 ) )
81 0m0e0 
 |-  ( 0 - 0 ) = 0
82 80 81 eqtrdi 
 |-  ( i = 1 -> ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) = 0 )
83 82 oveq2d 
 |-  ( i = 1 -> ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. 0 ) )
84 69 83 neeq12d 
 |-  ( i = 1 -> ( ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> ( 1 x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. 0 ) ) )
85 fveq2 
 |-  ( j = 2 -> ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) = ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) )
86 40 41 41 3pm3.2i 
 |-  ( 1 e. ZZ /\ 2 e. ZZ /\ 2 e. ZZ )
87 2re 
 |-  2 e. RR
88 87 leidi 
 |-  2 <_ 2
89 21 88 pm3.2i 
 |-  ( 1 <_ 2 /\ 2 <_ 2 )
90 elfz4 
 |-  ( ( ( 1 e. ZZ /\ 2 e. ZZ /\ 2 e. ZZ ) /\ ( 1 <_ 2 /\ 2 <_ 2 ) ) -> 2 e. ( 1 ... 2 ) )
91 86 89 90 mp2an 
 |-  2 e. ( 1 ... 2 )
92 39 91 pm3.2i 
 |-  ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 2 e. ( 1 ... 2 ) )
93 fvun1 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 1 >. } Fn ( 1 ... 2 ) /\ ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) /\ ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 2 e. ( 1 ... 2 ) ) ) -> ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 2 ) )
94 73 38 92 93 mp3an 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 2 )
95 41 elexi 
 |-  2 e. _V
96 95 50 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 2 ) = 1 )
97 49 96 ax-mp 
 |-  ( { <. 1 , 0 >. , <. 2 , 1 >. } ` 2 ) = 1
98 94 97 eqtri 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = 1
99 85 98 eqtrdi 
 |-  ( j = 2 -> ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) = 1 )
100 fveq2 
 |-  ( j = 2 -> ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) = ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) )
101 fvun1 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 0 >. } Fn ( 1 ... 2 ) /\ ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) /\ ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 2 e. ( 1 ... 2 ) ) ) -> ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 2 ) )
102 58 38 92 101 mp3an 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 2 )
103 95 61 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 2 ) = 0 )
104 49 103 ax-mp 
 |-  ( { <. 1 , 0 >. , <. 2 , 0 >. } ` 2 ) = 0
105 102 104 eqtri 
 |-  ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = 0
106 100 105 eqtrdi 
 |-  ( j = 2 -> ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) = 0 )
107 99 106 oveq12d 
 |-  ( j = 2 -> ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) = ( 1 - 0 ) )
108 107 67 eqtrdi 
 |-  ( j = 2 -> ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) = 1 )
109 108 oveq2d 
 |-  ( j = 2 -> ( 1 x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( 1 x. 1 ) )
110 fveq2 
 |-  ( j = 2 -> ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) = ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) )
111 fvun1 
 |-  ( ( { <. 1 , 1 >. , <. 2 , 0 >. } Fn ( 1 ... 2 ) /\ ( ( 3 ... N ) X. { 0 } ) Fn ( 3 ... N ) /\ ( ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) /\ 2 e. ( 1 ... 2 ) ) ) -> ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 2 ) )
112 35 38 92 111 mp3an 
 |-  ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 2 )
113 95 61 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 2 ) = 0 )
114 49 113 ax-mp 
 |-  ( { <. 1 , 1 >. , <. 2 , 0 >. } ` 2 ) = 0
115 112 114 eqtri 
 |-  ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` 2 ) = 0
116 110 115 eqtrdi 
 |-  ( j = 2 -> ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) = 0 )
117 116 106 oveq12d 
 |-  ( j = 2 -> ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) = ( 0 - 0 ) )
118 117 81 eqtrdi 
 |-  ( j = 2 -> ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) = 0 )
119 118 oveq1d 
 |-  ( j = 2 -> ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. 0 ) = ( 0 x. 0 ) )
120 109 119 neeq12d 
 |-  ( j = 2 -> ( ( 1 x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. 0 ) <-> ( 1 x. 1 ) =/= ( 0 x. 0 ) ) )
121 84 120 rspc2ev 
 |-  ( ( 1 e. ( 1 ... N ) /\ 2 e. ( 1 ... N ) /\ ( 1 x. 1 ) =/= ( 0 x. 0 ) ) -> E. i e. ( 1 ... N ) E. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
122 30 121 mp3an3 
 |-  ( ( 1 e. ( 1 ... N ) /\ 2 e. ( 1 ... N ) ) -> E. i e. ( 1 ... N ) E. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
123 18 24 122 syl2anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. i e. ( 1 ... N ) E. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
124 df-ne 
 |-  ( ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> -. ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
125 124 rexbii 
 |-  ( E. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> E. j e. ( 1 ... N ) -. ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
126 rexnal 
 |-  ( E. j e. ( 1 ... N ) -. ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> -. A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
127 125 126 bitri 
 |-  ( E. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> -. A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
128 127 rexbii 
 |-  ( E. i e. ( 1 ... N ) E. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> E. i e. ( 1 ... N ) -. A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
129 rexnal 
 |-  ( E. i e. ( 1 ... N ) -. A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> -. A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
130 128 129 bitri 
 |-  ( E. i e. ( 1 ... N ) E. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) =/= ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) <-> -. A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
131 123 130 sylib 
 |-  ( N e. ( ZZ>= ` 2 ) -> -. A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) )
132 32 32 axlowdimlem5 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
133 14 32 axlowdimlem5 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
134 32 14 axlowdimlem5 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) )
135 colinearalg 
 |-  ( ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) /\ ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) /\ ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) e. ( EE ` N ) ) -> ( ( ( { <. 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 } ) ) >. ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) ) )
136 132 133 134 135 syl3anc 
 |-  ( 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 } ) ) >. ) <-> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) ) = ( ( ( ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` j ) ) x. ( ( ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) - ( ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) ` i ) ) ) ) )
137 131 136 mtbird 
 |-  ( 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 } ) ) >. ) )
138 2 3 opeq12i 
 |-  <. B , C >. = <. ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.
139 1 138 breq12i 
 |-  ( A Btwn <. B , C >. <-> ( { <. 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 } ) ) >. )
140 3 1 opeq12i 
 |-  <. C , A >. = <. ( { <. 1 , 0 >. , <. 2 , 1 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.
141 2 140 breq12i 
 |-  ( B Btwn <. C , A >. <-> ( { <. 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 } ) ) >. )
142 1 2 opeq12i 
 |-  <. A , B >. = <. ( { <. 1 , 0 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) , ( { <. 1 , 1 >. , <. 2 , 0 >. } u. ( ( 3 ... N ) X. { 0 } ) ) >.
143 3 142 breq12i 
 |-  ( C Btwn <. A , B >. <-> ( { <. 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 139 141 143 3orbi123i 
 |-  ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) <-> ( ( { <. 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 } ) ) >. ) )
145 137 144 sylnibr 
 |-  ( N e. ( ZZ>= ` 2 ) -> -. ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) )