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

Theorem colinearalg 25814
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 25809. (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 25809 . . 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 25809 . . . . 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 1161 . . . 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 25812 . . . . . 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 1161 . . . . 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 685 . . . 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 245 . . 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 25809 . . . . 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 25811 . . . . . 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 685 . . . . 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 245 . . . 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 1160 . . 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 1253 . 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 25806 . . . . . . . . . . . . 13  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
15 fveecn 25806 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
16 subid 9311 . . . . . . . . . . . . . . . 16  |-  ( ( C `  i )  e.  CC  ->  (
( C `  i
)  -  ( C `
 i ) )  =  0 )
1716oveq2d 6089 . . . . . . . . . . . . . . 15  |-  ( ( C `  i )  e.  CC  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( C `  i ) )  x.  0 ) )
1817adantl 453 . . . . . . . . . . . . . 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 9295 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( B `  i )  -  ( C `  i )
)  e.  CC )
2019mul01d 9255 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  0 )  =  0 )
2118, 20eqtrd 2467 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  0 )
2214, 15, 21syl2an 464 . . . . . . . . . . . 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 805 . . . . . . . . . . 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 10071 . . . . . . . . . . 11  |-  0  <_  0
2523, 24syl6eqbr 4241 . . . . . . . . . 10  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0 )
2625ralrimiva 2781 . . . . . . . . 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 975 . . . . . . . 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 5719 . . . . . . . . . . . 12  |-  ( C  =  A  ->  ( C `  i )  =  ( A `  i ) )
2928oveq2d 6089 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( B `  i
)  -  ( C `
 i ) )  =  ( ( B `
 i )  -  ( A `  i ) ) )
3028oveq2d 6089 . . . . . . . . . . 11  |-  ( C  =  A  ->  (
( C `  i
)  -  ( C `
 i ) )  =  ( ( C `
 i )  -  ( A `  i ) ) )
3129, 30oveq12d 6091 . . . . . . . . . 10  |-  ( C  =  A  ->  (
( ( B `  i )  -  ( C `  i )
)  x.  ( ( C `  i )  -  ( C `  i ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
3231breq1d 4214 . . . . . . . . 9  |-  ( C  =  A  ->  (
( ( ( B `
 i )  -  ( C `  i ) )  x.  ( ( C `  i )  -  ( C `  i ) ) )  <_  0  <->  ( (
( B `  i
)  -  ( A `
 i ) )  x.  ( ( C `
 i )  -  ( A `  i ) ) )  <_  0
) )
3332ralbidv 2717 . . . . . . . 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 212 . . . . . . 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 1126 . . . . . . 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 31 . . . . . 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 44 . . . . 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 959 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  C  e.  ( EE `  N
) )
39 simp1 957 . . . . . . . . 9  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  A  e.  ( EE `  N
) )
40 eqeefv 25807 . . . . . . . . 9  |-  ( ( C  e.  ( EE
`  N )  /\  A  e.  ( EE `  N ) )  -> 
( C  =  A  <->  A. p  e.  (
1 ... N ) ( C `  p )  =  ( A `  p ) ) )
4138, 39, 40syl2anc 643 . . . . . . . 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 2631 . . . . . . 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 2600 . . . . . . . . 9  |-  ( ( C `  p )  =/=  ( A `  p )  <->  -.  ( C `  p )  =  ( A `  p ) )
4443rexbii 2722 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N ) ( C `  p )  =/=  ( A `  p )  <->  E. p  e.  ( 1 ... N
)  -.  ( C `
 p )  =  ( A `  p
) )
45 rexnal 2708 . . . . . . . 8  |-  ( E. p  e.  ( 1 ... N )  -.  ( C `  p
)  =  ( A `
 p )  <->  -.  A. p  e.  ( 1 ... N
) ( C `  p )  =  ( A `  p ) )
4644, 45bitr2i 242 . . . . . . 7  |-  ( -. 
A. p  e.  ( 1 ... N ) ( C `  p
)  =  ( A `
 p )  <->  E. p  e.  ( 1 ... N
) ( C `  p )  =/=  ( A `  p )
)
4742, 46syl6bb 253 . . . . . 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 2860 . . . . . . . 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 5720 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( C `  j )  =  ( C `  p ) )
50 fveq2 5720 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( A `  j )  =  ( A `  p ) )
5149, 50oveq12d 6091 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( C `  j
)  -  ( A `
 j ) )  =  ( ( C `
 p )  -  ( A `  p ) ) )
5251oveq2d 6089 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  i )  -  ( A `  i )
)  x.  ( ( C `  j )  -  ( A `  j ) ) )  =  ( ( ( B `  i )  -  ( A `  i ) )  x.  ( ( C `  p )  -  ( A `  p )
) ) )
53 fveq2 5720 . . . . . . . . . . . . . . 15  |-  ( j  =  p  ->  ( B `  j )  =  ( B `  p ) )
5453, 50oveq12d 6091 . . . . . . . . . . . . . 14  |-  ( j  =  p  ->  (
( B `  j
)  -  ( A `
 j ) )  =  ( ( B `
 p )  -  ( A `  p ) ) )
5554oveq1d 6088 . . . . . . . . . . . . 13  |-  ( j  =  p  ->  (
( ( B `  j )  -  ( A `  j )
)  x.  ( ( C `  i )  -  ( A `  i ) ) )  =  ( ( ( B `  p )  -  ( A `  p ) )  x.  ( ( C `  i )  -  ( A `  i )
) ) )
5652, 55eqeq12d 2449 . . . . . . . . . . . 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 2717 . . . . . . . . . . 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 3040 . . . . . . . . . 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 709 . . . . . . . . 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 25805 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( A `  p )  e.  RR )
61603ad2antl1 1119 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( A `  p )  e.  RR )
62 fveere 25805 . . . . . . . . . . . . . 14  |-  ( ( B  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( B `  p )  e.  RR )
63623ad2antl2 1120 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( B `  p )  e.  RR )
64 fveere 25805 . . . . . . . . . . . . . 14  |-  ( ( C  e.  ( EE
`  N )  /\  p  e.  ( 1 ... N ) )  ->  ( C `  p )  e.  RR )
65643ad2antl3 1121 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  p  e.  ( 1 ... N
) )  ->  ( C `  p )  e.  RR )
6661, 63, 653jca 1134 . . . . . . . . . . . 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 552 . . . . . . . . . . 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 629 . . . . . . . . . 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 25806 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  CC )
70693ad2antl1 1119 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( A `  i )  e.  CC )
71143ad2antl2 1120 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( B `  i )  e.  CC )
72153ad2antl3 1121 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( C `  i )  e.  CC )
7370, 71, 723jca 1134 . . . . . . . . . . . . . 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 696 . . . . . . . . . . . . 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 9070 . . . . . . . . . . . . . . . 16  |-  ( ( A `  p )  e.  RR  ->  ( A `  p )  e.  CC )
76 recn 9070 . . . . . . . . . . . . . . . 16  |-  ( ( B `  p )  e.  RR  ->  ( B `  p )  e.  CC )
77 recn 9070 . . . . . . . . . . . . . . . 16  |-  ( ( C `  p )  e.  RR  ->  ( C `  p )  e.  CC )
7875, 76, 773anim123i 1139 . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . 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 738 . . . . . . . . . . . . 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 2437 . . . . . . . . . . . . . 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 988 . . . . . . . . . . . . . . . 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 987 . . . . . . . . . . . . . . . 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 991 . . . . . . . . . . . . . . . . . . 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 990 . . . . . . . . . . . . . . . . . . 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 9401 . . . . . . . . . . . . . . . . . 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 992 . . . . . . . . . . . . . . . . . . 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 9401 . . . . . . . . . . . . . . . . . 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 965 . . . . . . . . . . . . . . . . . . . . 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 963 . . . . . . . . . . . . . . . . . . . . 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 9411 . . . . . . . . . . . . . . . . . . . 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 2633 . . . . . . . . . . . . . . . . . . 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 1284 . . . . . . . . . . . . . . . . . 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 9780 . . . . . . . . . . . . . . . . 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 989 . . . . . . . . . . . . . . . . . 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 9401 . . . . . . . . . . . . . . . . 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 9098 . . . . . . . . . . . . . . . 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 9299 . . . . . . . . . . . . . . . . 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 193 . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . 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 9817 . . . . . . . . . . . . . . . 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 2446 . . . . . . . . . . . . . . 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 2437 . . . . . . . . . . . . . . . 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 9098 . . . . . . . . . . . . . . . . . 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 9401 . . . . . . . . . . . . . . . . . 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 9802 . . . . . . . . . . . . . . . . 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 9099 . . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . . 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 245 . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . 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 273 . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . 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 1184 . . . . . . . . . . . 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 2713 . . . . . . . . . . 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 955 . . . . . . . . . . . 12  |-  ( ( A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( A  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) ) )
117 simpl2 961 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( B `  p
)  e.  RR )
118 simpl1 960 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( A `  p
)  e.  RR )
119117, 118resubcld 9455 . . . . . . . . . . . . 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 962 . . . . . . . . . . . . . 14  |-  ( ( ( ( A `  p )  e.  RR  /\  ( B `  p
)  e.  RR  /\  ( C `  p )  e.  RR )  /\  ( C `  p )  =/=  ( A `  p ) )  -> 
( C `  p
)  e.  RR )
121120, 118resubcld 9455 . . . . . . . . . . . . 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 959 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  RR )
123122recnd 9104 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( C `  p )  e.  CC )
124753ad2ant1 978 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  ( A `  p )  e.  CC )
125123, 124subeq0ad 9411 . . . . . . . . . . . . . . 15  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =  0  <->  ( C `  p )  =  ( A `  p ) ) )
126125necon3bid 2633 . . . . . . . . . . . . . 14  |-  ( ( ( A `  p
)  e.  RR  /\  ( B `  p )  e.  RR  /\  ( C `  p )  e.  RR )  ->  (
( ( C `  p )  -  ( A `  p )
)  =/=  0  <->  ( C `  p )  =/=  ( A `  p
) ) )
127126biimpar 472 . . . . . . . . . . . . 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 9832 . . . . . . . . . . . 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 25813 . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . 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 6088 . . . . . . . . . . . . . . . . 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 4214 . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . 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 2834 . . . . . . . . . . . . . . 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 6081 . . . . . . . . . . . . . . . . . 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 6081 . . . . . . . . . . . . . . . . . 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 6091 . . . . . . . . . . . . . . . . 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 4214 . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . 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 2834 . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . 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 6089 . . . . . . . . . . . . . . . . 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 4214 . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . 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 2834 . . . . . . . . . . . . . . 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 1253 . . . . . . . . . . . . 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 214 . . . . . . . . . . . 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 464 . . . . . . . . . . 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 227 . . . . . . . . . 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 )
) )  =