Metamath Proof Explorer

Theorem brbtwn2

Description: Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 brbtwn 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A Btwn <. B , C >. <-> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) )
2 fveere 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
3 2 3ad2antl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
4 fveere 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. RR )
5 4 3ad2antl3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. RR )
6 3 5 jca 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) e. RR /\ ( C ` i ) e. RR ) )
7 resubcl 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR ) -> ( ( B ` i ) - ( C ` i ) ) e. RR )
8 7 3adant3 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( B ` i ) - ( C ` i ) ) e. RR )
9 8 recnd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( B ` i ) - ( C ` i ) ) e. CC )
10 9 sqvald 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) = ( ( ( B ` i ) - ( C ` i ) ) x. ( ( B ` i ) - ( C ` i ) ) ) )
11 10 oveq2d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. -u ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) = ( ( t x. -u ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) x. ( ( B ` i ) - ( C ` i ) ) ) ) )
12 elicc01 
 |-  ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
13 12 simp1bi 
 |-  ( t e. ( 0 [,] 1 ) -> t e. RR )
14 13 recnd 
 |-  ( t e. ( 0 [,] 1 ) -> t e. CC )
15 14 3ad2ant3 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> t e. CC )
16 1re 
 |-  1 e. RR
17 resubcl 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 1 - t ) e. RR )
18 16 13 17 sylancr 
 |-  ( t e. ( 0 [,] 1 ) -> ( 1 - t ) e. RR )
19 18 3ad2ant3 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( 1 - t ) e. RR )
20 19 recnd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( 1 - t ) e. CC )
21 20 negcld 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> -u ( 1 - t ) e. CC )
22 15 9 21 9 mul4d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. ( ( B ` i ) - ( C ` i ) ) ) x. ( -u ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) ) = ( ( t x. -u ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) x. ( ( B ` i ) - ( C ` i ) ) ) ) )
23 recn 
 |-  ( ( B ` i ) e. RR -> ( B ` i ) e. CC )
24 23 3ad2ant1 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( B ` i ) e. CC )
25 recn 
 |-  ( ( C ` i ) e. RR -> ( C ` i ) e. CC )
26 25 3ad2ant2 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( C ` i ) e. CC )
27 15 24 26 subdid 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( t x. ( B ` i ) ) - ( t x. ( C ` i ) ) ) )
28 ax-1cn 
 |-  1 e. CC
29 subdir 
 |-  ( ( 1 e. CC /\ ( 1 - t ) e. CC /\ ( B ` i ) e. CC ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` i ) ) = ( ( 1 x. ( B ` i ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
30 28 20 24 29 mp3an2i 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` i ) ) = ( ( 1 x. ( B ` i ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
31 nncan 
 |-  ( ( 1 e. CC /\ t e. CC ) -> ( 1 - ( 1 - t ) ) = t )
32 28 15 31 sylancr 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( 1 - ( 1 - t ) ) = t )
33 32 oveq1d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` i ) ) = ( t x. ( B ` i ) ) )
34 24 mullidd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( 1 x. ( B ` i ) ) = ( B ` i ) )
35 34 oveq1d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 x. ( B ` i ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) = ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
36 30 33 35 3eqtr3d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( B ` i ) ) = ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
37 36 oveq1d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. ( B ` i ) ) - ( t x. ( C ` i ) ) ) = ( ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) - ( t x. ( C ` i ) ) ) )
38 simp1 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( B ` i ) e. RR )
39 19 38 remulcld 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - t ) x. ( B ` i ) ) e. RR )
40 39 recnd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - t ) x. ( B ` i ) ) e. CC )
41 13 3ad2ant3 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> t e. RR )
42 simp2 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( C ` i ) e. RR )
43 41 42 remulcld 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( C ` i ) ) e. RR )
44 43 recnd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( C ` i ) ) e. CC )
45 24 40 44 subsub4d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) - ( t x. ( C ` i ) ) ) = ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
46 27 37 45 3eqtrd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
47 20 9 mulneg1d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( -u ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) = -u ( ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) )
48 20 24 26 subdid 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) - ( ( 1 - t ) x. ( C ` i ) ) ) )
49 subdir 
 |-  ( ( 1 e. CC /\ t e. CC /\ ( C ` i ) e. CC ) -> ( ( 1 - t ) x. ( C ` i ) ) = ( ( 1 x. ( C ` i ) ) - ( t x. ( C ` i ) ) ) )
50 28 15 26 49 mp3an2i 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - t ) x. ( C ` i ) ) = ( ( 1 x. ( C ` i ) ) - ( t x. ( C ` i ) ) ) )
51 26 mullidd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( 1 x. ( C ` i ) ) = ( C ` i ) )
52 51 oveq1d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 x. ( C ` i ) ) - ( t x. ( C ` i ) ) ) = ( ( C ` i ) - ( t x. ( C ` i ) ) ) )
53 50 52 eqtrd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - t ) x. ( C ` i ) ) = ( ( C ` i ) - ( t x. ( C ` i ) ) ) )
54 53 oveq2d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( 1 - t ) x. ( B ` i ) ) - ( ( 1 - t ) x. ( C ` i ) ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) - ( ( C ` i ) - ( t x. ( C ` i ) ) ) ) )
55 40 26 44 subsub3d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( 1 - t ) x. ( B ` i ) ) - ( ( C ` i ) - ( t x. ( C ` i ) ) ) ) = ( ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) - ( C ` i ) ) )
56 48 54 55 3eqtrd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) - ( C ` i ) ) )
57 56 negeqd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> -u ( ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) = -u ( ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) - ( C ` i ) ) )
58 39 43 readdcld 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) e. RR )
59 58 recnd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) e. CC )
60 59 26 negsubdi2d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> -u ( ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) - ( C ` i ) ) = ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
61 47 57 60 3eqtrd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( -u ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
62 46 61 oveq12d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. ( ( B ` i ) - ( C ` i ) ) ) x. ( -u ( 1 - t ) x. ( ( B ` i ) - ( C ` i ) ) ) ) = ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
63 11 22 62 3eqtr2rd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) = ( ( t x. -u ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) )
64 15 20 mulneg2d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. -u ( 1 - t ) ) = -u ( t x. ( 1 - t ) ) )
65 64 oveq1d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. -u ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) = ( -u ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) )
66 41 19 remulcld 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( 1 - t ) ) e. RR )
67 66 recnd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( 1 - t ) ) e. CC )
68 8 resqcld 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) e. RR )
69 68 recnd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) e. CC )
70 67 69 mulneg1d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( -u ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) = -u ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) )
71 65 70 eqtrd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. -u ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) = -u ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) )
72 12 simp2bi 
 |-  ( t e. ( 0 [,] 1 ) -> 0 <_ t )
73 12 simp3bi 
 |-  ( t e. ( 0 [,] 1 ) -> t <_ 1 )
74 subge0 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 0 <_ ( 1 - t ) <-> t <_ 1 ) )
75 16 13 74 sylancr 
 |-  ( t e. ( 0 [,] 1 ) -> ( 0 <_ ( 1 - t ) <-> t <_ 1 ) )
76 73 75 mpbird 
 |-  ( t e. ( 0 [,] 1 ) -> 0 <_ ( 1 - t ) )
77 13 18 72 76 mulge0d 
 |-  ( t e. ( 0 [,] 1 ) -> 0 <_ ( t x. ( 1 - t ) ) )
78 77 3ad2ant3 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> 0 <_ ( t x. ( 1 - t ) ) )
79 8 sqge0d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> 0 <_ ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) )
80 66 68 78 79 mulge0d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> 0 <_ ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) )
81 66 68 remulcld 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) e. RR )
82 81 le0neg2d 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( 0 <_ ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) <-> -u ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) <_ 0 ) )
83 80 82 mpbid 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> -u ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) <_ 0 )
84 71 83 eqbrtrd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. -u ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) ^ 2 ) ) <_ 0 )
85 63 84 eqbrtrd 
 |-  ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 )
86 85 3expa 
 |-  ( ( ( ( B ` i ) e. RR /\ ( C ` i ) e. RR ) /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 )
87 6 86 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 )
88 87 an32s 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ t e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 )
89 88 ralrimiva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ t e. ( 0 [,] 1 ) ) -> A. i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 )
90 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
91 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
92 90 91 anim12i 
 |-  ( ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) /\ ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) ) -> ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) )
93 92 anandirs 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) )
94 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) e. CC )
95 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
96 94 95 anim12i 
 |-  ( ( ( B e. ( EE ` N ) /\ j e. ( 1 ... N ) ) /\ ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) ) -> ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) )
97 96 anandirs 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) )
98 93 97 anim12dan 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) )
99 98 3adantl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) )
100 subcl 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( B ` i ) - ( C ` i ) ) e. CC )
101 100 3ad2ant1 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( B ` i ) - ( C ` i ) ) e. CC )
102 subcl 
 |-  ( ( ( C ` j ) e. CC /\ ( B ` j ) e. CC ) -> ( ( C ` j ) - ( B ` j ) ) e. CC )
103 102 ancoms 
 |-  ( ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( C ` j ) - ( B ` j ) ) e. CC )
104 103 3ad2ant2 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( C ` j ) - ( B ` j ) ) e. CC )
105 101 104 mulcomd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( B ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) )
106 simp2r 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( C ` j ) e. CC )
107 simp2l 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( B ` j ) e. CC )
108 simp1l 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( B ` i ) e. CC )
109 simp1r 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( C ` i ) e. CC )
110 mulsub2 
 |-  ( ( ( ( C ` j ) e. CC /\ ( B ` j ) e. CC ) /\ ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) ) -> ( ( ( C ` j ) - ( B ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( ( B ` j ) - ( C ` j ) ) x. ( ( C ` i ) - ( B ` i ) ) ) )
111 106 107 108 109 110 syl22anc 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( C ` j ) - ( B ` j ) ) x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( ( B ` j ) - ( C ` j ) ) x. ( ( C ` i ) - ( B ` i ) ) ) )
112 105 111 eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` j ) - ( B ` j ) ) ) = ( ( ( B ` j ) - ( C ` j ) ) x. ( ( C ` i ) - ( B ` i ) ) ) )
113 112 oveq2d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` j ) - ( B ` j ) ) ) ) = ( ( t x. ( 1 - t ) ) x. ( ( ( B ` j ) - ( C ` j ) ) x. ( ( C ` i ) - ( B ` i ) ) ) ) )
114 simp3 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> t e. CC )
115 subcl 
 |-  ( ( 1 e. CC /\ t e. CC ) -> ( 1 - t ) e. CC )
116 28 115 mpan 
 |-  ( t e. CC -> ( 1 - t ) e. CC )
117 116 3ad2ant3 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( 1 - t ) e. CC )
118 114 117 101 104 mul4d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` j ) - ( B ` j ) ) ) ) = ( ( t x. ( ( B ` i ) - ( C ` i ) ) ) x. ( ( 1 - t ) x. ( ( C ` j ) - ( B ` j ) ) ) ) )
119 114 108 109 subdid 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( t x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( t x. ( B ` i ) ) - ( t x. ( C ` i ) ) ) )
120 28 117 108 29 mp3an2i 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` i ) ) = ( ( 1 x. ( B ` i ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
121 28 31 mpan 
 |-  ( t e. CC -> ( 1 - ( 1 - t ) ) = t )
122 121 3ad2ant3 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( 1 - ( 1 - t ) ) = t )
123 122 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` i ) ) = ( t x. ( B ` i ) ) )
124 108 mullidd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( 1 x. ( B ` i ) ) = ( B ` i ) )
125 124 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 x. ( B ` i ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) = ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
126 120 123 125 3eqtr3d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( t x. ( B ` i ) ) = ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
127 126 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( B ` i ) ) - ( t x. ( C ` i ) ) ) = ( ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) - ( t x. ( C ` i ) ) ) )
128 117 108 mulcld 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( B ` i ) ) e. CC )
129 114 109 mulcld 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( t x. ( C ` i ) ) e. CC )
130 108 128 129 subsub4d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( B ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) - ( t x. ( C ` i ) ) ) = ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
131 119 127 130 3eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( t x. ( ( B ` i ) - ( C ` i ) ) ) = ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
132 117 106 107 subdid 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( ( C ` j ) - ( B ` j ) ) ) = ( ( ( 1 - t ) x. ( C ` j ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) )
133 subdir 
 |-  ( ( 1 e. CC /\ t e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - t ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( t x. ( C ` j ) ) ) )
134 28 114 106 133 mp3an2i 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( t x. ( C ` j ) ) ) )
135 106 mullidd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( 1 x. ( C ` j ) ) = ( C ` j ) )
136 135 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 x. ( C ` j ) ) - ( t x. ( C ` j ) ) ) = ( ( C ` j ) - ( t x. ( C ` j ) ) ) )
137 134 136 eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( C ` j ) ) = ( ( C ` j ) - ( t x. ( C ` j ) ) ) )
138 137 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( 1 - t ) x. ( C ` j ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) = ( ( ( C ` j ) - ( t x. ( C ` j ) ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) )
139 132 138 eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( ( C ` j ) - ( B ` j ) ) ) = ( ( ( C ` j ) - ( t x. ( C ` j ) ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) )
140 114 106 mulcld 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( t x. ( C ` j ) ) e. CC )
141 117 107 mulcld 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( B ` j ) ) e. CC )
142 106 140 141 sub32d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( C ` j ) - ( t x. ( C ` j ) ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) = ( ( ( C ` j ) - ( ( 1 - t ) x. ( B ` j ) ) ) - ( t x. ( C ` j ) ) ) )
143 106 141 140 subsub4d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( C ` j ) - ( ( 1 - t ) x. ( B ` j ) ) ) - ( t x. ( C ` j ) ) ) = ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) )
144 139 142 143 3eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( ( C ` j ) - ( B ` j ) ) ) = ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) )
145 131 144 oveq12d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( ( B ` i ) - ( C ` i ) ) ) x. ( ( 1 - t ) x. ( ( C ` j ) - ( B ` j ) ) ) ) = ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) )
146 118 145 eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( 1 - t ) ) x. ( ( ( B ` i ) - ( C ` i ) ) x. ( ( C ` j ) - ( B ` j ) ) ) ) = ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) )
147 subcl 
 |-  ( ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( B ` j ) - ( C ` j ) ) e. CC )
148 147 3ad2ant2 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( B ` j ) - ( C ` j ) ) e. CC )
149 subcl 
 |-  ( ( ( C ` i ) e. CC /\ ( B ` i ) e. CC ) -> ( ( C ` i ) - ( B ` i ) ) e. CC )
150 149 ancoms 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( C ` i ) - ( B ` i ) ) e. CC )
151 150 3ad2ant1 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( C ` i ) - ( B ` i ) ) e. CC )
152 114 117 148 151 mul4d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( 1 - t ) ) x. ( ( ( B ` j ) - ( C ` j ) ) x. ( ( C ` i ) - ( B ` i ) ) ) ) = ( ( t x. ( ( B ` j ) - ( C ` j ) ) ) x. ( ( 1 - t ) x. ( ( C ` i ) - ( B ` i ) ) ) ) )
153 114 107 106 subdid 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( t x. ( ( B ` j ) - ( C ` j ) ) ) = ( ( t x. ( B ` j ) ) - ( t x. ( C ` j ) ) ) )
154 subdir 
 |-  ( ( 1 e. CC /\ ( 1 - t ) e. CC /\ ( B ` j ) e. CC ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` j ) ) = ( ( 1 x. ( B ` j ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) )
155 28 117 107 154 mp3an2i 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` j ) ) = ( ( 1 x. ( B ` j ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) )
156 122 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - ( 1 - t ) ) x. ( B ` j ) ) = ( t x. ( B ` j ) ) )
157 107 mullidd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( 1 x. ( B ` j ) ) = ( B ` j ) )
158 157 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 x. ( B ` j ) ) - ( ( 1 - t ) x. ( B ` j ) ) ) = ( ( B ` j ) - ( ( 1 - t ) x. ( B ` j ) ) ) )
159 155 156 158 3eqtr3rd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( B ` j ) - ( ( 1 - t ) x. ( B ` j ) ) ) = ( t x. ( B ` j ) ) )
160 159 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( B ` j ) - ( ( 1 - t ) x. ( B ` j ) ) ) - ( t x. ( C ` j ) ) ) = ( ( t x. ( B ` j ) ) - ( t x. ( C ` j ) ) ) )
161 107 141 140 subsub4d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( B ` j ) - ( ( 1 - t ) x. ( B ` j ) ) ) - ( t x. ( C ` j ) ) ) = ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) )
162 153 160 161 3eqtr2d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( t x. ( ( B ` j ) - ( C ` j ) ) ) = ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) )
163 117 109 108 subdid 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( ( C ` i ) - ( B ` i ) ) ) = ( ( ( 1 - t ) x. ( C ` i ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
164 28 114 109 49 mp3an2i 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( C ` i ) ) = ( ( 1 x. ( C ` i ) ) - ( t x. ( C ` i ) ) ) )
165 109 mullidd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( 1 x. ( C ` i ) ) = ( C ` i ) )
166 165 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 x. ( C ` i ) ) - ( t x. ( C ` i ) ) ) = ( ( C ` i ) - ( t x. ( C ` i ) ) ) )
167 164 166 eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( C ` i ) ) = ( ( C ` i ) - ( t x. ( C ` i ) ) ) )
168 167 oveq1d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( 1 - t ) x. ( C ` i ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) = ( ( ( C ` i ) - ( t x. ( C ` i ) ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) )
169 109 129 128 sub32d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( C ` i ) - ( t x. ( C ` i ) ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) = ( ( ( C ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) - ( t x. ( C ` i ) ) ) )
170 109 128 129 subsub4d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( C ` i ) - ( ( 1 - t ) x. ( B ` i ) ) ) - ( t x. ( C ` i ) ) ) = ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
171 169 170 eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( C ` i ) - ( t x. ( C ` i ) ) ) - ( ( 1 - t ) x. ( B ` i ) ) ) = ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
172 163 168 171 3eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( 1 - t ) x. ( ( C ` i ) - ( B ` i ) ) ) = ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
173 162 172 oveq12d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( ( B ` j ) - ( C ` j ) ) ) x. ( ( 1 - t ) x. ( ( C ` i ) - ( B ` i ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
174 152 173 eqtrd 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( t x. ( 1 - t ) ) x. ( ( ( B ` j ) - ( C ` j ) ) x. ( ( C ` i ) - ( B ` i ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
175 113 146 174 3eqtr3d 
 |-  ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) /\ t e. CC ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
176 175 3expa 
 |-  ( ( ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC ) /\ ( ( B ` j ) e. CC /\ ( C ` j ) e. CC ) ) /\ t e. CC ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
177 99 14 176 syl2an 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
178 177 an32s 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ t e. ( 0 [,] 1 ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
179 178 ralrimivva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ t e. ( 0 [,] 1 ) ) -> A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
180 fveq2 
 |-  ( k = i -> ( A ` k ) = ( A ` i ) )
181 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
182 181 oveq2d 
 |-  ( k = i -> ( ( 1 - t ) x. ( B ` k ) ) = ( ( 1 - t ) x. ( B ` i ) ) )
183 fveq2 
 |-  ( k = i -> ( C ` k ) = ( C ` i ) )
184 183 oveq2d 
 |-  ( k = i -> ( t x. ( C ` k ) ) = ( t x. ( C ` i ) ) )
185 182 184 oveq12d 
 |-  ( k = i -> ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) )
186 180 185 eqeq12d 
 |-  ( k = i -> ( ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) <-> ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
187 186 rspccva 
 |-  ( ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) )
188 oveq2 
 |-  ( ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) -> ( ( B ` i ) - ( A ` i ) ) = ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
189 oveq2 
 |-  ( ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) -> ( ( C ` i ) - ( A ` i ) ) = ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
190 188 189 oveq12d 
 |-  ( ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) -> ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
191 190 breq1d 
 |-  ( ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 <-> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 ) )
192 187 191 syl 
 |-  ( ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 <-> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 ) )
193 192 ralbidva 
 |-  ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 <-> A. i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 ) )
194 fveq2 
 |-  ( k = j -> ( A ` k ) = ( A ` j ) )
195 fveq2 
 |-  ( k = j -> ( B ` k ) = ( B ` j ) )
196 195 oveq2d 
 |-  ( k = j -> ( ( 1 - t ) x. ( B ` k ) ) = ( ( 1 - t ) x. ( B ` j ) ) )
197 fveq2 
 |-  ( k = j -> ( C ` k ) = ( C ` j ) )
198 197 oveq2d 
 |-  ( k = j -> ( t x. ( C ` k ) ) = ( t x. ( C ` j ) ) )
199 196 198 oveq12d 
 |-  ( k = j -> ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) )
200 194 199 eqeq12d 
 |-  ( k = j -> ( ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) <-> ( A ` j ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) )
201 200 rspccva 
 |-  ( ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) )
202 oveq2 
 |-  ( ( A ` j ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) -> ( ( C ` j ) - ( A ` j ) ) = ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) )
203 188 202 oveqan12d 
 |-  ( ( ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( A ` j ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) -> ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) )
204 oveq2 
 |-  ( ( A ` j ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) -> ( ( B ` j ) - ( A ` j ) ) = ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) )
205 204 189 oveqan12rd 
 |-  ( ( ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( A ` j ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) -> ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
206 203 205 eqeq12d 
 |-  ( ( ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( A ` j ) = ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) ) )
207 187 201 206 syl2an 
 |-  ( ( ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) /\ i e. ( 1 ... N ) ) /\ ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) /\ j e. ( 1 ... N ) ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) ) )
208 207 anandis 
 |-  ( ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) ) )
209 208 2ralbidva 
 |-  ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) -> ( 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 ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) ) )
210 193 209 anbi12d 
 |-  ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) -> ( ( 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 ) ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 /\ A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) ) ) )
211 210 biimprcd 
 |-  ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) <_ 0 /\ A. i e. ( 1 ... N ) A. j e. ( 1 ... N ) ( ( ( B ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) x. ( ( C ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) ) = ( ( ( B ` j ) - ( ( ( 1 - t ) x. ( B ` j ) ) + ( t x. ( C ` j ) ) ) ) x. ( ( C ` i ) - ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) ) -> ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) -> ( 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 ) ) ) ) ) )
212 89 179 211 syl2anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ t e. ( 0 [,] 1 ) ) -> ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) -> ( 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 ) ) ) ) ) )
213 212 rexlimdva 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) -> ( 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 ) ) ) ) ) )
214 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
215 214 3ad2antl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
216 mulsuble0b 
 |-  ( ( ( B ` i ) e. RR /\ ( A ` i ) e. RR /\ ( C ` i ) e. RR ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 <-> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
217 3 215 5 216 syl3anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 <-> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
218 217 ralbidva 
 |-  ( ( 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 ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
219 218 anbi1d 
 |-  ( ( 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 ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) ) )
220 simpl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) -> B e. ( EE ` N ) )
221 simpl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) -> A e. ( EE ` N ) )
222 eqeefv 
 |-  ( ( B e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( B = A <-> A. i e. ( 1 ... N ) ( B ` i ) = ( A ` i ) ) )
223 220 221 222 syl2anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) -> ( B = A <-> A. i e. ( 1 ... N ) ( B ` i ) = ( A ` i ) ) )
224 3 adantlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
225 215 adantlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
226 224 225 letri3d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) = ( A ` i ) <-> ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) )
227 pm4.25 
 |-  ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) <-> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) \/ ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) )
228 fveq1 
 |-  ( B = C -> ( B ` i ) = ( C ` i ) )
229 228 breq2d 
 |-  ( B = C -> ( ( A ` i ) <_ ( B ` i ) <-> ( A ` i ) <_ ( C ` i ) ) )
230 229 anbi2d 
 |-  ( B = C -> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) <-> ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) ) )
231 228 breq1d 
 |-  ( B = C -> ( ( B ` i ) <_ ( A ` i ) <-> ( C ` i ) <_ ( A ` i ) ) )
232 231 anbi1d 
 |-  ( B = C -> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) <-> ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) )
233 230 232 orbi12d 
 |-  ( B = C -> ( ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) \/ ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) <-> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
234 233 ad2antlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) \/ ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) <-> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
235 227 234 bitrid 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) <-> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
236 226 235 bitrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) = ( A ` i ) <-> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
237 236 ralbidva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( A ` i ) <-> A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
238 223 237 bitrd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) -> ( B = A <-> A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) ) )
239 238 biimprd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) -> ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) -> B = A ) )
240 239 adantrd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ B = C ) -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> B = A ) )
241 240 ex 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B = C -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> B = A ) ) )
242 0elunit 
 |-  0 e. ( 0 [,] 1 )
243 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. CC )
244 243 3ad2antl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. CC )
245 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. CC )
246 245 3ad2antl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. CC )
247 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. CC )
248 247 3ad2antl3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. CC )
249 244 246 248 3jca 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) )
250 mullid 
 |-  ( ( B ` k ) e. CC -> ( 1 x. ( B ` k ) ) = ( B ` k ) )
251 mul02 
 |-  ( ( C ` k ) e. CC -> ( 0 x. ( C ` k ) ) = 0 )
252 250 251 oveqan12d 
 |-  ( ( ( B ` k ) e. CC /\ ( C ` k ) e. CC ) -> ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) = ( ( B ` k ) + 0 ) )
253 addrid 
 |-  ( ( B ` k ) e. CC -> ( ( B ` k ) + 0 ) = ( B ` k ) )
254 253 adantr 
 |-  ( ( ( B ` k ) e. CC /\ ( C ` k ) e. CC ) -> ( ( B ` k ) + 0 ) = ( B ` k ) )
255 252 254 eqtrd 
 |-  ( ( ( B ` k ) e. CC /\ ( C ` k ) e. CC ) -> ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) = ( B ` k ) )
256 255 3adant1 
 |-  ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) -> ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) = ( B ` k ) )
257 256 adantr 
 |-  ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( B = C /\ B = A ) ) -> ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) = ( B ` k ) )
258 fveq1 
 |-  ( B = A -> ( B ` k ) = ( A ` k ) )
259 258 ad2antll 
 |-  ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( B = C /\ B = A ) ) -> ( B ` k ) = ( A ` k ) )
260 257 259 eqtr2d 
 |-  ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( B = C /\ B = A ) ) -> ( A ` k ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) )
261 249 260 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) /\ ( B = C /\ B = A ) ) -> ( A ` k ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) )
262 261 an32s 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B = C /\ B = A ) ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) )
263 262 ralrimiva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B = C /\ B = A ) ) -> A. k e. ( 1 ... N ) ( A ` k ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) )
264 oveq2 
 |-  ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
265 1m0e1 
 |-  ( 1 - 0 ) = 1
266 264 265 eqtrdi 
 |-  ( t = 0 -> ( 1 - t ) = 1 )
267 266 oveq1d 
 |-  ( t = 0 -> ( ( 1 - t ) x. ( B ` k ) ) = ( 1 x. ( B ` k ) ) )
268 oveq1 
 |-  ( t = 0 -> ( t x. ( C ` k ) ) = ( 0 x. ( C ` k ) ) )
269 267 268 oveq12d 
 |-  ( t = 0 -> ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) )
270 269 eqeq2d 
 |-  ( t = 0 -> ( ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) <-> ( A ` k ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) ) )
271 270 ralbidv 
 |-  ( t = 0 -> ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) <-> A. k e. ( 1 ... N ) ( A ` k ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) ) )
272 271 rspcev 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ A. k e. ( 1 ... N ) ( A ` k ) = ( ( 1 x. ( B ` k ) ) + ( 0 x. ( C ` k ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) )
273 242 263 272 sylancr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B = C /\ B = A ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) )
274 273 exp32 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B = C -> ( B = A -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) ) )
275 241 274 syldd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B = C -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) ) )
276 eqeefv 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B = C <-> A. p e. ( 1 ... N ) ( B ` p ) = ( C ` p ) ) )
277 276 3adant1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B = C <-> A. p e. ( 1 ... N ) ( B ` p ) = ( C ` p ) ) )
278 277 necon3abid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B =/= C <-> -. A. p e. ( 1 ... N ) ( B ` p ) = ( C ` p ) ) )
279 df-ne 
 |-  ( ( B ` p ) =/= ( C ` p ) <-> -. ( B ` p ) = ( C ` p ) )
280 279 rexbii 
 |-  ( E. p e. ( 1 ... N ) ( B ` p ) =/= ( C ` p ) <-> E. p e. ( 1 ... N ) -. ( B ` p ) = ( C ` p ) )
281 rexnal 
 |-  ( E. p e. ( 1 ... N ) -. ( B ` p ) = ( C ` p ) <-> -. A. p e. ( 1 ... N ) ( B ` p ) = ( C ` p ) )
282 280 281 bitri 
 |-  ( E. p e. ( 1 ... N ) ( B ` p ) =/= ( C ` p ) <-> -. A. p e. ( 1 ... N ) ( B ` p ) = ( C ` p ) )
283 278 282 bitr4di 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B =/= C <-> E. p e. ( 1 ... N ) ( B ` p ) =/= ( C ` p ) ) )
284 fveq2 
 |-  ( i = p -> ( B ` i ) = ( B ` p ) )
285 fveq2 
 |-  ( i = p -> ( A ` i ) = ( A ` p ) )
286 284 285 breq12d 
 |-  ( i = p -> ( ( B ` i ) <_ ( A ` i ) <-> ( B ` p ) <_ ( A ` p ) ) )
287 fveq2 
 |-  ( i = p -> ( C ` i ) = ( C ` p ) )
288 285 287 breq12d 
 |-  ( i = p -> ( ( A ` i ) <_ ( C ` i ) <-> ( A ` p ) <_ ( C ` p ) ) )
289 286 288 anbi12d 
 |-  ( i = p -> ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) <-> ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) )
290 287 285 breq12d 
 |-  ( i = p -> ( ( C ` i ) <_ ( A ` i ) <-> ( C ` p ) <_ ( A ` p ) ) )
291 285 284 breq12d 
 |-  ( i = p -> ( ( A ` i ) <_ ( B ` i ) <-> ( A ` p ) <_ ( B ` p ) ) )
292 290 291 anbi12d 
 |-  ( i = p -> ( ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) <-> ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) )
293 289 292 orbi12d 
 |-  ( i = p -> ( ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) <-> ( ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) \/ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) ) )
294 293 rspcv 
 |-  ( p e. ( 1 ... N ) -> ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) -> ( ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) \/ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) ) )
295 294 ad2antrl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) -> ( ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) \/ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) ) )
296 simprr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( A ` p ) <_ ( C ` p ) )
297 simp1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> A e. ( EE ` N ) )
298 simpl 
 |-  ( ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) -> p e. ( 1 ... N ) )
299 fveere 
 |-  ( ( A e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( A ` p ) e. RR )
300 297 298 299 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( A ` p ) e. RR )
301 simp3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> C e. ( EE ` N ) )
302 fveere 
 |-  ( ( C e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( C ` p ) e. RR )
303 301 298 302 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( C ` p ) e. RR )
304 simpl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> B e. ( EE ` N ) )
305 simprl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> p e. ( 1 ... N ) )
306 fveere 
 |-  ( ( B e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( B ` p ) e. RR )
307 304 305 306 syl2anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( B ` p ) e. RR )
308 300 303 307 lesub1d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( A ` p ) <_ ( C ` p ) <-> ( ( A ` p ) - ( B ` p ) ) <_ ( ( C ` p ) - ( B ` p ) ) ) )
309 308 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( A ` p ) <_ ( C ` p ) <-> ( ( A ` p ) - ( B ` p ) ) <_ ( ( C ` p ) - ( B ` p ) ) ) )
310 296 309 mpbid 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( A ` p ) - ( B ` p ) ) <_ ( ( C ` p ) - ( B ` p ) ) )
311 300 307 resubcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( A ` p ) - ( B ` p ) ) e. RR )
312 311 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( A ` p ) - ( B ` p ) ) e. RR )
313 simprl 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( B ` p ) <_ ( A ` p ) )
314 300 307 subge0d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( 0 <_ ( ( A ` p ) - ( B ` p ) ) <-> ( B ` p ) <_ ( A ` p ) ) )
315 314 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( 0 <_ ( ( A ` p ) - ( B ` p ) ) <-> ( B ` p ) <_ ( A ` p ) ) )
316 313 315 mpbird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> 0 <_ ( ( A ` p ) - ( B ` p ) ) )
317 303 307 resubcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( C ` p ) - ( B ` p ) ) e. RR )
318 317 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( C ` p ) - ( B ` p ) ) e. RR )
319 letr 
 |-  ( ( ( B ` p ) e. RR /\ ( A ` p ) e. RR /\ ( C ` p ) e. RR ) -> ( ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) -> ( B ` p ) <_ ( C ` p ) ) )
320 307 300 303 319 syl3anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) -> ( B ` p ) <_ ( C ` p ) ) )
321 320 imp 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( B ` p ) <_ ( C ` p ) )
322 simplrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( B ` p ) =/= ( C ` p ) )
323 322 necomd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( C ` p ) =/= ( B ` p ) )
324 307 303 ltlend 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( B ` p ) < ( C ` p ) <-> ( ( B ` p ) <_ ( C ` p ) /\ ( C ` p ) =/= ( B ` p ) ) ) )
325 324 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( B ` p ) < ( C ` p ) <-> ( ( B ` p ) <_ ( C ` p ) /\ ( C ` p ) =/= ( B ` p ) ) ) )
326 321 323 325 mpbir2and 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( B ` p ) < ( C ` p ) )
327 307 303 posdifd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( B ` p ) < ( C ` p ) <-> 0 < ( ( C ` p ) - ( B ` p ) ) ) )
328 327 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( B ` p ) < ( C ` p ) <-> 0 < ( ( C ` p ) - ( B ` p ) ) ) )
329 326 328 mpbid 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> 0 < ( ( C ` p ) - ( B ` p ) ) )
330 divelunit 
 |-  ( ( ( ( ( A ` p ) - ( B ` p ) ) e. RR /\ 0 <_ ( ( A ` p ) - ( B ` p ) ) ) /\ ( ( ( C ` p ) - ( B ` p ) ) e. RR /\ 0 < ( ( C ` p ) - ( B ` p ) ) ) ) -> ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) <-> ( ( A ` p ) - ( B ` p ) ) <_ ( ( C ` p ) - ( B ` p ) ) ) )
331 312 316 318 329 330 syl22anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) <-> ( ( A ` p ) - ( B ` p ) ) <_ ( ( C ` p ) - ( B ` p ) ) ) )
332 310 331 mpbird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) )
333 300 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( A ` p ) e. CC )
334 307 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( B ` p ) e. CC )
335 303 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( C ` p ) e. CC )
336 simprr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( B ` p ) =/= ( C ` p ) )
337 336 necomd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( C ` p ) =/= ( B ` p ) )
338 333 334 335 334 337 div2subd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( ( B ` p ) - ( A ` p ) ) / ( ( B ` p ) - ( C ` p ) ) ) )
339 338 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( ( B ` p ) - ( A ` p ) ) / ( ( B ` p ) - ( C ` p ) ) ) )
340 simprl 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( C ` p ) <_ ( A ` p ) )
341 303 300 307 lesub2d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( C ` p ) <_ ( A ` p ) <-> ( ( B ` p ) - ( A ` p ) ) <_ ( ( B ` p ) - ( C ` p ) ) ) )
342 341 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( C ` p ) <_ ( A ` p ) <-> ( ( B ` p ) - ( A ` p ) ) <_ ( ( B ` p ) - ( C ` p ) ) ) )
343 340 342 mpbid 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( B ` p ) - ( A ` p ) ) <_ ( ( B ` p ) - ( C ` p ) ) )
344 307 300 resubcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( B ` p ) - ( A ` p ) ) e. RR )
345 344 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( B ` p ) - ( A ` p ) ) e. RR )
346 simprr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( A ` p ) <_ ( B ` p ) )
347 307 300 subge0d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( 0 <_ ( ( B ` p ) - ( A ` p ) ) <-> ( A ` p ) <_ ( B ` p ) ) )
348 347 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( 0 <_ ( ( B ` p ) - ( A ` p ) ) <-> ( A ` p ) <_ ( B ` p ) ) )
349 346 348 mpbird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> 0 <_ ( ( B ` p ) - ( A ` p ) ) )
350 307 303 resubcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( B ` p ) - ( C ` p ) ) e. RR )
351 350 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( B ` p ) - ( C ` p ) ) e. RR )
352 letr 
 |-  ( ( ( C ` p ) e. RR /\ ( A ` p ) e. RR /\ ( B ` p ) e. RR ) -> ( ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) -> ( C ` p ) <_ ( B ` p ) ) )
353 303 300 307 352 syl3anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) -> ( C ` p ) <_ ( B ` p ) ) )
354 353 imp 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( C ` p ) <_ ( B ` p ) )
355 simplrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( B ` p ) =/= ( C ` p ) )
356 303 307 ltlend 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( C ` p ) < ( B ` p ) <-> ( ( C ` p ) <_ ( B ` p ) /\ ( B ` p ) =/= ( C ` p ) ) ) )
357 356 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( C ` p ) < ( B ` p ) <-> ( ( C ` p ) <_ ( B ` p ) /\ ( B ` p ) =/= ( C ` p ) ) ) )
358 354 355 357 mpbir2and 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( C ` p ) < ( B ` p ) )
359 303 307 posdifd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( C ` p ) < ( B ` p ) <-> 0 < ( ( B ` p ) - ( C ` p ) ) ) )
360 359 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( C ` p ) < ( B ` p ) <-> 0 < ( ( B ` p ) - ( C ` p ) ) ) )
361 358 360 mpbid 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> 0 < ( ( B ` p ) - ( C ` p ) ) )
362 divelunit 
 |-  ( ( ( ( ( B ` p ) - ( A ` p ) ) e. RR /\ 0 <_ ( ( B ` p ) - ( A ` p ) ) ) /\ ( ( ( B ` p ) - ( C ` p ) ) e. RR /\ 0 < ( ( B ` p ) - ( C ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) / ( ( B ` p ) - ( C ` p ) ) ) e. ( 0 [,] 1 ) <-> ( ( B ` p ) - ( A ` p ) ) <_ ( ( B ` p ) - ( C ` p ) ) ) )
363 345 349 351 361 362 syl22anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) / ( ( B ` p ) - ( C ` p ) ) ) e. ( 0 [,] 1 ) <-> ( ( B ` p ) - ( A ` p ) ) <_ ( ( B ` p ) - ( C ` p ) ) ) )
364 343 363 mpbird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) / ( ( B ` p ) - ( C ` p ) ) ) e. ( 0 [,] 1 ) )
365 339 364 eqeltrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) )
366 332 365 jaodan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) /\ ( ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) \/ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) )
367 366 ex 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( ( ( B ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( C ` p ) ) \/ ( ( C ` p ) <_ ( A ` p ) /\ ( A ` p ) <_ ( B ` p ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) ) )
368 295 367 syld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( B ` i ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) ) )
369 simp2l 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> p e. ( 1 ... N ) )
370 simp3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> k e. ( 1 ... N ) )
371 284 285 oveq12d 
 |-  ( i = p -> ( ( B ` i ) - ( A ` i ) ) = ( ( B ` p ) - ( A ` p ) ) )
372 371 oveq1d 
 |-  ( i = p -> ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` j ) - ( A ` j ) ) ) )
373 287 285 oveq12d 
 |-  ( i = p -> ( ( C ` i ) - ( A ` i ) ) = ( ( C ` p ) - ( A ` p ) ) )
374 373 oveq2d 
 |-  ( i = p -> ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` p ) - ( A ` p ) ) ) )
375 372 374 eqeq12d 
 |-  ( i = p -> ( ( ( ( B ` i ) - ( A ` i ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <-> ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) )
376 fveq2 
 |-  ( j = k -> ( C ` j ) = ( C ` k ) )
377 fveq2 
 |-  ( j = k -> ( A ` j ) = ( A ` k ) )
378 376 377 oveq12d 
 |-  ( j = k -> ( ( C ` j ) - ( A ` j ) ) = ( ( C ` k ) - ( A ` k ) ) )
379 378 oveq2d 
 |-  ( j = k -> ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) )
380 fveq2 
 |-  ( j = k -> ( B ` j ) = ( B ` k ) )
381 380 377 oveq12d 
 |-  ( j = k -> ( ( B ` j ) - ( A ` j ) ) = ( ( B ` k ) - ( A ` k ) ) )
382 381 oveq1d 
 |-  ( j = k -> ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` p ) - ( A ` p ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) )
383 379 382 eqeq12d 
 |-  ( j = k -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` j ) - ( A ` j ) ) ) = ( ( ( B ` j ) - ( A ` j ) ) x. ( ( C ` p ) - ( A ` p ) ) ) <-> ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) )
384 375 383 rspc2v 
 |-  ( ( p e. ( 1 ... N ) /\ k e. ( 1 ... 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 ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) )
385 369 370 384 syl2anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... 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 ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) )
386 simp11 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> A e. ( EE ` N ) )
387 386 370 243 syl2anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. CC )
388 simp12 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> B e. ( EE ` N ) )
389 388 370 245 syl2anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. CC )
390 simp13 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> C e. ( EE ` N ) )
391 390 370 247 syl2anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. CC )
392 333 3adant3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( A ` p ) e. CC )
393 334 3adant3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( B ` p ) e. CC )
394 335 3adant3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( C ` p ) e. CC )
395 simp2r 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( B ` p ) =/= ( C ` p ) )
396 395 necomd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( C ` p ) =/= ( B ` p ) )
397 simpl23 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( C ` p ) e. CC )
398 simpl21 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( A ` p ) e. CC )
399 397 398 subcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( C ` p ) - ( A ` p ) ) e. CC )
400 simpl12 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( B ` k ) e. CC )
401 399 400 mulcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) e. CC )
402 simpl22 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( B ` p ) e. CC )
403 398 402 subcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( A ` p ) - ( B ` p ) ) e. CC )
404 simpl13 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( C ` k ) e. CC )
405 403 404 mulcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) e. CC )
406 397 402 subcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( C ` p ) - ( B ` p ) ) e. CC )
407 simpl3 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( C ` p ) =/= ( B ` p ) )
408 397 402 407 subne0d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( C ` p ) - ( B ` p ) ) =/= 0 )
409 401 405 406 408 divdird 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) / ( ( C ` p ) - ( B ` p ) ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) )
410 npncan2 
 |-  ( ( ( B ` p ) e. CC /\ ( A ` p ) e. CC ) -> ( ( ( B ` p ) - ( A ` p ) ) + ( ( A ` p ) - ( B ` p ) ) ) = 0 )
411 402 398 410 syl2anc 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) + ( ( A ` p ) - ( B ` p ) ) ) = 0 )
412 411 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) + ( ( A ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) = ( 0 x. ( C ` k ) ) )
413 402 398 subcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( B ` p ) - ( A ` p ) ) e. CC )
414 413 403 404 adddird 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) + ( ( A ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) = ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
415 404 mul02d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( 0 x. ( C ` k ) ) = 0 )
416 412 414 415 3eqtr3d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) = 0 )
417 416 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) = ( 0 + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) )
418 413 404 mulcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) e. CC )
419 simpl11 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( A ` k ) e. CC )
420 406 419 mulcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) e. CC )
421 418 405 420 add32d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
422 420 addlidd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( 0 + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) = ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) )
423 417 421 422 3eqtr3rd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) = ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
424 399 419 mulcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) e. CC )
425 413 419 mulcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) e. CC )
426 418 424 425 addsubd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
427 397 402 398 nnncan2d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( A ` p ) ) - ( ( B ` p ) - ( A ` p ) ) ) = ( ( C ` p ) - ( B ` p ) ) )
428 427 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( A ` p ) ) - ( ( B ` p ) - ( A ` p ) ) ) x. ( A ` k ) ) = ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) )
429 399 413 419 subdird 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( A ` p ) ) - ( ( B ` p ) - ( A ` p ) ) ) x. ( A ` k ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
430 428 429 eqtr3d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
431 430 oveq2d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) ) )
432 418 424 425 addsubassd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) ) )
433 431 432 eqtr4d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
434 413 404 419 subdid 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
435 434 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) - ( ( ( B ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
436 426 433 435 3eqtr4d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
437 436 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( C ` k ) ) + ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) = ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
438 423 437 eqtrd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) = ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
439 simpr 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) )
440 439 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
441 440 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) = ( ( ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
442 400 419 subcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( B ` k ) - ( A ` k ) ) e. CC )
443 442 399 mulcomd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) = ( ( ( C ` p ) - ( A ` p ) ) x. ( ( B ` k ) - ( A ` k ) ) ) )
444 443 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) x. ( ( B ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
445 399 442 419 adddid 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( A ` p ) ) x. ( ( ( B ` k ) - ( A ` k ) ) + ( A ` k ) ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) x. ( ( B ` k ) - ( A ` k ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) )
446 400 419 npcand 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( B ` k ) - ( A ` k ) ) + ( A ` k ) ) = ( B ` k ) )
447 446 oveq2d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( A ` p ) ) x. ( ( ( B ` k ) - ( A ` k ) ) + ( A ` k ) ) ) = ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) )
448 444 445 447 3eqtr2d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) = ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) )
449 448 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) + ( ( ( C ` p ) - ( A ` p ) ) x. ( A ` k ) ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
450 438 441 449 3eqtrd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) )
451 401 405 addcld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) e. CC )
452 451 406 419 408 divmuld 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( A ` k ) <-> ( ( ( C ` p ) - ( B ` p ) ) x. ( A ` k ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) ) )
453 450 452 mpbird 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) + ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( A ` k ) )
454 399 400 406 408 div23d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( ( ( C ` p ) - ( A ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( B ` k ) ) )
455 406 403 406 408 divsubdird 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( B ` p ) ) - ( ( A ` p ) - ( B ` p ) ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( ( ( C ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) )
456 397 398 402 nnncan2d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( B ` p ) ) - ( ( A ` p ) - ( B ` p ) ) ) = ( ( C ` p ) - ( A ` p ) ) )
457 456 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( B ` p ) ) - ( ( A ` p ) - ( B ` p ) ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( ( C ` p ) - ( A ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) )
458 406 408 dividd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) = 1 )
459 458 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) = ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) )
460 455 457 459 3eqtr3d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( C ` p ) - ( A ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) )
461 460 oveq1d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( A ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( B ` k ) ) = ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) )
462 454 461 eqtrd 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) )
463 403 404 406 408 div23d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) / ( ( C ` p ) - ( B ` p ) ) ) = ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) )
464 462 463 oveq12d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( ( ( ( ( C ` p ) - ( A ` p ) ) x. ( B ` k ) ) / ( ( C ` p ) - ( B ` p ) ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) x. ( C ` k ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) )
465 409 453 464 3eqtr3d 
 |-  ( ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) /\ ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) ) -> ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) )
466 465 ex 
 |-  ( ( ( ( A ` k ) e. CC /\ ( B ` k ) e. CC /\ ( C ` k ) e. CC ) /\ ( ( A ` p ) e. CC /\ ( B ` p ) e. CC /\ ( C ` p ) e. CC ) /\ ( C ` p ) =/= ( B ` p ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) -> ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) )
467 387 389 391 392 393 394 396 466 syl331anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( ( B ` p ) - ( A ` p ) ) x. ( ( C ` k ) - ( A ` k ) ) ) = ( ( ( B ` k ) - ( A ` k ) ) x. ( ( C ` p ) - ( A ` p ) ) ) -> ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) )
468 385 467 syld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) /\ k e. ( 1 ... 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 ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) )
469 468 3expia 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( k e. ( 1 ... 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 ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) ) )
470 469 com23 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` 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 ) ) ) -> ( k e. ( 1 ... N ) -> ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) ) )
471 470 ralrimdv 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` 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. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) )
472 368 471 anim12d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) /\ A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) ) )
473 oveq2 
 |-  ( t = ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) -> ( 1 - t ) = ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) )
474 473 oveq1d 
 |-  ( t = ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) -> ( ( 1 - t ) x. ( B ` k ) ) = ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) )
475 oveq1 
 |-  ( t = ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) -> ( t x. ( C ` k ) ) = ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) )
476 474 475 oveq12d 
 |-  ( t = ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) -> ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) )
477 476 eqeq2d 
 |-  ( t = ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) -> ( ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) <-> ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) )
478 477 ralbidv 
 |-  ( t = ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) -> ( A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) <-> A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) )
479 478 rspcev 
 |-  ( ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) e. ( 0 [,] 1 ) /\ A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) ) x. ( B ` k ) ) + ( ( ( ( A ` p ) - ( B ` p ) ) / ( ( C ` p ) - ( B ` p ) ) ) x. ( C ` k ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) )
480 472 479 syl6 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( p e. ( 1 ... N ) /\ ( B ` p ) =/= ( C ` p ) ) ) -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) )
481 480 rexlimdvaa 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( E. p e. ( 1 ... N ) ( B ` p ) =/= ( C ` p ) -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) ) )
482 283 481 sylbid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B =/= C -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) ) )
483 275 482 pm2.61dne 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( ( A. i e. ( 1 ... N ) ( ( ( B ` i ) <_ ( A ` i ) /\ ( A ` i ) <_ ( C ` i ) ) \/ ( ( C ` i ) <_ ( A ` i ) /\ ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) )
484 219 483 sylbid 
 |-  ( ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) ) )
485 213 484 impbid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( E. t e. ( 0 [,] 1 ) A. k e. ( 1 ... N ) ( A ` k ) = ( ( ( 1 - t ) x. ( B ` k ) ) + ( t x. ( C ` k ) ) ) <-> ( 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 ) ) ) ) ) )
486 1 485 bitrd 
 |-  ( ( 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 ) ) ) ) ) )