MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axlowdimlem6 Structured version   Visualization version   Unicode version

Theorem axlowdimlem6 24970
Description: Lemma for axlowdim 24984. Show that three points are non-colinear. (Contributed by Scott Fenton, 29-Jun-2013.)
Hypotheses
Ref Expression
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
Ref Expression
axlowdimlem6  |-  ( N  e.  ( ZZ>= `  2
)  ->  -.  ( A  Btwn  <. B ,  C >.  \/  B  Btwn  <. C ,  A >.  \/  C  Btwn  <. A ,  B >. ) )

Proof of Theorem axlowdimlem6
Dummy variables  i 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1zzd 10965 . . . . . 6  |-  ( N  e.  ( ZZ>= `  2
)  ->  1  e.  ZZ )
2 eluzelz 11165 . . . . . 6  |-  ( N  e.  ( ZZ>= `  2
)  ->  N  e.  ZZ )
3 2nn 10764 . . . . . . . . . . 11  |-  2  e.  NN
4 uznnssnn 11203 . . . . . . . . . . 11  |-  ( 2  e.  NN  ->  ( ZZ>=
`  2 )  C_  NN )
53, 4ax-mp 5 . . . . . . . . . 10  |-  ( ZZ>= ` 
2 )  C_  NN
6 nnuz 11191 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
75, 6sseqtri 3463 . . . . . . . . 9  |-  ( ZZ>= ` 
2 )  C_  ( ZZ>=
`  1 )
87sseli 3427 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  2
)  ->  N  e.  ( ZZ>= `  1 )
)
9 eluzle 11168 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  1
)  ->  1  <_  N )
108, 9syl 17 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  2
)  ->  1  <_  N )
11 1re 9639 . . . . . . . 8  |-  1  e.  RR
1211leidi 10145 . . . . . . 7  |-  1  <_  1
1310, 12jctil 540 . . . . . 6  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( 1  <_  1  /\  1  <_  N ) )
14 elfz4 11790 . . . . . 6  |-  ( ( ( 1  e.  ZZ  /\  N  e.  ZZ  /\  1  e.  ZZ )  /\  ( 1  <_  1  /\  1  <_  N ) )  ->  1  e.  ( 1 ... N
) )
151, 2, 1, 13, 14syl31anc 1270 . . . . 5  |-  ( N  e.  ( ZZ>= `  2
)  ->  1  e.  ( 1 ... N
) )
16 eluzel2 11161 . . . . . 6  |-  ( N  e.  ( ZZ>= `  2
)  ->  2  e.  ZZ )
17 eluzle 11168 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  2
)  ->  2  <_  N )
18 1le2 10820 . . . . . . 7  |-  1  <_  2
1917, 18jctil 540 . . . . . 6  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( 1  <_  2  /\  2  <_  N ) )
20 elfz4 11790 . . . . . 6  |-  ( ( ( 1  e.  ZZ  /\  N  e.  ZZ  /\  2  e.  ZZ )  /\  ( 1  <_  2  /\  2  <_  N ) )  ->  2  e.  ( 1 ... N
) )
211, 2, 16, 19, 20syl31anc 1270 . . . . 5  |-  ( N  e.  ( ZZ>= `  2
)  ->  2  e.  ( 1 ... N
) )
22 ax-1ne0 9605 . . . . . . 7  |-  1  =/=  0
23 1t1e1 10754 . . . . . . . 8  |-  ( 1  x.  1 )  =  1
24 0cn 9632 . . . . . . . . 9  |-  0  e.  CC
2524mul01i 9820 . . . . . . . 8  |-  ( 0  x.  0 )  =  0
2623, 25neeq12i 2689 . . . . . . 7  |-  ( ( 1  x.  1 )  =/=  ( 0  x.  0 )  <->  1  =/=  0 )
2722, 26mpbir 213 . . . . . 6  |-  ( 1  x.  1 )  =/=  ( 0  x.  0 )
28 fveq2 5863 . . . . . . . . . . . 12  |-  ( i  =  1  ->  (
( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  i )  =  ( ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 ) )
29 0re 9640 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
3011, 29axlowdimlem4 24968 . . . . . . . . . . . . . . 15  |-  { <. 1 ,  1 >. , 
<. 2 ,  0
>. } : ( 1 ... 2 ) --> RR
31 ffn 5726 . . . . . . . . . . . . . . 15  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. } : ( 1 ... 2 ) --> RR  ->  { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  Fn  ( 1 ... 2 ) )
3230, 31ax-mp 5 . . . . . . . . . . . . . 14  |-  { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  Fn  ( 1 ... 2 )
33 axlowdimlem1 24965 . . . . . . . . . . . . . . 15  |-  ( ( 3 ... N )  X.  { 0 } ) : ( 3 ... N ) --> RR
34 ffn 5726 . . . . . . . . . . . . . . 15  |-  ( ( ( 3 ... N
)  X.  { 0 } ) : ( 3 ... N ) --> RR  ->  ( (
3 ... N )  X. 
{ 0 } )  Fn  ( 3 ... N ) )
3533, 34ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 3 ... N )  X.  { 0 } )  Fn  ( 3 ... N )
36 axlowdimlem2 24966 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... 2 )  i^i  ( 3 ... N ) )  =  (/)
37 1z 10964 . . . . . . . . . . . . . . . . 17  |-  1  e.  ZZ
38 2z 10966 . . . . . . . . . . . . . . . . 17  |-  2  e.  ZZ
3937, 38, 373pm3.2i 1185 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  /\  2  e.  ZZ  /\  1  e.  ZZ )
4012, 18pm3.2i 457 . . . . . . . . . . . . . . . 16  |-  ( 1  <_  1  /\  1  <_  2 )
41 elfz4 11790 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  e.  ZZ  /\  2  e.  ZZ  /\  1  e.  ZZ )  /\  ( 1  <_  1  /\  1  <_  2 ) )  ->  1  e.  ( 1 ... 2
) )
4239, 40, 41mp2an 677 . . . . . . . . . . . . . . 15  |-  1  e.  ( 1 ... 2
)
4336, 42pm3.2i 457 . . . . . . . . . . . . . 14  |-  ( ( ( 1 ... 2
)  i^i  ( 3 ... N ) )  =  (/)  /\  1  e.  ( 1 ... 2
) )
44 fvun1 5934 . . . . . . . . . . . . . 14  |-  ( ( { <. 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
) )
4532, 35, 43, 44mp3an 1363 . . . . . . . . . . . . 13  |-  ( ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 )  =  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. } `  1
)
46 1ne2 10819 . . . . . . . . . . . . . 14  |-  1  =/=  2
47 1ex 9635 . . . . . . . . . . . . . . 15  |-  1  e.  _V
4847, 47fvpr1 6105 . . . . . . . . . . . . . 14  |-  ( 1  =/=  2  ->  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. } `  1
)  =  1 )
4946, 48ax-mp 5 . . . . . . . . . . . . 13  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. } `  1
)  =  1
5045, 49eqtri 2472 . . . . . . . . . . . 12  |-  ( ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 )  =  1
5128, 50syl6eq 2500 . . . . . . . . . . 11  |-  ( i  =  1  ->  (
( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  i )  =  1 )
52 fveq2 5863 . . . . . . . . . . . 12  |-  ( i  =  1  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  i )  =  ( ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 ) )
5329, 29axlowdimlem4 24968 . . . . . . . . . . . . . . 15  |-  { <. 1 ,  0 >. , 
<. 2 ,  0
>. } : ( 1 ... 2 ) --> RR
54 ffn 5726 . . . . . . . . . . . . . . 15  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. } : ( 1 ... 2 ) --> RR  ->  { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  Fn  ( 1 ... 2 ) )
5553, 54ax-mp 5 . . . . . . . . . . . . . 14  |-  { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  Fn  ( 1 ... 2 )
56 fvun1 5934 . . . . . . . . . . . . . 14  |-  ( ( { <. 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
) )
5755, 35, 43, 56mp3an 1363 . . . . . . . . . . . . 13  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 )  =  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. } `  1
)
5829elexi 3054 . . . . . . . . . . . . . . 15  |-  0  e.  _V
5947, 58fvpr1 6105 . . . . . . . . . . . . . 14  |-  ( 1  =/=  2  ->  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. } `  1
)  =  0 )
6046, 59ax-mp 5 . . . . . . . . . . . . 13  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. } `  1
)  =  0
6157, 60eqtri 2472 . . . . . . . . . . . 12  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 )  =  0
6252, 61syl6eq 2500 . . . . . . . . . . 11  |-  ( i  =  1  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  i )  =  0 )
6351, 62oveq12d 6306 . . . . . . . . . 10  |-  ( i  =  1  ->  (
( ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  i
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  i ) )  =  ( 1  -  0 ) )
64 1m0e1 10717 . . . . . . . . . 10  |-  ( 1  -  0 )  =  1
6563, 64syl6eq 2500 . . . . . . . . 9  |-  ( i  =  1  ->  (
( ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  i
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  i ) )  =  1 )
6665oveq1d 6303 . . . . . . . 8  |-  ( 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 ) ) ) )
67 fveq2 5863 . . . . . . . . . . . 12  |-  ( i  =  1  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  i )  =  ( ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 ) )
6829, 11axlowdimlem4 24968 . . . . . . . . . . . . . . 15  |-  { <. 1 ,  0 >. , 
<. 2 ,  1
>. } : ( 1 ... 2 ) --> RR
69 ffn 5726 . . . . . . . . . . . . . . 15  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. } : ( 1 ... 2 ) --> RR  ->  { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  Fn  ( 1 ... 2 ) )
7068, 69ax-mp 5 . . . . . . . . . . . . . 14  |-  { <. 1 ,  0 >. , 
<. 2 ,  1
>. }  Fn  ( 1 ... 2 )
71 fvun1 5934 . . . . . . . . . . . . . 14  |-  ( ( { <. 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
) )
7270, 35, 43, 71mp3an 1363 . . . . . . . . . . . . 13  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 )  =  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. } `  1
)
7347, 58fvpr1 6105 . . . . . . . . . . . . . 14  |-  ( 1  =/=  2  ->  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. } `  1
)  =  0 )
7446, 73ax-mp 5 . . . . . . . . . . . . 13  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. } `  1
)  =  0
7572, 74eqtri 2472 . . . . . . . . . . . 12  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
1 )  =  0
7667, 75syl6eq 2500 . . . . . . . . . . 11  |-  ( i  =  1  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  i )  =  0 )
7776, 62oveq12d 6306 . . . . . . . . . 10  |-  ( i  =  1  ->  (
( ( { <. 1 ,  0 >. , 
<. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  i
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  i ) )  =  ( 0  -  0 ) )
78 0m0e0 10716 . . . . . . . . . 10  |-  ( 0  -  0 )  =  0
7977, 78syl6eq 2500 . . . . . . . . 9  |-  ( i  =  1  ->  (
( ( { <. 1 ,  0 >. , 
<. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  i
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  i ) )  =  0 )
8079oveq2d 6304 . . . . . . . 8  |-  ( 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 ) )
8166, 80neeq12d 2684 . . . . . . 7  |-  ( 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 ) ) )
82 fveq2 5863 . . . . . . . . . . . 12  |-  ( j  =  2  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  j )  =  ( ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 ) )
8337, 38, 383pm3.2i 1185 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  /\  2  e.  ZZ  /\  2  e.  ZZ )
84 2re 10676 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
8584leidi 10145 . . . . . . . . . . . . . . . . 17  |-  2  <_  2
8618, 85pm3.2i 457 . . . . . . . . . . . . . . . 16  |-  ( 1  <_  2  /\  2  <_  2 )
87 elfz4 11790 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  e.  ZZ  /\  2  e.  ZZ  /\  2  e.  ZZ )  /\  ( 1  <_  2  /\  2  <_  2 ) )  ->  2  e.  ( 1 ... 2
) )
8883, 86, 87mp2an 677 . . . . . . . . . . . . . . 15  |-  2  e.  ( 1 ... 2
)
8936, 88pm3.2i 457 . . . . . . . . . . . . . 14  |-  ( ( ( 1 ... 2
)  i^i  ( 3 ... N ) )  =  (/)  /\  2  e.  ( 1 ... 2
) )
90 fvun1 5934 . . . . . . . . . . . . . 14  |-  ( ( { <. 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
) )
9170, 35, 89, 90mp3an 1363 . . . . . . . . . . . . 13  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 )  =  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. } `  2
)
9238elexi 3054 . . . . . . . . . . . . . . 15  |-  2  e.  _V
9392, 47fvpr2 6106 . . . . . . . . . . . . . 14  |-  ( 1  =/=  2  ->  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. } `  2
)  =  1 )
9446, 93ax-mp 5 . . . . . . . . . . . . 13  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. } `  2
)  =  1
9591, 94eqtri 2472 . . . . . . . . . . . 12  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 )  =  1
9682, 95syl6eq 2500 . . . . . . . . . . 11  |-  ( j  =  2  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  j )  =  1 )
97 fveq2 5863 . . . . . . . . . . . 12  |-  ( j  =  2  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  j )  =  ( ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 ) )
98 fvun1 5934 . . . . . . . . . . . . . 14  |-  ( ( { <. 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
) )
9955, 35, 89, 98mp3an 1363 . . . . . . . . . . . . 13  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 )  =  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. } `  2
)
10092, 58fvpr2 6106 . . . . . . . . . . . . . 14  |-  ( 1  =/=  2  ->  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. } `  2
)  =  0 )
10146, 100ax-mp 5 . . . . . . . . . . . . 13  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. } `  2
)  =  0
10299, 101eqtri 2472 . . . . . . . . . . . 12  |-  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 )  =  0
10397, 102syl6eq 2500 . . . . . . . . . . 11  |-  ( j  =  2  ->  (
( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  j )  =  0 )
10496, 103oveq12d 6306 . . . . . . . . . 10  |-  ( j  =  2  ->  (
( ( { <. 1 ,  0 >. , 
<. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  j
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  j ) )  =  ( 1  -  0 ) )
105104, 64syl6eq 2500 . . . . . . . . 9  |-  ( j  =  2  ->  (
( ( { <. 1 ,  0 >. , 
<. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  j
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  j ) )  =  1 )
106105oveq2d 6304 . . . . . . . 8  |-  ( 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 ) )
107 fveq2 5863 . . . . . . . . . . . 12  |-  ( j  =  2  ->  (
( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  j )  =  ( ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 ) )
108 fvun1 5934 . . . . . . . . . . . . . 14  |-  ( ( { <. 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
) )
10932, 35, 89, 108mp3an 1363 . . . . . . . . . . . . 13  |-  ( ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 )  =  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. } `  2
)
11092, 58fvpr2 6106 . . . . . . . . . . . . . 14  |-  ( 1  =/=  2  ->  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. } `  2
)  =  0 )
11146, 110ax-mp 5 . . . . . . . . . . . . 13  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. } `  2
)  =  0
112109, 111eqtri 2472 . . . . . . . . . . . 12  |-  ( ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ` 
2 )  =  0
113107, 112syl6eq 2500 . . . . . . . . . . 11  |-  ( j  =  2  ->  (
( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) `  j )  =  0 )
114113, 103oveq12d 6306 . . . . . . . . . 10  |-  ( j  =  2  ->  (
( ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  j
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  j ) )  =  ( 0  -  0 ) )
115114, 78syl6eq 2500 . . . . . . . . 9  |-  ( j  =  2  ->  (
( ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) `  j
)  -  ( ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) `  j ) )  =  0 )
116115oveq1d 6303 . . . . . . . 8  |-  ( 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 ) )
117106, 116neeq12d 2684 . . . . . . 7  |-  ( 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 ) ) )
11881, 117rspc2ev 3160 . . . . . 6  |-  ( ( 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 ) ) ) )
11927, 118mp3an3 1352 . . . . 5  |-  ( ( 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 ) ) ) )
12015, 21, 119syl2anc 666 . . . 4  |-  ( 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 ) ) ) )
121 df-ne 2623 . . . . . . . 8  |-  ( ( ( ( ( {
<. 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 ) ) ) )
122121rexbii 2888 . . . . . . 7  |-  ( 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 ) ) ) )
123 rexnal 2835 . . . . . . 7  |-  ( 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 ) ) ) )
124122, 123bitri 253 . . . . . 6  |-  ( 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 ) ) ) )
125124rexbii 2888 . . . . 5  |-  ( 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 ) ) ) )
126 rexnal 2835 . . . . 5  |-  ( 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 ) ) ) )
127125, 126bitri 253 . . . 4  |-  ( 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 ) ) ) )
128120, 127sylib 200 . . 3  |-  ( 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 ) ) ) )
12929, 29axlowdimlem5 24969 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
13011, 29axlowdimlem5 24969 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
13129, 11axlowdimlem5 24969 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
132 colinearalg 24933 . . . 4  |-  ( ( ( { <. 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 ) ) ) ) )
133129, 130, 131, 132syl3anc 1267 . . 3  |-  ( 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 ) ) ) ) )
134128, 133mtbird 303 . 2  |-  ( 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 } ) ) >. ) )
135 axlowdimlem6.1 . . . 4  |-  A  =  ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
136 axlowdimlem6.2 . . . . 5  |-  B  =  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
137 axlowdimlem6.3 . . . . 5  |-  C  =  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
138136, 137opeq12i 4170 . . . 4  |-  <. B ,  C >.  =  <. ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >.
139135, 138breq12i 4410 . . 3  |-  ( 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 } ) ) >. )
140137, 135opeq12i 4170 . . . 4  |-  <. C ,  A >.  =  <. ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >.
141136, 140breq12i 4410 . . 3  |-  ( 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 } ) ) >. )
142135, 136opeq12i 4170 . . . 4  |-  <. A ,  B >.  =  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >.
143137, 142breq12i 4410 . . 3  |-  ( 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 } ) ) >. )
144139, 141, 1433orbi123i 1197 . 2  |-  ( ( 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 } ) ) >.
) )
145134, 144sylnibr 307 1  |-  ( N  e.  ( ZZ>= `  2
)  ->  -.  ( A  Btwn  <. B ,  C >.  \/  B  Btwn  <. C ,  A >.  \/  C  Btwn  <. A ,  B >. ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    \/ w3o 983    /\ w3a 984    = wceq 1443    e. wcel 1886    =/= wne 2621   A.wral 2736   E.wrex 2737    u. cun 3401    i^i cin 3402    C_ wss 3403   (/)c0 3730   {csn 3967   {cpr 3969   <.cop 3973   class class class wbr 4401    X. cxp 4831    Fn wfn 5576   -->wf 5577   ` cfv 5581  (class class class)co 6288   RRcr 9535   0cc0 9536   1c1 9537    x. cmul 9541    <_ cle 9673    - cmin 9857   NNcn 10606   2c2 10656   3c3 10657   ZZcz 10934   ZZ>=cuz 11156   ...cfz 11781   EEcee 24911    Btwn cbtwn 24912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-map 7471  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-n0 10867  df-z 10935  df-uz 11157  df-icc 11639  df-fz 11782  df-seq 12211  df-exp 12270  df-ee 24914  df-btwn 24915
This theorem is referenced by:  axlowdim2  24983  axlowdim  24984
  Copyright terms: Public domain W3C validator