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

Theorem colinearalg 23156
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 23151. (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 23151 . . 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 23151 . . . . 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 1195 . . . 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 23154 . . . . . 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 1195 . . . . 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 703 . . . 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 253 . . 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 23151 . . . . 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 23153 . . . . . 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 703 . . . . 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 253 . . . 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 1194 . . 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 1288 . 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 23148 . . . . . . . . . . . . 13  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
15 fveecn 23148 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
16 subid 9628 . . . . . . . . . . . . . . . 16  |-  ( ( C `  i )  e.  CC  ->  (
( C `  i
)  -  ( C `
 i ) )  =  0 )
1716oveq2d 6107 . . . . . . . . . . . . . . 15  |-  ( ( C `  i )  e.  CC  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( C `  i ) )  x.  0 ) )
1817adantl 466 . . . . . . . . . . . . . 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 9609 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( B `  i )  -  ( C `  i )
)  e.  CC )
2019mul01d 9568 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  0 )  =  0 )
2118, 20eqtrd 2475 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  0 )
2214, 15, 21syl2an 477 . . . . . . . . . . . 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 827 . . . . . . . . . . 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 10411 . . . . . . . . . . 11  |-  0  <_  0
2523, 24syl6eqbr 4329 . . . . . . . . . 10  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0 )
2625ralrimiva 2799 . . . . . . . . 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 1006 . . . . . . . 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 5690 . . . . . . . . . . . 12  |-  ( C  =  A  ->  ( C `  i )  =  ( A `  i ) )
2928oveq2d 6107 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( B `  i
)  -  ( C `
 i ) )  =  ( ( B `
 i )  -  ( A `  i ) ) )
3028oveq2d 6107 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( C `  i
)  -  ( C `
 i ) )  =  ( ( C `
 i )  -  ( A `  i ) ) )
3129, 30oveq12d 6109 . . . . . . . . . 10  |-  ( C  =  A  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
3231breq1d 4302 . . . . . . . . 9  |-  ( C  =  A  ->  (
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0
) )
3332ralbidv 2735 . . . . . . . 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 220 . . . . . . 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 1157 . . . . . . 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 33 . . . . . 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 46 . . . . 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 990 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  C  e.  ( EE `  N
) )
39 simp1 988 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  A  e.  ( EE `  N
) )
40 eqeefv 23149 . . . . . . . . 9  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N ) )  -> 
( C  =  A  <->  A. p  e.  (
1 ... N ) ( C `  p )  =  ( A `  p ) ) )
4138, 39, 40syl2anc 661 . . . . . . . 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 2641 . . . . . . 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 2608 . . . . . . . . 9  |-  ( ( C `  p )  =/=  ( A `  p )  <->  -.  ( C `  p )  =  ( A `  p ) )
4443rexbii 2740 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N ) ( C `  p )  =/=  ( A `  p )  <->  E. p  e.  ( 1 ... N
)  -.  ( C `
 p )  =  ( A `  p
) )
45 rexnal 2726 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N )  -.  ( C `  p
)  =  ( A `
 p )  <->  -.  A. p  e.  ( 1 ... N
) ( C `  p )  =  ( A `  p ) )
4644, 45bitr2i 250 . . . . . . 7  |-  ( -. 
A. p  e.  ( 1 ... N ) ( C `  p
)  =  ( A `
 p )  <->  E. p  e.  ( 1 ... N
) ( C `  p )  =/=  ( A `  p )
)
4742, 46syl6bb 261 . . . . . 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 2881 . . . . . . . 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 5691 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( C `  j )  =  ( C `  p ) )
50 fveq2 5691 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( A `  j )  =  ( A `  p ) )
5149, 50oveq12d 6109 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( C `  j
)  -  ( A `
 j ) )  =  ( ( C `
 p )  -  ( A `  p ) ) )
5251oveq2d 6107 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) ) )
53 fveq2 5691 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( B `  j )  =  ( B `  p ) )
5453, 50oveq12d 6109 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( B `  j
)  -  ( A `
 j ) )  =  ( ( B `
 p )  -  ( A `  p ) ) )
5554oveq1d 6106 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
5652, 55eqeq12d 2457 . . . . . . . . . . . 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 2735 . . . . . . . . . . 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 3069 . . . . . . . . . 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 727 . . . . . . . . 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 23147 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( A `  p )  e.  RR )
61603ad2antl1 1150 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( A `  p )  e.  RR )
62 fveere 23147 . . . . . . . . . . . . . 14  |-  ( ( B  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( B `  p )  e.  RR )
63623ad2antl2 1151 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( B `  p )  e.  RR )
64 fveere 23147 . . . . . . . . . . . . . 14  |-  ( ( C  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( C `  p )  e.  RR )
65643ad2antl3 1152 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( C `  p )  e.  RR )
6661, 63, 653jca 1168 . . . . . . . . . . . 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 568 . . . . . . . . . . 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 647 . . . . . . . . . 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 23148 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  CC )
70693ad2antl1 1150 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( A `  i )  e.  CC )
71143ad2antl2 1151 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( B `  i )  e.  CC )
72153ad2antl3 1152 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( C `  i )  e.  CC )
7370, 71, 723jca 1168 . . . . . . . . . . . . . 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 714 . . . . . . . . . . . . 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 9372 . . . . . . . . . . . . . . . 16  |-  ( ( A `  p )  e.  RR  ->  ( A `  p )  e.  CC )
76 recn 9372 . . . . . . . . . . . . . . . 16  |-  ( ( B `  p )  e.  RR  ->  ( B `  p )  e.  CC )
77 recn 9372 . . . . . . . . . . . . . . . 16  |-  ( ( C `  p )  e.  RR  ->  ( C `  p )  e.  CC )
7875, 76, 773anim123i 1173 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . 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 760 . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . . 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 1019 . . . . . . . . . . . . . . . 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 1018 . . . . . . . . . . . . . . . 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 1022 . . . . . . . . . . . . . . . . . . 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 1021 . . . . . . . . . . . . . . . . . . 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 9719 . . . . . . . . . . . . . . . . . 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 1023 . . . . . . . . . . . . . . . . . . 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 9719 . . . . . . . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . . . . . . 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 994 . . . . . . . . . . . . . . . . . . . . 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 9729 . . . . . . . . . . . . . . . . . . . 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 2643 . . . . . . . . . . . . . . . . . . 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 1319 . . . . . . . . . . . . . . . . . 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 10107 . . . . . . . . . . . . . . . . 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 1020 . . . . . . . . . . . . . . . . . 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 9719 . . . . . . . . . . . . . . . . 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 9406 . . . . . . . . . . . . . . . 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 9614 . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . 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 10144 . . . . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . . . . 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 9406 . . . . . . . . . . . . . . . . . 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 9719 . . . . . . . . . . . . . . . . . 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 10129 . . . . . . . . . . . . . . . . 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 9407 . . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . 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 281 . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . 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 1218 . . . . . . . . . . . 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 2731 . . . . . . . . . . 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 986 . . . . . . . . . . . 12  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( A  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) ) )
117 simpl2 992 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( B `  p
)  e.  RR )
118 simpl1 991 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( A `  p
)  e.  RR )
119117, 118resubcld 9776 . . . . . . . . . . . . 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 993 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( C `  p
)  e.  RR )
121120, 118resubcld 9776 . . . . . . . . . . . . 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 990 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  RR )
123122recnd 9412 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  CC )
124753ad2ant1 1009 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( A `  p )  e.  CC )
125123, 124subeq0ad 9729 . . . . . . . . . . . . . . 15  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =  0  <->  ( C `  p )  =  ( A `  p ) ) )
126125necon3bid 2643 . . . . . . . . . . . . . 14  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =/=  0  <->  ( C `  p )  =/=  ( A `  p
) ) )
127126biimpar 485 . . . . . . . . . . . . 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 10159 . . . . . . . . . . . 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 23155 . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . 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 6106 . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . 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 2853 . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . 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 6099 . . . . . . . . . . . . . . . . . 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 6099 . . . . . . . . . . . . . . . . . 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 6109 . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . 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 2853 . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . 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 6107 . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . 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 2853 . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . 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 1288 . . . . . . . . . . . . 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 222 . . . . . . . . . . . 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 477 . . . . . . . . . . 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 235 . . . . . . . . . 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 )
) )  =  ( (