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

Theorem colinearalg 24952
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 24947. (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 24947 . . 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 24947 . . . . 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 1217 . . . 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 24950 . . . . . 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 1217 . . . . 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 711 . . . 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 257 . . 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 24947 . . . . 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 24949 . . . . . 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 711 . . . . 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 257 . . . 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 1216 . . 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 1340 . 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 24944 . . . . . . . . . . . . 13  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
15 fveecn 24944 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
16 subid 9898 . . . . . . . . . . . . . . . 16  |-  ( ( C `  i )  e.  CC  ->  (
( C `  i
)  -  ( C `
 i ) )  =  0 )
1716oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( ( C `  i )  e.  CC  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( C `  i ) )  x.  0 ) )
1817adantl 468 . . . . . . . . . . . . . 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 9879 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( B `  i )  -  ( C `  i )
)  e.  CC )
2019mul01d 9837 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  0 )  =  0 )
2118, 20eqtrd 2487 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  0 )
2214, 15, 21syl2an 480 . . . . . . . . . . . 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 841 . . . . . . . . . . 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 10706 . . . . . . . . . . 11  |-  0  <_  0
2523, 24syl6eqbr 4443 . . . . . . . . . 10  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0 )
2625ralrimiva 2804 . . . . . . . . 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 1027 . . . . . . . 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 5869 . . . . . . . . . . . 12  |-  ( C  =  A  ->  ( C `  i )  =  ( A `  i ) )
2928oveq2d 6311 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( B `  i
)  -  ( C `
 i ) )  =  ( ( B `
 i )  -  ( A `  i ) ) )
3028oveq2d 6311 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( C `  i
)  -  ( C `
 i ) )  =  ( ( C `
 i )  -  ( A `  i ) ) )
3129, 30oveq12d 6313 . . . . . . . . . 10  |-  ( C  =  A  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
3231breq1d 4415 . . . . . . . . 9  |-  ( C  =  A  ->  (
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0
) )
3332ralbidv 2829 . . . . . . . 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 224 . . . . . . 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 1178 . . . . . . 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 34 . . . . . 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 47 . . . . 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 1011 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  C  e.  ( EE `  N
) )
39 simp1 1009 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  A  e.  ( EE `  N
) )
40 eqeefv 24945 . . . . . . . . 9  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N ) )  -> 
( C  =  A  <->  A. p  e.  (
1 ... N ) ( C `  p )  =  ( A `  p ) ) )
4138, 39, 40syl2anc 667 . . . . . . . 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 2662 . . . . . . 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 2626 . . . . . . . . 9  |-  ( ( C `  p )  =/=  ( A `  p )  <->  -.  ( C `  p )  =  ( A `  p ) )
4443rexbii 2891 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N ) ( C `  p )  =/=  ( A `  p )  <->  E. p  e.  ( 1 ... N
)  -.  ( C `
 p )  =  ( A `  p
) )
45 rexnal 2838 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N )  -.  ( C `  p
)  =  ( A `
 p )  <->  -.  A. p  e.  ( 1 ... N
) ( C `  p )  =  ( A `  p ) )
4644, 45bitr2i 254 . . . . . . 7  |-  ( -. 
A. p  e.  ( 1 ... N ) ( C `  p
)  =  ( A `
 p )  <->  E. p  e.  ( 1 ... N
) ( C `  p )  =/=  ( A `  p )
)
4742, 46syl6bb 265 . . . . . 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 2953 . . . . . . . 8  |-  ( 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 5870 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( C `  j )  =  ( C `  p ) )
50 fveq2 5870 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( A `  j )  =  ( A `  p ) )
5149, 50oveq12d 6313 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( C `  j
)  -  ( A `
 j ) )  =  ( ( C `
 p )  -  ( A `  p ) ) )
5251oveq2d 6311 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) ) )
53 fveq2 5870 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( B `  j )  =  ( B `  p ) )
5453, 50oveq12d 6313 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( B `  j
)  -  ( A `
 j ) )  =  ( ( B `
 p )  -  ( A `  p ) ) )
5554oveq1d 6310 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
5652, 55eqeq12d 2468 . . . . . . . . . . . 12  |-  ( 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 2829 . . . . . . . . . . 11  |-  ( 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 3148 . . . . . . . . . 10  |-  ( 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 735 . . . . . . . . 9  |-  ( ( ( 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 24943 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( A `  p )  e.  RR )
61603ad2antl1 1171 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( A `  p )  e.  RR )
62 fveere 24943 . . . . . . . . . . . . . 14  |-  ( ( B  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( B `  p )  e.  RR )
63623ad2antl2 1172 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( B `  p )  e.  RR )
64 fveere 24943 . . . . . . . . . . . . . 14  |-  ( ( C  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( C `  p )  e.  RR )
65643ad2antl3 1173 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( C `  p )  e.  RR )
6661, 63, 653jca 1189 . . . . . . . . . . . 12  |-  ( ( ( 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 572 . . . . . . . . . . 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 ) ) )
6867anasss 653 . . . . . . . . . 10  |-  ( ( ( 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 24944 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  CC )
70693ad2antl1 1171 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( A `  i )  e.  CC )
71143ad2antl2 1172 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( B `  i )  e.  CC )
72153ad2antl3 1173 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( C `  i )  e.  CC )
7370, 71, 723jca 1189 . . . . . . . . . . . . . 14  |-  ( ( ( 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 722 . . . . . . . . . . . . 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 ) )  ->  ( ( A `
 i )  e.  CC  /\  ( B `
 i )  e.  CC  /\  ( C `
 i )  e.  CC ) )
75 recn 9634 . . . . . . . . . . . . . . . 16  |-  ( ( A `  p )  e.  RR  ->  ( A `  p )  e.  CC )
76 recn 9634 . . . . . . . . . . . . . . . 16  |-  ( ( B `  p )  e.  RR  ->  ( B `  p )  e.  CC )
77 recn 9634 . . . . . . . . . . . . . . . 16  |-  ( ( C `  p )  e.  RR  ->  ( C `  p )  e.  CC )
7875, 76, 773anim123i 1194 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 734 . . . . . . . . . . . . 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 ) )  ->  ( ( A `
 p )  e.  CC  /\  ( B `
 p )  e.  CC  /\  ( C `
 p )  e.  CC ) )
81 simplrr 772 . . . . . . . . . . . . 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 ) )  ->  ( C `  p )  =/=  ( A `  p )
)
82 eqcom 2460 . . . . . . . . . . . . . 14  |-  ( ( 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 1040 . . . . . . . . . . . . . . . 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
)  e.  CC )
84 simp11 1039 . . . . . . . . . . . . . . . 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 ) )  -> 
( A `  i
)  e.  CC )
85 simp22 1043 . . . . . . . . . . . . . . . . . . 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
)  e.  CC )
86 simp21 1042 . . . . . . . . . . . . . . . . . . 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 ) )  -> 
( A `  p
)  e.  CC )
8785, 86subcld 9991 . . . . . . . . . . . . . . . . . 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 )
)  e.  CC )
88 simp23 1044 . . . . . . . . . . . . . . . . . . 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
)  e.  CC )
8988, 86subcld 9991 . . . . . . . . . . . . . . . . . 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 )
)  e.  CC )
90 simpr3 1017 . . . . . . . . . . . . . . . . . . . . 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 )  e.  CC )
91 simpr1 1015 . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  ( A `  p )  e.  CC )
9290, 91subeq0ad 10001 . . . . . . . . . . . . . . . . . . . 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 ) ) )
9392necon3bid 2670 . . . . . . . . . . . . . . . . . . 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 ) )  =/=  0  <->  ( C `  p )  =/=  ( A `  p )
) )
9493biimp3ar 1372 . . . . . . . . . . . . . . . . . 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 )
)  =/=  0 )
9587, 89, 94divcld 10390 . . . . . . . . . . . . . . . . 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 ) ) )  e.  CC )
96 simp13 1041 . . . . . . . . . . . . . . . . . 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
)  e.  CC )
9796, 84subcld 9991 . . . . . . . . . . . . . . . . 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 ) )  -> 
( ( C `  i )  -  ( A `  i )
)  e.  CC )
9895, 97mulcld 9668 . . . . . . . . . . . . . . . 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 ) ) )  e.  CC )
99 subadd2 9884 . . . . . . . . . . . . . . . . 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 `  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 ) ) )
10099bicomd 205 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) ) )
10183, 84, 98, 100syl3anc 1269 . . . . . . . . . . . . . . 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 ) )  =  ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) ) ) )
10287, 97, 89, 94div23d 10427 . . . . . . . . . . . . . . . 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 ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  /  (
( C `  p
)  -  ( A `
 p ) ) )  =  ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) ) )
103102eqeq2d 2463 . . . . . . . . . . . . . . 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 `
 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 ) ) ) ) )
104 eqcom 2460 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
10587, 97mulcld 9668 . . . . . . . . . . . . . . . . . 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 ) ) )  e.  CC )
10683, 84subcld 9991 . . . . . . . . . . . . . . . . . 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 `  i )  -  ( A `  i )
)  e.  CC )
107105, 89, 106, 94divmuld 10412 . . . . . . . . . . . . . . . . 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 ) )  <->  ( (
( C `  p
)  -  ( A `
 p ) )  x.  ( ( B `
 i )  -  ( A `  i ) ) )  =  ( ( ( B `  p )  -  ( A `  p )
)  x.  ( ( C `  i )  -  ( A `  i ) ) ) ) )
10889, 106mulcomd 9669 . . . . . . . . . . . . . . . . . 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 `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) ) )
109108eqeq1d 2455 . . . . . . . . . . . . . . . . 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 ) )  -> 
( ( ( ( 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 )
) ) ) )
110107, 109bitrd 257 . . . . . . . . . . . . . . . 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 ) )  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 ) ) ) ) )
111104, 110syl5bb 261 . . . . . . . . . . . . . . 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 `
 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 ) ) ) ) )
112101, 103, 1113bitr2d 285 . . . . . . . . . . . . . 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 `  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 ) ) ) ) )
11382, 112syl5bb 261 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) ) )
11474, 80, 81, 113syl3anc 1269 . . . . . . . . . . . 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
) ) )  /\  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 )
) ) ) )
115114ralbidva 2826 . . . . . . . . . . 11  |-  ( ( ( 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 )
) ) ) )
116 3simpb 1007 . . . . . . . . . . . 12  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( A  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) ) )
117 simpl2 1013 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( B `  p
)  e.  RR )
118 simpl1 1012 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( A `  p
)  e.  RR )
119117, 118resubcld 10054 . . . . . . . . . . . . 13  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( B `  p )  -  ( A `  p )
)  e.  RR )
120 simpl3 1014 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( C `  p
)  e.  RR )
121120, 118resubcld 10054 . . . . . . . . . . . . 13  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( C `  p )  -  ( A `  p )
)  e.  RR )
122 simp3 1011 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  RR )
123122recnd 9674 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  CC )
124753ad2ant1 1030 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( A `  p )  e.  CC )
125123, 124subeq0ad 10001 . . . . . . . . . . . . . . 15  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =  0  <->  ( C `  p )  =  ( A `  p ) ) )
126125necon3bid 2670 . . . . . . . . . . . . . 14  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =/=  0  <->  ( C `  p )  =/=  ( A `  p
) ) )
127126biimpar 488 . . . . . . . . . . . . 13  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( ( C `  p )  -  ( A `  p )
)  =/=  0 )
128119, 121, 127redivcld 10442 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
129 colinearalglem4 24951 . . . . . . . . . . . . 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 `  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 ) )
130 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
131130oveq1d 6310 . . . . . . . . . . . . . . . . 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 ) ) )  =  ( ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) ) )
132131breq1d 4415 . . . . . . . . . . . . . . . 16  |-  ( ( 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
) )
133132ralimi 2783 . . . . . . . . . . . . . . 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  <->  ( ( ( ( ( ( ( B `  p )  -  ( A `  p )
)  /  ( ( C `  p )  -  ( A `  p ) ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  +  ( A `  i ) )  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0
) )
134 ralbi 2923 . . . . . . . . . . . . . . 15  |-  ( 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
) )
135133, 134syl 17 . . . . . . . . . . . . . 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
) ( ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) )  <_  0
) )
136 oveq2 6303 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) )
137 oveq2 6303 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) )
138136, 137oveq12d 6313 . . . . . . . . . . . . . . . . 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 ) ) )  =  ( ( ( 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 ) ) ) ) )
139138breq1d 4415 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) )
140139ralimi 2783 . . . . . . . . . . . . . . 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  <->  ( ( ( 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 ) )
141 ralbi 2923 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
142140, 141syl 17 . . . . . . . . . . . . . 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 ) ( ( ( 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 ) )
143 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
144143oveq2d 6311 . . . . . . . . . . . . . . . . 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 ) ) )  =  ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( C `  i ) ) ) )
145144breq1d 4415 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) )
146145ralimi 2783 . . . . . . . . . . . . . . 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 )  -  ( C `  i )
)  x.  ( ( ( ( ( ( B `  p )  -  ( A `  p ) )  / 
( ( C `  p )  -  ( A `  p )
) )  x.  (
( C `  i
)  -  ( A `
 i ) ) )  +  ( A `
 i ) )  -  ( C `  i ) ) )  <_  0 ) )
147 ralbi 2923 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
148146, 147syl 17 . . . . . . . . . . . . . 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 ) ( ( ( 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 ) )
149135, 142, 1483orbi123d 1340 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
150129, 149syl5ibrcom 226 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
151116, 128, 150syl2an 480 . . . . . . . . . . 11  |-  ( ( ( 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 `
 i )  -  ( B `  i ) )  x.  ( ( A `  i )  -  ( B `  i ) ) )  <_  0  \/  A. i  e.  ( 1 ... N ) ( ( ( A `  i )  -  ( C `  i )
)  x.  ( ( B `  i )  -  ( C `  i ) ) )  <_  0 ) ) )
152115, 151sylbird 239 . . . . . . . . . 10  |-  ( ( ( 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 )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) )  =