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

Theorem colinearalg 23075
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 23070. (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 23070 . . 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 23070 . . . . 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 1190 . . . 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 23073 . . . . . 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 1190 . . . . 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 698 . . . 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 23070 . . . . 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 23072 . . . . . 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 698 . . . . 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 1189 . . 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 1283 . 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 23067 . . . . . . . . . . . . 13  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
15 fveecn 23067 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
16 subid 9624 . . . . . . . . . . . . . . . 16  |-  ( ( C `  i )  e.  CC  ->  (
( C `  i
)  -  ( C `
 i ) )  =  0 )
1716oveq2d 6106 . . . . . . . . . . . . . . 15  |-  ( ( C `  i )  e.  CC  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( C `  i ) )  x.  0 ) )
1817adantl 463 . . . . . . . . . . . . . 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 9605 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( B `  i )  -  ( C `  i )
)  e.  CC )
2019mul01d 9564 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  0 )  =  0 )
2118, 20eqtrd 2473 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  0 )
2214, 15, 21syl2an 474 . . . . . . . . . . . 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 822 . . . . . . . . . . 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 10407 . . . . . . . . . . 11  |-  0  <_  0
2523, 24syl6eqbr 4326 . . . . . . . . . 10  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0 )
2625ralrimiva 2797 . . . . . . . . 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 1001 . . . . . . . 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 5687 . . . . . . . . . . . 12  |-  ( C  =  A  ->  ( C `  i )  =  ( A `  i ) )
2928oveq2d 6106 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( B `  i
)  -  ( C `
 i ) )  =  ( ( B `
 i )  -  ( A `  i ) ) )
3028oveq2d 6106 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( C `  i
)  -  ( C `
 i ) )  =  ( ( C `
 i )  -  ( A `  i ) ) )
3129, 30oveq12d 6108 . . . . . . . . . 10  |-  ( C  =  A  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
3231breq1d 4299 . . . . . . . . 9  |-  ( C  =  A  ->  (
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0
) )
3332ralbidv 2733 . . . . . . . 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 1152 . . . . . . 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 985 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  C  e.  ( EE `  N
) )
39 simp1 983 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  A  e.  ( EE `  N
) )
40 eqeefv 23068 . . . . . . . . 9  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N ) )  -> 
( C  =  A  <->  A. p  e.  (
1 ... N ) ( C `  p )  =  ( A `  p ) ) )
4138, 39, 40syl2anc 656 . . . . . . . 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 2639 . . . . . . 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 2606 . . . . . . . . 9  |-  ( ( C `  p )  =/=  ( A `  p )  <->  -.  ( C `  p )  =  ( A `  p ) )
4443rexbii 2738 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N ) ( C `  p )  =/=  ( A `  p )  <->  E. p  e.  ( 1 ... N
)  -.  ( C `
 p )  =  ( A `  p
) )
45 rexnal 2724 . . . . . . . 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 2879 . . . . . . . 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 5688 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( C `  j )  =  ( C `  p ) )
50 fveq2 5688 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( A `  j )  =  ( A `  p ) )
5149, 50oveq12d 6108 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( C `  j
)  -  ( A `
 j ) )  =  ( ( C `
 p )  -  ( A `  p ) ) )
5251oveq2d 6106 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) ) )
53 fveq2 5688 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( B `  j )  =  ( B `  p ) )
5453, 50oveq12d 6108 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( B `  j
)  -  ( A `
 j ) )  =  ( ( B `
 p )  -  ( A `  p ) ) )
5554oveq1d 6105 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
5652, 55eqeq12d 2455 . . . . . . . . . . . 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 2733 . . . . . . . . . . 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 3066 . . . . . . . . . 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 722 . . . . . . . . 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 23066 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( A `  p )  e.  RR )
61603ad2antl1 1145 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( A `  p )  e.  RR )
62 fveere 23066 . . . . . . . . . . . . . 14  |-  ( ( B  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( B `  p )  e.  RR )
63623ad2antl2 1146 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( B `  p )  e.  RR )
64 fveere 23066 . . . . . . . . . . . . . 14  |-  ( ( C  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( C `  p )  e.  RR )
65643ad2antl3 1147 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( C `  p )  e.  RR )
6661, 63, 653jca 1163 . . . . . . . . . . . 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 565 . . . . . . . . . . 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 642 . . . . . . . . . 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 23067 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  CC )
70693ad2antl1 1145 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( A `  i )  e.  CC )
71143ad2antl2 1146 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( B `  i )  e.  CC )
72153ad2antl3 1147 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( C `  i )  e.  CC )
7370, 71, 723jca 1163 . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . 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 9368 . . . . . . . . . . . . . . . 16  |-  ( ( A `  p )  e.  RR  ->  ( A `  p )  e.  CC )
76 recn 9368 . . . . . . . . . . . . . . . 16  |-  ( ( B `  p )  e.  RR  ->  ( B `  p )  e.  CC )
77 recn 9368 . . . . . . . . . . . . . . . 16  |-  ( ( C `  p )  e.  RR  ->  ( C `  p )  e.  CC )
7875, 76, 773anim123i 1168 . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . 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 755 . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . 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 1014 . . . . . . . . . . . . . . . 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 1013 . . . . . . . . . . . . . . . 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 1017 . . . . . . . . . . . . . . . . . . 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 1016 . . . . . . . . . . . . . . . . . . 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 9715 . . . . . . . . . . . . . . . . . 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 1018 . . . . . . . . . . . . . . . . . . 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 9715 . . . . . . . . . . . . . . . . . 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 991 . . . . . . . . . . . . . . . . . . . . 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 989 . . . . . . . . . . . . . . . . . . . . 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 9725 . . . . . . . . . . . . . . . . . . . 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 2641 . . . . . . . . . . . . . . . . . . 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 1314 . . . . . . . . . . . . . . . . . 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 10103 . . . . . . . . . . . . . . . . 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 1015 . . . . . . . . . . . . . . . . . 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 9715 . . . . . . . . . . . . . . . . 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 9402 . . . . . . . . . . . . . . . 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 9610 . . . . . . . . . . . . . . . . 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 1213 . . . . . . . . . . . . . . 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 10140 . . . . . . . . . . . . . . . 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 2452 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . 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 9402 . . . . . . . . . . . . . . . . . 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 9715 . . . . . . . . . . . . . . . . . 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 10125 . . . . . . . . . . . . . . . . 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 9403 . . . . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . 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 1213 . . . . . . . . . . . 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 2729 . . . . . . . . . . 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 981 . . . . . . . . . . . 12  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( A  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) ) )
117 simpl2 987 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( B `  p
)  e.  RR )
118 simpl1 986 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( A `  p
)  e.  RR )
119117, 118resubcld 9772 . . . . . . . . . . . . 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 988 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( C `  p
)  e.  RR )
121120, 118resubcld 9772 . . . . . . . . . . . . 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 985 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  RR )
123122recnd 9408 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  CC )
124753ad2ant1 1004 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( A `  p )  e.  CC )
125123, 124subeq0ad 9725 . . . . . . . . . . . . . . 15  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =  0  <->  ( C `  p )  =  ( A `  p ) ) )
126125necon3bid 2641 . . . . . . . . . . . . . 14  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =/=  0  <->  ( C `  p )  =/=  ( A `  p
) ) )
127126biimpar 482 . . . . . . . . . . . . 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 10155 . . . . . . . . . . . 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 23074 . . . . . . . . . . . . 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 6097 . . . . . . . . . . . . . . . . . 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 6105 . . . . . . . . . . . . . . . . 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 4299 . . . . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . . . 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 2851 . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . 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 6108 . . . . . . . . . . . . . . . . 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 4299 . . . . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . . . 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 2851 . . . . . . . . . . . . . . 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 6097 . . . . . . . . . . . . . . . . . 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 6106 . . . . . . . . . . . . . . . . 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 4299 . . . . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . . . 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 2851 . . . . . . . . . . . . . . 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 1283 . . . . . . . . . . . . 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 474 . . . . . . . . . . 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 )
) )  =  ( (