Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  colinearalg Unicode version

Theorem colinearalg 24610
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 24605. (Contributed by Scott Fenton, 24-Jun-2013.)
Assertion
Ref Expression
colinearalg  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  (
( A  Btwn  <. B ,  C >.  \/  B  Btwn  <. C ,  A >.  \/  C  Btwn  <. A ,  B >. )  <->  A. i  e.  ( 1 ... N
) A. j  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j )
) )  =  ( ( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
Distinct variable groups:    i, N, j    A, i, j    B, i, j    C, i, j

Proof of Theorem colinearalg
Dummy variable  p is distinct from all other variables.
StepHypRef Expression
1 brbtwn2 24605 . . 3  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( A  Btwn  <. B ,  C >.  <-> 
( A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) ) )
2 brbtwn2 24605 . . . . 5  |-  ( ( B  e.  ( EE
`  N )  /\  C  e.  ( EE `  N )  /\  A  e.  ( EE `  N
) )  ->  ( B  Btwn  <. C ,  A >.  <-> 
( A. i  e.  ( 1 ... N
) ( ( ( C `  i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( C `
 i )  -  ( B `  i ) )  x.  ( ( A `  j )  -  ( B `  j ) ) )  =  ( ( ( C `  j )  -  ( B `  j ) )  x.  ( ( A `  i )  -  ( B `  i )
) ) ) ) )
323comr 1159 . . . 4  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( B  Btwn  <. C ,  A >.  <-> 
( A. i  e.  ( 1 ... N
) ( ( ( C `  i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( C `
 i )  -  ( B `  i ) )  x.  ( ( A `  j )  -  ( B `  j ) ) )  =  ( ( ( C `  j )  -  ( B `  j ) )  x.  ( ( A `  i )  -  ( B `  i )
) ) ) ) )
4 colinearalglem3 24608 . . . . . 6  |-  ( ( B  e.  ( EE
`  N )  /\  C  e.  ( EE `  N )  /\  A  e.  ( EE `  N
) )  ->  ( A. i  e.  (
1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  j )  -  ( B `  j ) ) )  =  ( ( ( C `  j )  -  ( B `  j ) )  x.  ( ( A `  i )  -  ( B `  i )
) )  <->  A. i  e.  ( 1 ... N
) A. j  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j )
) )  =  ( ( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
543comr 1159 . . . . 5  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( A. i  e.  (
1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  j )  -  ( B `  j ) ) )  =  ( ( ( C `  j )  -  ( B `  j ) )  x.  ( ( A `  i )  -  ( B `  i )
) )  <->  A. i  e.  ( 1 ... N
) A. j  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j )
) )  =  ( ( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
65anbi2d 684 . . . 4  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  (
( A. i  e.  ( 1 ... N
) ( ( ( C `  i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( C `
 i )  -  ( B `  i ) )  x.  ( ( A `  j )  -  ( B `  j ) ) )  =  ( ( ( C `  j )  -  ( B `  j ) )  x.  ( ( A `  i )  -  ( B `  i )
) ) )  <->  ( A. i  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) ) )
73, 6bitrd 244 . . 3  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( B  Btwn  <. C ,  A >.  <-> 
( A. i  e.  ( 1 ... N
) ( ( ( C `  i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) ) )
8 brbtwn2 24605 . . . . 5  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  ->  ( C  Btwn  <. A ,  B >.  <-> 
( A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( B `  i )  -  ( C `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( A `
 i )  -  ( C `  i ) )  x.  ( ( B `  j )  -  ( C `  j ) ) )  =  ( ( ( A `  j )  -  ( C `  j ) )  x.  ( ( B `  i )  -  ( C `  i )
) ) ) ) )
9 colinearalglem2 24607 . . . . . 6  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  ->  ( A. i  e.  (
1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  j )  -  ( C `  j ) ) )  =  ( ( ( A `  j )  -  ( C `  j ) )  x.  ( ( B `  i )  -  ( C `  i )
) )  <->  A. i  e.  ( 1 ... N
) A. j  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j )
) )  =  ( ( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
109anbi2d 684 . . . . 5  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  ->  (
( A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( B `  i )  -  ( C `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( A `
 i )  -  ( C `  i ) )  x.  ( ( B `  j )  -  ( C `  j ) ) )  =  ( ( ( A `  j )  -  ( C `  j ) )  x.  ( ( B `  i )  -  ( C `  i )
) ) )  <->  ( A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) ) )
118, 10bitrd 244 . . . 4  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N )  /\  B  e.  ( EE `  N
) )  ->  ( C  Btwn  <. A ,  B >.  <-> 
( A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( B `  i )  -  ( C `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) ) )
12113coml 1158 . . 3  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( C  Btwn  <. A ,  B >.  <-> 
( A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( B `  i )  -  ( C `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) ) )
131, 7, 123orbi123d 1251 . 2  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  (
( A  Btwn  <. B ,  C >.  \/  B  Btwn  <. C ,  A >.  \/  C  Btwn  <. A ,  B >. )  <->  ( ( A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )  \/  ( A. i  e.  ( 1 ... N
) ( ( ( C `  i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )  \/  ( A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( B `  i )  -  ( C `  i )
) )  <_  0  /\  A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) ) ) )
14 fveecn 24602 . . . . . . . . . . . . 13  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
15 fveecn 24602 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
16 subid 9083 . . . . . . . . . . . . . . . 16  |-  ( ( C `  i )  e.  CC  ->  (
( C `  i
)  -  ( C `
 i ) )  =  0 )
1716oveq2d 5890 . . . . . . . . . . . . . . 15  |-  ( ( C `  i )  e.  CC  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( C `  i ) )  x.  0 ) )
1817adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( C `  i ) )  x.  0 ) )
19 subcl 9067 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( B `  i )  -  ( C `  i )
)  e.  CC )
2019mul01d 9027 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  0 )  =  0 )
2118, 20eqtrd 2328 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  0 )
2214, 15, 21syl2an 463 . . . . . . . . . . . 12  |-  ( ( ( B  e.  ( EE `  N )  /\  i  e.  ( 1 ... N ) )  /\  ( C  e.  ( EE `  N )  /\  i  e.  ( 1 ... N
) ) )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  0 )
2322anandirs 804 . . . . . . . . . . 11  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  0 )
24 0le0 9843 . . . . . . . . . . 11  |-  0  <_  0
2523, 24syl6eqbr 4076 . . . . . . . . . 10  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0 )
2625ralrimiva 2639 . . . . . . . . 9  |-  ( ( B  e.  ( EE
`  N )  /\  C  e.  ( EE `  N ) )  ->  A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0 )
27263adant1 973 . . . . . . . 8  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i )
) )  <_  0
)
28 fveq1 5540 . . . . . . . . . . . 12  |-  ( C  =  A  ->  ( C `  i )  =  ( A `  i ) )
2928oveq2d 5890 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( B `  i
)  -  ( C `
 i ) )  =  ( ( B `
 i )  -  ( A `  i ) ) )
3028oveq2d 5890 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( C `  i
)  -  ( C `
 i ) )  =  ( ( C `
 i )  -  ( A `  i ) ) )
3129, 30oveq12d 5892 . . . . . . . . . 10  |-  ( C  =  A  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
3231breq1d 4049 . . . . . . . . 9  |-  ( C  =  A  ->  (
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0
) )
3332ralbidv 2576 . . . . . . . 8  |-  ( C  =  A  ->  ( A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0  <->  A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0
) )
3427, 33syl5ibcom 211 . . . . . . 7  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( C  =  A  ->  A. i  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0 ) )
35 3mix1 1124 . . . . . . 7  |-  ( A. i  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  ->  ( A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0 ) )
3634, 35syl6 29 . . . . . 6  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( C  =  A  ->  ( A. i  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0 ) ) )
3736a1dd 42 . . . . 5  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( C  =  A  ->  ( A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  ->  ( A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0 ) ) ) )
38 simp3 957 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  C  e.  ( EE `  N
) )
39 simp1 955 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  A  e.  ( EE `  N
) )
40 eqeefv 24603 . . . . . . . . 9  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N ) )  -> 
( C  =  A  <->  A. p  e.  (
1 ... N ) ( C `  p )  =  ( A `  p ) ) )
4138, 39, 40syl2anc 642 . . . . . . . 8  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( C  =  A  <->  A. p  e.  ( 1 ... N
) ( C `  p )  =  ( A `  p ) ) )
4241necon3abid 2492 . . . . . . 7  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( C  =/=  A  <->  -.  A. p  e.  ( 1 ... N
) ( C `  p )  =  ( A `  p ) ) )
43 df-ne 2461 . . . . . . . . 9  |-  ( ( C `  p )  =/=  ( A `  p )  <->  -.  ( C `  p )  =  ( A `  p ) )
4443rexbii 2581 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N ) ( C `  p )  =/=  ( A `  p )  <->  E. p  e.  ( 1 ... N
)  -.  ( C `
 p )  =  ( A `  p
) )
45 rexnal 2567 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N )  -.  ( C `  p
)  =  ( A `
 p )  <->  -.  A. p  e.  ( 1 ... N
) ( C `  p )  =  ( A `  p ) )
4644, 45bitr2i 241 . . . . . . 7  |-  ( -. 
A. p  e.  ( 1 ... N ) ( C `  p
)  =  ( A `
 p )  <->  E. p  e.  ( 1 ... N
) ( C `  p )  =/=  ( A `  p )
)
4742, 46syl6bb 252 . . . . . 6  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( C  =/=  A  <->  E. p  e.  ( 1 ... N
) ( C `  p )  =/=  ( A `  p )
) )
48 ralcom 2713 . . . . . . . . 9  |-  ( A. i  e.  ( 1 ... N ) A. j  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <->  A. j  e.  ( 1 ... N
) A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j )
) )  =  ( ( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) )
49 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( j  =  p  ->  ( C `  j )  =  ( C `  p ) )
50 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( j  =  p  ->  ( A `  j )  =  ( A `  p ) )
5149, 50oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  (
( C `  j
)  -  ( A `
 j ) )  =  ( ( C `
 p )  -  ( A `  p ) ) )
5251oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) ) )
53 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( j  =  p  ->  ( B `  j )  =  ( B `  p ) )
5453, 50oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  (
( B `  j
)  -  ( A `
 j ) )  =  ( ( B `
 p )  -  ( A `  p ) ) )
5554oveq1d 5889 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
5652, 55eqeq12d 2310 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
5756ralbidv 2576 . . . . . . . . . . . 12  |-  ( j  =  p  ->  ( A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
5857rspcv 2893 . . . . . . . . . . 11  |-  ( p  e.  ( 1 ... N )  ->  ( A. j  e.  (
1 ... N ) A. i  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  j )  -  ( A `  j ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  ->  A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
5958ad2antrl 708 . . . . . . . . . 10  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( p  e.  ( 1 ... N )  /\  ( C `  p )  =/=  ( A `  p
) ) )  -> 
( A. j  e.  ( 1 ... N
) A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  j )  -  ( A `  j )
) )  =  ( ( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  ->  A. i  e.  ( 1 ... N ) ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) )
60 fveere 24601 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( A `  p )  e.  RR )
61603ad2antl1 1117 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( A `  p )  e.  RR )
62 fveere 24601 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( B `  p )  e.  RR )
63623ad2antl2 1118 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( B `  p )  e.  RR )
64 fveere 24601 . . . . . . . . . . . . . . 15  |-  ( ( C  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( C `  p )  e.  RR )
65643ad2antl3 1119 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( C `  p )  e.  RR )
6661, 63, 653jca 1132 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  (
( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR ) )
6766anim1i 551 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  /\  ( C `  p )  =/=  ( A `  p
) )  ->  (
( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) ) )
6867anasss 628 . . . . . . . . . . 11  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( p  e.  ( 1 ... N )  /\  ( C `  p )  =/=  ( A `  p
) ) )  -> 
( ( ( A `
 p )  e.  RR  /\  ( B `
 p )  e.  RR  /\  ( C `
 p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p
) ) )
69 fveecn 24602 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  CC )
70693ad2antl1 1117 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( A `  i )  e.  CC )
71143ad2antl2 1118 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( B `  i )  e.  CC )
72153ad2antl3 1119 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( C `  i )  e.  CC )
7370, 71, 723jca 1132 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( A `  i
)  e.  CC  /\  ( B `  i )  e.  CC  /\  ( C `  i )  e.  CC ) )
7473adantlr 695 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p
) ) )  /\  i  e.  ( 1 ... N ) )  ->  ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC  /\  ( C `
 i )  e.  CC ) )
75 recn 8843 . . . . . . . . . . . . . . . . 17  |-  ( ( A `  p )  e.  RR  ->  ( A `  p )  e.  CC )
76 recn 8843 . . . . . . . . . . . . . . . . 17  |-  ( ( B `  p )  e.  RR  ->  ( B `  p )  e.  CC )
77 recn 8843 . . . . . . . . . . . . . . . . 17  |-  ( ( C `  p )  e.  RR  ->  ( C `  p )  e.  CC )
7875, 76, 773anim123i 1137 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( A `  p
)  e.  CC  /\  ( B `  p )  e.  CC  /\  ( C `  p )  e.  CC ) )
7978adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC ) )
8079ad2antlr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p
) ) )  /\  i  e.  ( 1 ... N ) )  ->  ( ( A `
 p )  e.  CC  /\  ( B `
 p )  e.  CC  /\  ( C `
 p )  e.  CC ) )
81 simplrr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p
) ) )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  p )  =/=  ( A `  p )
)
82 eqcom 2298 . . . . . . . . . . . . . . 15  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  <->  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  =  ( B `
 i ) )
83 simp12 986 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( B `  i
)  e.  CC )
84 simp11 985 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( A `  i
)  e.  CC )
85 simp22 989 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( B `  p
)  e.  CC )
86 simp21 988 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( A `  p
)  e.  CC )
8785, 86subcld 9173 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( B `  p )  -  ( A `  p )
)  e.  CC )
88 simp23 990 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( C `  p
)  e.  CC )
8988, 86subcld 9173 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( C `  p )  -  ( A `  p )
)  e.  CC )
90 simpr3 963 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC ) )  ->  ( C `  p )  e.  CC )
91 simpr1 961 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC ) )  ->  ( A `  p )  e.  CC )
92 subeq0 9089 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C `  p
)  e.  CC  /\  ( A `  p )  e.  CC )  -> 
( ( ( C `
 p )  -  ( A `  p ) )  =  0  <->  ( C `  p )  =  ( A `  p ) ) )
9390, 91, 92syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC ) )  ->  ( ( ( C `  p )  -  ( A `  p ) )  =  0  <->  ( C `  p )  =  ( A `  p ) ) )
9493necon3bid 2494 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC ) )  ->  ( ( ( C `  p )  -  ( A `  p ) )  =/=  0  <->  ( C `  p )  =/=  ( A `  p )
) )
9594biimp3ar 1282 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( C `  p )  -  ( A `  p )
)  =/=  0 )
9687, 89, 95divcld 9552 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  e.  CC )
97 simp13 987 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( C `  i
)  e.  CC )
9897, 84subcld 9173 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( C `  i )  -  ( A `  i )
)  e.  CC )
9996, 98mulcld 8871 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  e.  CC )
100 subadd2 9071 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( B `  i
)  e.  CC  /\  ( A `  i )  e.  CC  /\  (
( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  e.  CC )  ->  ( ( ( B `  i )  -  ( A `  i ) )  =  ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  <->  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  =  ( B `
 i ) ) )
101100bicomd 192 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B `  i
)  e.  CC  /\  ( A `  i )  e.  CC  /\  (
( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  e.  CC )  ->  ( ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  =  ( B `
 i )  <->  ( ( B `  i )  -  ( A `  i ) )  =  ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) ) ) )
10283, 84, 99, 101syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  =  ( B `
 i )  <->  ( ( B `  i )  -  ( A `  i ) )  =  ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) ) ) )
10387, 98, 89, 95div23d 9589 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  /  (
( C `  p
)  -  ( A `
 p ) ) )  =  ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) ) )
104103eqeq2d 2307 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( B `
 i )  -  ( A `  i ) )  =  ( ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  <->  ( ( B `  i )  -  ( A `  i ) )  =  ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) ) ) )
105 eqcom 2298 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B `  i
)  -  ( A `
 i ) )  =  ( ( ( ( B `  p
)  -  ( A `
 p ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  /  (
( C `  p
)  -  ( A `
 p ) ) )  <->  ( ( ( ( B `  p
)  -  ( A `
 p ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  /  (
( C `  p
)  -  ( A `
 p ) ) )  =  ( ( B `  i )  -  ( A `  i ) ) )
10687, 98mulcld 8871 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( B `
 p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i ) ) )  e.  CC )
10783, 84subcld 9173 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( B `  i )  -  ( A `  i )
)  e.  CC )
108106, 89, 107, 95divmuld 9574 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( ( ( B `  p
)  -  ( A `
 p ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  /  (
( C `  p
)  -  ( A `
 p ) ) )  =  ( ( B `  i )  -  ( A `  i ) )  <->  ( (
( C `  p
)  -  ( A `
 p ) )  x.  ( ( B `
 i )  -  ( A `  i ) ) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
10989, 107mulcomd 8872 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( C `
 p )  -  ( A `  p ) )  x.  ( ( B `  i )  -  ( A `  i ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) ) )
110109eqeq1d 2304 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( ( C `  p )  -  ( A `  p ) )  x.  ( ( B `  i )  -  ( A `  i )
) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <-> 
( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) )
111108, 110bitrd 244 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( ( ( B `  p
)  -  ( A `
 p ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  /  (
( C `  p
)  -  ( A `
 p ) ) )  =  ( ( B `  i )  -  ( A `  i ) )  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
112105, 111syl5bb 248 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( B `
 i )  -  ( A `  i ) )  =  ( ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
113102, 104, 1123bitr2d 272 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  =  ( B `
 i )  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
11482, 113syl5bb 248 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  i )  e.  CC  /\  ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  /\  ( ( A `  p )  e.  CC  /\  ( B `  p
)  e.  CC  /\  ( C `  p )  e.  CC )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  <-> 
( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) )
11574, 80, 81, 114syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p
) ) )  /\  i  e.  ( 1 ... N ) )  ->  ( ( B `
 i )  =  ( ( ( ( ( B `  p
)  -  ( A `
 p ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  <-> 
( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) )
116115ralbidva 2572 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p
) ) )  -> 
( A. i  e.  ( 1 ... N
) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  <->  A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  p )  -  ( A `  p ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) ) )
117 3simpb 953 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( A  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) ) )
118 simpl2 959 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( B `  p
)  e.  RR )
119 simpl1 958 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( A `  p
)  e.  RR )
120118, 119resubcld 9227 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( B `  p )  -  ( A `  p )
)  e.  RR )
121 simpl3 960 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( C `  p
)  e.  RR )
122121, 119resubcld 9227 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( C `  p )  -  ( A `  p )
)  e.  RR )
123 simp3 957 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  RR )
124123recnd 8877 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  CC )
125753ad2ant1 976 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( A `  p )  e.  CC )
126124, 125, 92syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =  0  <->  ( C `  p )  =  ( A `  p ) ) )
127126necon3bid 2494 . . . . . . . . . . . . . . 15  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =/=  0  <->  ( C `  p )  =/=  ( A `  p
) ) )
128127biimpar 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( C `  p )  -  ( A `  p )
)  =/=  0 )
129120, 122, 128redivcld 9604 . . . . . . . . . . . . 13  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  e.  RR )
130 colinearalglem4 24609 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( B `  p
)  -  ( A `
 p ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  e.  RR )  ->  ( A. i  e.  ( 1 ... N
) ( ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C `
 i )  -  ( ( ( ( ( B `  p
)  -  ( A `
 p ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) ) )  x.  ( ( A `  i )  -  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) )  <_ 
0  \/  A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( C `
 i ) ) )  <_  0 ) )
131 oveq1 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( ( B `  i )  -  ( A `  i ) )  =  ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( A `
 i ) ) )
132131oveq1d 5889 . . . . . . . . . . . . . . . . . 18  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  =  ( ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) ) )
133132breq1d 4049 . . . . . . . . . . . . . . . . 17  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( (
( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  <->  ( (
( ( ( ( ( B `  p
)  -  ( A `
 p ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0
) )
134133ralimi 2631 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  A. i  e.  ( 1 ... N
) ( ( ( ( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0  <->  ( ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0
) )
135 ralbi 2692 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 1 ... N ) ( ( ( ( B `
 i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  <->  ( (
( ( ( ( ( B `  p
)  -  ( A `
 p ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0
)  ->  ( A. i  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  <->  A. i  e.  ( 1 ... N
) ( ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0
) )
136134, 135syl 15 . . . . . . . . . . . . . . 15  |-  ( A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( A. i  e.  ( 1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  <->  A. i  e.  ( 1 ... N
) ( ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0
) )
137 oveq2 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( ( C `  i )  -  ( B `  i ) )  =  ( ( C `  i )  -  (
( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) ) ) )
138 oveq2 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( ( A `  i )  -  ( B `  i ) )  =  ( ( A `  i )  -  (
( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) ) ) )
139137, 138oveq12d 5892 . . . . . . . . . . . . . . . . . 18  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( (
( C `  i
)  -  ( B `
 i ) )  x.  ( ( A `
 i )  -  ( B `  i ) ) )  =  ( ( ( C `  i )  -  (
( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) ) )  x.  ( ( A `  i )  -  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) ) )
140139breq1d 4049 . . . . . . . . . . . . . . . . 17  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( (
( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  <->  ( (
( C `  i
)  -  ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) )  x.  (
( A `  i
)  -  ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) )  <_ 
0 ) )
141140ralimi 2631 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  A. i  e.  ( 1 ... N
) ( ( ( ( C `  i
)  -  ( B `
 i ) )  x.  ( ( A `
 i )  -  ( B `  i ) ) )  <_  0  <->  ( ( ( C `  i )  -  (
( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) ) )  x.  ( ( A `  i )  -  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) )  <_ 
0 ) )
142 ralbi 2692 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 1 ... N ) ( ( ( ( C `
 i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  <->  ( (
( C `  i
)  -  ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) )  x.  (
( A `  i
)  -  ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) )  <_ 
0 )  ->  ( A. i  e.  (
1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  <->  A. i  e.  ( 1 ... N
) ( ( ( C `  i )  -  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) )  x.  (
( A `  i
)  -  ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) )  <_ 
0 ) )
143141, 142syl 15 . . . . . . . . . . . . . . 15  |-  ( A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( A. i  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  <->  A. i  e.  ( 1 ... N
) ( ( ( C `  i )  -  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) )  x.  (
( A `  i
)  -  ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) )  <_ 
0 ) )
144 oveq1 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( ( B `  i )  -  ( C `  i ) )  =  ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( C `
 i ) ) )
145144oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( (
( A `  i
)  -  ( C `
 i ) )  x.  ( ( B `
 i )  -  ( C `  i ) ) )  =  ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( C `  i ) ) ) )
146145breq1d 4049 . . . . . . . . . . . . . . . . 17  |-  ( ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( (
( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0  <->  ( (
( A `  i
)  -  ( C `
 i ) )  x.  ( ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( C `
 i ) ) )  <_  0 ) )
147146ralimi 2631 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  A. i  e.  ( 1 ... N
) ( ( ( ( A `  i
)  -  ( C `
 i ) )  x.  ( ( B `
 i )  -  ( C `  i ) ) )  <_  0  <->  ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( C `  i ) ) )  <_  0 ) )
148 ralbi 2692 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 1 ... N ) ( ( ( ( A `
 i )  -  ( C `  i ) )  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0  <->  ( (
( A `  i
)  -  ( C `
 i ) )  x.  ( ( ( ( ( ( B `
 p )  -  ( A `  p ) )  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( C `
 i ) ) )  <_  0 )  ->  ( A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( B `  i )  -  ( C `  i )
) )  <_  0  <->  A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( C `  i ) ) )  <_  0 ) )
149147, 148syl 15 . . . . . . . . . . . . . . 15  |-  ( A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0  <->  A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( C `
 i ) ) )  <_  0 ) )
150136, 143, 1493orbi123d 1251 . . . . . . . . . . . . . 14  |-  ( A. i  e.  ( 1 ... N ) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  ->  ( ( A. i  e.  (
1 ... N ) ( ( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C `  i )  -  ( B `  i )
)  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0 )  <->  ( A. i  e.  ( 1 ... N ) ( ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C `
 i )  -  ( ( ( ( ( B `  p
)  -  ( A `
 p ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) ) )  x.  ( ( A `  i )  -  ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) ) ) )  <_ 
0  \/  A. i  e.  ( 1 ... N
) ( ( ( A `  i )  -  ( C `  i ) )  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( C `
 i ) ) )  <_  0 ) ) )
151130, 150syl5ibrcom 213 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( B `  p
)  -  ( A `
 p ) )  /  ( ( C `
 p )  -  ( A `  p ) ) )  e.  RR )  ->  ( A. i  e.  ( 1 ... N
) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  ->  ( A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C `
 i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0 ) ) )
152117, 129, 151syl2an 463 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p
) ) )  -> 
( A. i  e.  ( 1 ... N
) ( B `  i )  =  ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  ->  ( A. i  e.  ( 1 ... N
) ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( C