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 mulid2d
 |-  ( ( ( 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 mulid2d
 |-  ( ( ( 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 mulid2d
 |-  ( ( ( ( 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 mulid2d
 |-  ( ( ( ( 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 mulid2d
 |-  ( ( ( ( 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 mulid2d
 |-  ( ( ( ( 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 syl5bb
 |-  ( ( ( ( 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 mulid2
 |-  ( ( 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 addid1
 |-  ( ( 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 addid2d
 |-  ( ( ( ( ( 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 ) ) ) ) ) )