Metamath Proof Explorer

Theorem colinearalg

Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 . (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 brbtwn2 
 |-  ( ( 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 
 |-  ( ( 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 ) ) ) ) ) )
3 2 3comr 
 |-  ( ( 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 
 |-  ( ( 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 ) ) ) ) )
5 4 3comr 
 |-  ( ( 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 ) ) ) ) )
6 5 anbi2d 
 |-  ( ( 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 ) ) ) ) ) )
7 3 6 bitrd 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 ) ) ) ) )
10 9 anbi2d 
 |-  ( ( 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 ) ) ) ) ) )
11 8 10 bitrd 
 |-  ( ( 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 ) ) ) ) ) )
12 11 3coml 
 |-  ( ( 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 ) ) ) ) ) )
13 1 7 12 3orbi123d 
 |-  ( ( 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 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
15 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
16 subid 
 |-  ( ( C ` i ) e. CC -> ( ( C ` i ) - ( C ` i ) ) = 0 )
17 16 oveq2d 
 |-  ( ( C ` i ) e. CC -> ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` i ) - ( C ` i ) ) ) = ( ( ( B ` i ) - ( C ` i ) ) x. 0 ) )
18 17 adantl 
 |-  ( ( ( 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 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( B ` i ) - ( C ` i ) ) e. CC )
20 19 mul01d 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( ( B ` i ) - ( C ` i ) ) x. 0 ) = 0 )
21 18 20 eqtrd 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` i ) - ( C ` i ) ) ) = 0 )
22 14 15 21 syl2an 
 |-  ( ( ( 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 )
23 22 anandirs 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` i ) - ( C ` i ) ) ) = 0 )
24 0le0 
 |-  0 <_ 0
25 23 24 eqbrtrdi 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` i ) - ( C ` i ) ) ) <_ 0 )
26 25 ralrimiva 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> A. i e. ( 1 ... N ) ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` i ) - ( C ` i ) ) ) <_ 0 )
27 26 3adant1 
 |-  ( ( 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 
 |-  ( C = A -> ( C ` i ) = ( A ` i ) )
29 28 oveq2d 
 |-  ( C = A -> ( ( B ` i ) - ( C ` i ) ) = ( ( B ` i ) - ( A ` i ) ) )
30 28 oveq2d 
 |-  ( C = A -> ( ( C ` i ) - ( C ` i ) ) = ( ( C ` i ) - ( A ` i ) ) )
31 29 30 oveq12d 
 |-  ( C = A -> ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` i ) - ( C ` i ) ) ) = ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) )
32 31 breq1d 
 |-  ( C = A -> ( ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` i ) - ( C ` i ) ) ) <_ 0 <-> ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 ) )
33 32 ralbidv 
 |-  ( 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 ) )
34 27 33 syl5ibcom 
 |-  ( ( 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 
 |-  ( 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 ) )
36 34 35 syl6 
 |-  ( ( 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 ) ) )
37 36 a1dd 
 |-  ( ( 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 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> C e. ( EE ` N ) )
39 simp1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> A e. ( EE ` N ) )
40 eqeefv 
 |-  ( ( C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( C = A <-> A. p e. ( 1 ... N ) ( C ` p ) = ( A ` p ) ) )
41 38 39 40 syl2anc 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( C = A <-> A. p e. ( 1 ... N ) ( C ` p ) = ( A ` p ) ) )
42 41 necon3abid 
 |-  ( ( 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 
 |-  ( ( C ` p ) =/= ( A ` p ) <-> -. ( C ` p ) = ( A ` p ) )
44 43 rexbii 
 |-  ( E. p e. ( 1 ... N ) ( C ` p ) =/= ( A ` p ) <-> E. p e. ( 1 ... N ) -. ( C ` p ) = ( A ` p ) )
45 rexnal 
 |-  ( E. p e. ( 1 ... N ) -. ( C ` p ) = ( A ` p ) <-> -. A. p e. ( 1 ... N ) ( C ` p ) = ( A ` p ) )
46 44 45 bitr2i 
 |-  ( -. A. p e. ( 1 ... N ) ( C ` p ) = ( A ` p ) <-> E. p e. ( 1 ... N ) ( C ` p ) =/= ( A ` p ) )
47 42 46 bitrdi 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( j = p -> ( C ` j ) = ( C ` p ) )
50 fveq2 
 |-  ( j = p -> ( A ` j ) = ( A ` p ) )
51 49 50 oveq12d 
 |-  ( j = p -> ( ( C ` j ) - ( A ` j ) ) = ( ( C ` p ) - ( A ` p ) ) )
52 51 oveq2d 
 |-  ( j = p -> ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` p ) - ( A ` p ) ) ) )
53 fveq2 
 |-  ( j = p -> ( B ` j ) = ( B ` p ) )
54 53 50 oveq12d 
 |-  ( j = p -> ( ( B ` j ) - ( A ` j ) ) = ( ( B ` p ) - ( A ` p ) ) )
55 54 oveq1d 
 |-  ( j = p -> ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` i ) - ( A ` i ) ) ) )
56 52 55 eqeq12d 
 |-  ( 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 ) ) ) ) )
57 56 ralbidv 
 |-  ( 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 ) ) ) ) )
58 57 rspcv 
 |-  ( 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 ) ) ) ) )
59 58 ad2antrl 
 |-  ( ( ( 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 
 |-  ( ( A e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( A ` p ) e. RR )
61 60 3ad2antl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( A ` p ) e. RR )
62 fveere 
 |-  ( ( B e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( B ` p ) e. RR )
63 62 3ad2antl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( B ` p ) e. RR )
64 fveere 
 |-  ( ( C e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( C ` p ) e. RR )
65 64 3ad2antl3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( C ` p ) e. RR )
66 61 63 65 3jca 
 |-  ( ( ( 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 ) )
67 66 anim1i 
 |-  ( ( ( ( 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 ) ) )
68 67 anasss 
 |-  ( ( ( 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 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
70 69 3ad2antl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
71 14 3ad2antl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
72 15 3ad2antl3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
73 70 71 72 3jca 
 |-  ( ( ( 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 ) )
74 73 adantlr 
 |-  ( ( ( ( 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 
 |-  ( ( A ` p ) e. RR -> ( A ` p ) e. CC )
76 recn 
 |-  ( ( B ` p ) e. RR -> ( B ` p ) e. CC )
77 recn 
 |-  ( ( C ` p ) e. RR -> ( C ` p ) e. CC )
78 75 76 77 3anim123i 
 |-  ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) -> ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) )
79 78 adantr 
 |-  ( ( ( ( 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 ) )
80 79 ad2antlr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 )
87 85 86 subcld 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 )
89 88 86 subcld 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) ) -> ( A ` p ) e. CC )
92 90 91 subeq0ad 
 |-  ( ( ( ( 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 ) ) )
93 92 necon3bid 
 |-  ( ( ( ( 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 ) ) )
94 93 biimp3ar 
 |-  ( ( ( ( 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 )
95 87 89 94 divcld 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 )
97 96 84 subcld 
 |-  ( ( ( ( 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 )
98 95 97 mulcld 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 ) ) )
100 99 bicomd 
 |-  ( ( ( 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 ) ) ) ) )
101 83 84 98 100 syl3anc 
 |-  ( ( ( ( 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 ) ) ) ) )
102 87 97 89 94 div23d 
 |-  ( ( ( ( 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 ) ) ) )
103 102 eqeq2d 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 ) ) )
105 87 97 mulcld 
 |-  ( ( ( ( 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 )
106 83 84 subcld 
 |-  ( ( ( ( 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 )
107 105 89 106 94 divmuld 
 |-  ( ( ( ( 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 ) ) ) ) )
108 89 106 mulcomd 
 |-  ( ( ( ( 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 ) ) ) )
109 108 eqeq1d 
 |-  ( ( ( ( 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 ) ) ) ) )
110 107 109 bitrd 
 |-  ( ( ( ( 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 ) ) ) ) )
111 104 110 syl5bb 
 |-  ( ( ( ( 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 ) ) ) ) )
112 101 103 111 3bitr2d 
 |-  ( ( ( ( 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 ) ) ) ) )
113 82 112 syl5bb 
 |-  ( ( ( ( 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 ) ) ) ) )
114 74 80 81 113 syl3anc 
 |-  ( ( ( ( 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 ) ) ) ) )
115 114 ralbidva 
 |-  ( ( ( 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 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
117 simpl2 
 |-  ( ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) /\ ( C ` p ) =/= ( A ` p ) ) -> ( B ` p ) e. RR )
118 simpl1 
 |-  ( ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) /\ ( C ` p ) =/= ( A ` p ) ) -> ( A ` p ) e. RR )
119 117 118 resubcld 
 |-  ( ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) /\ ( C ` p ) =/= ( A ` p ) ) -> ( ( B ` p ) - ( A ` p ) ) e. RR )
120 simpl3 
 |-  ( ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) /\ ( C ` p ) =/= ( A ` p ) ) -> ( C ` p ) e. RR )
121 120 118 resubcld 
 |-  ( ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) /\ ( C ` p ) =/= ( A ` p ) ) -> ( ( C ` p ) - ( A ` p ) ) e. RR )
122 simp3 
 |-  ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) -> ( C ` p ) e. RR )
123 122 recnd 
 |-  ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) -> ( C ` p ) e. CC )
124 75 3ad2ant1 
 |-  ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) -> ( A ` p ) e. CC )
125 123 124 subeq0ad 
 |-  ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) -> ( ( ( C ` p ) - ( A ` p ) ) = 0 <-> ( C ` p ) = ( A ` p ) ) )
126 125 necon3bid 
 |-  ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) -> ( ( ( C ` p ) - ( A ` p ) ) =/= 0 <-> ( C ` p ) =/= ( A ` p ) ) )
127 126 biimpar 
 |-  ( ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR /\ ( C ` p ) e. RR ) /\ ( C ` p ) =/= ( A ` p ) ) -> ( ( C ` p ) - ( A ` p ) ) =/= 0 )
128 119 121 127 redivcld 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 ) ) )
131 130 oveq1d 
 |-  ( ( 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 ) ) ) )
132 131 breq1d 
 |-  ( ( 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 ) )
133 132 ralimi 
 |-  ( 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 
 |-  ( 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 ) )
135 133 134 syl 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( 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 ) ) ) )
138 136 137 oveq12d 
 |-  ( ( 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 ) ) ) ) )
139 138 breq1d 
 |-  ( ( 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 ) )
140 139 ralimi 
 |-  ( 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 
 |-  ( 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 ) )
142 140 141 syl 
 |-  ( 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 
 |-  ( ( 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 ) ) )
144 143 oveq2d 
 |-  ( ( 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 ) ) ) )
145 144 breq1d 
 |-  ( ( 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 ) )
146 145 ralimi 
 |-  ( 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 
 |-  ( 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 ) )
148 146 147 syl 
 |-  ( 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 ) )
149 135 142 148 3orbi123d 
 |-  ( 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 ) ) )
150 129 149 syl5ibrcom 
 |-  ( ( ( 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 ) ) )
151 116 128 150 syl2an 
 |-  ( ( ( 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 ) ) )
152 115 151 sylbird 
 |-  ( ( ( 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 ) ) ) = ( ( ( B ` p ) - ( A ` p ) ) 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 ) ) )
153 68 152 syldan 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( C ` p ) =/= ( A ` p ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` p ) - ( A ` p ) ) ) = ( ( ( B ` p ) - ( A ` p ) ) 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 ) ) )
154 59 153 syld 
 |-  ( ( ( 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 ` 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 ) ) )
155 48 154 syl5bi 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( C ` p ) =/= ( A ` p ) ) ) -> ( 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 ) ) )
156 155 rexlimdvaa 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( E. p e. ( 1 ... N ) ( C ` p ) =/= ( A ` p ) -> ( 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 ) ) ) )
157 47 156 sylbid 
 |-  ( ( 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 ) ) ) )
158 37 157 pm2.61dne 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( 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 ) ) )
159 158 pm4.71rd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( 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 ) /\ 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 ) ) ) ) ) )
160 andir 
 |-  ( ( ( 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. 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 ) 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 ) ) ) ) ) )
161 160 orbi1i 
 |-  ( ( ( ( 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. 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) )
162 df-3or 
 |-  ( ( 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 ` 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 ) )
163 162 anbi1i 
 |-  ( ( ( 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 ) 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 ) /\ 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 ) ) ) ) )
164 andir 
 |-  ( ( ( ( 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 ) 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. 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 ) ) ) ) ) )
165 163 164 bitri 
 |-  ( ( ( 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 ) 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. 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 ) ) ) ) ) )
166 df-3or 
 |-  ( ( ( 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 ) ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) )
167 161 165 166 3bitr4i 
 |-  ( ( ( 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 ) 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 ) 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 ) ) ) ) ) )
168 159 167 bitr2di 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( ( ( 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 ) ) ) ) ) <-> 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 ) ) ) ) )
169 13 168 bitrd 
 |-  ( ( 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 ) ) ) ) )