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

Theorem brbtwn2 24533
Description: Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.)
Assertion
Ref Expression
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 )
) ) ) ) )
Distinct variable groups:    i, N, j    A, i, j    B, i, j    C, i, j

Proof of Theorem brbtwn2
Dummy variables  k  p  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brbtwn 24527 . 2  |-  ( ( 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 24529 . . . . . . . . . 10  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  RR )
323ad2antl2 1118 . . . . . . . . 9  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( B `  i )  e.  RR )
4 fveere 24529 . . . . . . . . . 10  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  RR )
543ad2antl3 1119 . . . . . . . . 9  |-  ( ( ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  ( C `  i )  e.  RR )
63, 5jca 518 . . . . . . . 8  |-  ( ( ( 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 9111 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR )  -> 
( ( B `  i )  -  ( C `  i )
)  e.  RR )
873adant3 975 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( B `  i
)  -  ( C `
 i ) )  e.  RR )
98recnd 8861 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( B `  i
)  -  ( C `
 i ) )  e.  CC )
109sqvald 11242 . . . . . . . . . . . 12  |-  ( ( ( 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 )
) ) )
1110oveq2d 5874 . . . . . . . . . . 11  |-  ( ( ( 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 0re 8838 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
13 1re 8837 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
1412, 13elicc2i 10716 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
1514simp1bi 970 . . . . . . . . . . . . . 14  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  RR )
1615recnd 8861 . . . . . . . . . . . . 13  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  CC )
17163ad2ant3 978 . . . . . . . . . . . 12  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  t  e.  CC )
18 resubcl 9111 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR  /\  t  e.  RR )  ->  ( 1  -  t
)  e.  RR )
1913, 15, 18sylancr 644 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( 0 [,] 1 )  ->  (
1  -  t )  e.  RR )
20193ad2ant3 978 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  -  t )  e.  RR )
2120recnd 8861 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  -  t )  e.  CC )
2221negcld 9144 . . . . . . . . . . . 12  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  -u (
1  -  t )  e.  CC )
2317, 9, 22, 9mul4d 9024 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) )
24 recn 8827 . . . . . . . . . . . . . . 15  |-  ( ( B `  i )  e.  RR  ->  ( B `  i )  e.  CC )
25243ad2ant1 976 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  ( B `  i )  e.  CC )
26 recn 8827 . . . . . . . . . . . . . . 15  |-  ( ( C `  i )  e.  RR  ->  ( C `  i )  e.  CC )
27263ad2ant2 977 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  ( C `  i )  e.  CC )
2817, 25, 27subdid 9235 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
) ) )
29 ax-1cn 8795 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
30 subdir 9214 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
) ) ) )
3129, 30mp3an1 1264 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  -  t
)  e.  CC  /\  ( B `  i )  e.  CC )  -> 
( ( 1  -  ( 1  -  t
) )  x.  ( B `  i )
)  =  ( ( 1  x.  ( B `
 i ) )  -  ( ( 1  -  t )  x.  ( B `  i
) ) ) )
3221, 25, 31syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
) ) )
33 nncan 9076 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  CC  /\  t  e.  CC )  ->  ( 1  -  (
1  -  t ) )  =  t )
3429, 17, 33sylancr 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  -  ( 1  -  t ) )  =  t )
3534oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( 1  -  (
1  -  t ) )  x.  ( B `
 i ) )  =  ( t  x.  ( B `  i
) ) )
3625mulid2d 8853 . . . . . . . . . . . . . . . 16  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  x.  ( B `
 i ) )  =  ( B `  i ) )
3736oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
) ) )
3832, 35, 373eqtr3d 2323 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
t  x.  ( B `
 i ) )  =  ( ( B `
 i )  -  ( ( 1  -  t )  x.  ( B `  i )
) ) )
3938oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
) ) )
40 simp1 955 . . . . . . . . . . . . . . . 16  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  ( B `  i )  e.  RR )
4120, 40remulcld 8863 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( 1  -  t
)  x.  ( B `
 i ) )  e.  RR )
4241recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( 1  -  t
)  x.  ( B `
 i ) )  e.  CC )
43153ad2ant3 978 . . . . . . . . . . . . . . . 16  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  t  e.  RR )
44 simp2 956 . . . . . . . . . . . . . . . 16  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  ( C `  i )  e.  RR )
4543, 44remulcld 8863 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
t  x.  ( C `
 i ) )  e.  RR )
4645recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
t  x.  ( C `
 i ) )  e.  CC )
4725, 42, 46subsub4d 9188 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) ) )
4828, 39, 473eqtrd 2319 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
4921, 9mulneg1d 9232 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
) ) )
5021, 25, 27subdid 9235 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
) ) )
51 subdir 9214 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  CC  /\  t  e.  CC  /\  ( C `  i )  e.  CC )  ->  (
( 1  -  t
)  x.  ( C `
 i ) )  =  ( ( 1  x.  ( C `  i ) )  -  ( t  x.  ( C `  i )
) ) )
5229, 51mp3an1 1264 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( 1  -  t )  x.  ( C `  i )
)  =  ( ( 1  x.  ( C `
 i ) )  -  ( t  x.  ( C `  i
) ) ) )
5317, 27, 52syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
) ) )
5427mulid2d 8853 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  x.  ( C `
 i ) )  =  ( C `  i ) )
5554oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
) ) )
5653, 55eqtrd 2315 . . . . . . . . . . . . . . . 16  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( 1  -  t
)  x.  ( C `
 i ) )  =  ( ( C `
 i )  -  ( t  x.  ( C `  i )
) ) )
5756oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) ) )
5842, 27, 46subsub3d 9187 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
5950, 57, 583eqtrd 2319 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
6059negeqd 9046 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
6141, 45readdcld 8862 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( 1  -  t )  x.  ( B `  i )
)  +  ( t  x.  ( C `  i ) ) )  e.  RR )
6261recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( 1  -  t )  x.  ( B `  i )
)  +  ( t  x.  ( C `  i ) ) )  e.  CC )
6362, 27negsubdi2d 9173 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) ) )
6449, 60, 633eqtrd 2319 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
6548, 64oveq12d 5876 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) ) )
6611, 23, 653eqtr2rd 2322 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
6717, 21mulneg2d 9233 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
t  x.  -u (
1  -  t ) )  =  -u (
t  x.  ( 1  -  t ) ) )
6867oveq1d 5873 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
6943, 20remulcld 8863 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
t  x.  ( 1  -  t ) )  e.  RR )
7069recnd 8861 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
t  x.  ( 1  -  t ) )  e.  CC )
718resqcld 11271 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( B `  i )  -  ( C `  i )
) ^ 2 )  e.  RR )
7271recnd 8861 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( ( B `  i )  -  ( C `  i )
) ^ 2 )  e.  CC )
7370, 72mulneg1d 9232 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
7468, 73eqtrd 2315 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
7514simp2bi 971 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( 0 [,] 1 )  ->  0  <_  t )
7614simp3bi 972 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( 0 [,] 1 )  ->  t  <_  1 )
77 subge0 9287 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  RR  /\  t  e.  RR )  ->  ( 0  <_  (
1  -  t )  <-> 
t  <_  1 ) )
7813, 15, 77sylancr 644 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( 0 [,] 1 )  ->  (
0  <_  ( 1  -  t )  <->  t  <_  1 ) )
7976, 78mpbird 223 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( 0 [,] 1 )  ->  0  <_  ( 1  -  t
) )
8015, 19, 75, 79mulge0d 9349 . . . . . . . . . . . . . 14  |-  ( t  e.  ( 0 [,] 1 )  ->  0  <_  ( t  x.  (
1  -  t ) ) )
81803ad2ant3 978 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  0  <_  ( t  x.  (
1  -  t ) ) )
828sqge0d 11272 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  0  <_  ( ( ( B `
 i )  -  ( C `  i ) ) ^ 2 ) )
8369, 71, 81, 82mulge0d 9349 . . . . . . . . . . . 12  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  0  <_  ( ( t  x.  ( 1  -  t
) )  x.  (
( ( B `  i )  -  ( C `  i )
) ^ 2 ) ) )
8469, 71remulcld 8863 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( t  x.  (
1  -  t ) )  x.  ( ( ( B `  i
)  -  ( C `
 i ) ) ^ 2 ) )  e.  RR )
8584le0neg2d 9345 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
8683, 85mpbid 201 . . . . . . . . . . 11  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  -u (
( t  x.  (
1  -  t ) )  x.  ( ( ( B `  i
)  -  ( C `
 i ) ) ^ 2 ) )  <_  0 )
8774, 86eqbrtrd 4043 . . . . . . . . . 10  |-  ( ( ( B `  i
)  e.  RR  /\  ( C `  i )  e.  RR  /\  t  e.  ( 0 [,] 1
) )  ->  (
( t  x.  -u (
1  -  t ) )  x.  ( ( ( B `  i
)  -  ( C `
 i ) ) ^ 2 ) )  <_  0 )
8866, 87eqbrtrd 4043 . . . . . . . . 9  |-  ( ( ( 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 )
89883expa 1151 . . . . . . . 8  |-  ( ( ( ( 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 )
906, 89sylan 457 . . . . . . 7  |-  ( ( ( ( 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 )
9190an32s 779 . . . . . 6  |-  ( ( ( ( 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 )
9291ralrimiva 2626 . . . . 5  |-  ( ( ( 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
)
93 fveecn 24530 . . . . . . . . . . . 12  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  CC )
94 fveecn 24530 . . . . . . . . . . . 12  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
9593, 94anim12i 549 . . . . . . . . . . 11  |-  ( ( ( B  e.  ( EE `  N )  /\  i  e.  ( 1 ... N ) )  /\  ( C  e.  ( EE `  N )  /\  i  e.  ( 1 ... N
) ) )  -> 
( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC ) )
9695anandirs 804 . . . . . . . . . 10  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC ) )
97 fveecn 24530 . . . . . . . . . . . 12  |-  ( ( B  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( B `  j )  e.  CC )
98 fveecn 24530 . . . . . . . . . . . 12  |-  ( ( C  e.  ( EE
`  N )  /\  j  e.  ( 1 ... N ) )  ->  ( C `  j )  e.  CC )
9997, 98anim12i 549 . . . . . . . . . . 11  |-  ( ( ( B  e.  ( EE `  N )  /\  j  e.  ( 1 ... N ) )  /\  ( C  e.  ( EE `  N )  /\  j  e.  ( 1 ... N
) ) )  -> 
( ( B `  j )  e.  CC  /\  ( C `  j
)  e.  CC ) )
10099anandirs 804 . . . . . . . . . 10  |-  ( ( ( B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  j  e.  ( 1 ... N
) )  ->  (
( B `  j
)  e.  CC  /\  ( C `  j )  e.  CC ) )
10196, 100anim12dan 810 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
1021013adantl1 1111 . . . . . . . 8  |-  ( ( ( 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 ) ) )
103 subcl 9051 . . . . . . . . . . . . . 14  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( B `  i )  -  ( C `  i )
)  e.  CC )
1041033ad2ant1 976 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
105 subcl 9051 . . . . . . . . . . . . . . 15  |-  ( ( ( C `  j
)  e.  CC  /\  ( B `  j )  e.  CC )  -> 
( ( C `  j )  -  ( B `  j )
)  e.  CC )
106105ancoms 439 . . . . . . . . . . . . . 14  |-  ( ( ( B `  j
)  e.  CC  /\  ( C `  j )  e.  CC )  -> 
( ( C `  j )  -  ( B `  j )
)  e.  CC )
1071063ad2ant2 977 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
108104, 107mulcomd 8856 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
) ) )
109 simp2r 982 . . . . . . . . . . . . 13  |-  ( ( ( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC )  /\  ( ( B `
 j )  e.  CC  /\  ( C `
 j )  e.  CC )  /\  t  e.  CC )  ->  ( C `  j )  e.  CC )
110 simp2l 981 . . . . . . . . . . . . 13  |-  ( ( ( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC )  /\  ( ( B `
 j )  e.  CC  /\  ( C `
 j )  e.  CC )  /\  t  e.  CC )  ->  ( B `  j )  e.  CC )
111 simp1l 979 . . . . . . . . . . . . 13  |-  ( ( ( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC )  /\  ( ( B `
 j )  e.  CC  /\  ( C `
 j )  e.  CC )  /\  t  e.  CC )  ->  ( B `  i )  e.  CC )
112 simp1r 980 . . . . . . . . . . . . 13  |-  ( ( ( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC )  /\  ( ( B `
 j )  e.  CC  /\  ( C `
 j )  e.  CC )  /\  t  e.  CC )  ->  ( C `  i )  e.  CC )
113 mulsub2 9223 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
114109, 110, 111, 112, 113syl22anc 1183 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
) ) )
115108, 114eqtrd 2315 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
) ) )
116115oveq2d 5874 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) ) )
117 simp3 957 . . . . . . . . . . . 12  |-  ( ( ( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC )  /\  ( ( B `
 j )  e.  CC  /\  ( C `
 j )  e.  CC )  /\  t  e.  CC )  ->  t  e.  CC )
118 subcl 9051 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  t  e.  CC )  ->  ( 1  -  t
)  e.  CC )
11929, 118mpan 651 . . . . . . . . . . . . 13  |-  ( t  e.  CC  ->  (
1  -  t )  e.  CC )
1201193ad2ant3 978 . . . . . . . . . . . 12  |-  ( ( ( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC )  /\  ( ( B `
 j )  e.  CC  /\  ( C `
 j )  e.  CC )  /\  t  e.  CC )  ->  (
1  -  t )  e.  CC )
121117, 120, 104, 107mul4d 9024 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) ) )
122117, 111, 112subdid 9235 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
123120, 111, 31syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) ) )
12429, 33mpan 651 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  CC  ->  (
1  -  ( 1  -  t ) )  =  t )
1251243ad2ant3 978 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( B `  i )  e.  CC  /\  ( C `  i
)  e.  CC )  /\  ( ( B `
 j )  e.  CC  /\  ( C `
 j )  e.  CC )  /\  t  e.  CC )  ->  (
1  -  ( 1  -  t ) )  =  t )
126125oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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
) ) )
127111mulid2d 8853 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
128127oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) ) )
129123, 126, 1283eqtr3d 2323 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) ) )
130129oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
131120, 111mulcld 8855 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
132117, 112mulcld 8855 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
133111, 131, 132subsub4d 9188 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) ) )
134122, 130, 1333eqtrd 2319 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) ) ) )
135120, 109, 110subdid 9235 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) ) )
136 subdir 9214 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  t  e.  CC  /\  ( C `  j )  e.  CC )  ->  (
( 1  -  t
)  x.  ( C `
 j ) )  =  ( ( 1  x.  ( C `  j ) )  -  ( t  x.  ( C `  j )
) ) )
13729, 136mp3an1 1264 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  CC  /\  ( C `  j )  e.  CC )  -> 
( ( 1  -  t )  x.  ( C `  j )
)  =  ( ( 1  x.  ( C `
 j ) )  -  ( t  x.  ( C `  j
) ) ) )
138117, 109, 137syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
) ) )
139109mulid2d 8853 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) )
140139oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
) ) )
141138, 140eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) ) )
142141oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) ) )
143135, 142eqtrd 2315 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
144117, 109mulcld 8855 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
145120, 110mulcld 8855 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
146109, 144, 145sub32d 9189 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
147109, 145, 144subsub4d 9188 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) ) )
148143, 146, 1473eqtrd 2319 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) ) ) )
149134, 148oveq12d 5876 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) ) ) ) )
150121, 149eqtrd 2315 . . . . . . . . . 10  |-  ( ( ( ( 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
) ) ) ) ) )
151 subcl 9051 . . . . . . . . . . . . 13  |-  ( ( ( B `  j
)  e.  CC  /\  ( C `  j )  e.  CC )  -> 
( ( B `  j )  -  ( C `  j )
)  e.  CC )
1521513ad2ant2 977 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
153 subcl 9051 . . . . . . . . . . . . . 14  |-  ( ( ( C `  i
)  e.  CC  /\  ( B `  i )  e.  CC )  -> 
( ( C `  i )  -  ( B `  i )
)  e.  CC )
154153ancoms 439 . . . . . . . . . . . . 13  |-  ( ( ( B `  i
)  e.  CC  /\  ( C `  i )  e.  CC )  -> 
( ( C `  i )  -  ( B `  i )
)  e.  CC )
1551543ad2ant1 976 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
156117, 120, 152, 155mul4d 9024 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) ) )
157117, 110, 109subdid 9235 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
158 subdir 9214 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
) ) ) )
15929, 158mp3an1 1264 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  -  t
)  e.  CC  /\  ( B `  j )  e.  CC )  -> 
( ( 1  -  ( 1  -  t
) )  x.  ( B `  j )
)  =  ( ( 1  x.  ( B `
 j ) )  -  ( ( 1  -  t )  x.  ( B `  j
) ) ) )
160120, 110, 159syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) ) )
161125oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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
) ) )
162110mulid2d 8853 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
163162oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) ) )
164160, 161, 1633eqtr3rd 2324 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
165164oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
166110, 145, 144subsub4d 9188 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) ) )
167157, 165, 1663eqtr2d 2321 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) ) ) )
168120, 112, 111subdid 9235 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
169117, 112, 52syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) ) )
170112mulid2d 8853 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
171170oveq1d 5873 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) ) )
172169, 171eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) ) )
173172oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
) ) )
174112, 132, 131sub32d 9189 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) ) )
175112, 131, 132subsub4d 9188 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) ) ) )
176174, 175eqtrd 2315 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) ) )
177168, 173, 1763eqtrd 2319 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) ) ) )
178167, 177oveq12d 5876 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) ) ) ) )
179156, 178eqtrd 2315 . . . . . . . . . 10  |-  ( ( ( ( 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
) ) ) ) ) )
180116, 150, 1793eqtr3d 2323 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) ) ) ) )
1811803expa 1151 . . . . . . . 8  |-  ( ( ( ( ( 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 )
) ) ) ) )
182102, 16, 181syl2an 463 . . . . . . 7  |-  ( ( ( ( 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 )
) ) ) ) )
183182an32s 779 . . . . . 6  |-  ( ( ( ( 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
) ) ) ) ) )
184183ralrimivva 2635 . . . . 5  |-  ( ( ( 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 )
) ) ) ) )
185 fveq2 5525 . . . . . . . . . . 11  |-  ( k  =  i  ->  ( A `  k )  =  ( A `  i ) )
186 fveq2 5525 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  ( B `  k )  =  ( B `  i ) )
187186oveq2d 5874 . . . . . . . . . . . 12  |-  ( k  =  i  ->  (
( 1  -  t
)  x.  ( B `
 k ) )  =  ( ( 1  -  t )  x.  ( B `  i
) ) )
188 fveq2 5525 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  ( C `  k )  =  ( C `  i ) )
189188oveq2d 5874 . . . . . . . . . . . 12  |-  ( k  =  i  ->  (
t  x.  ( C `
 k ) )  =  ( t  x.  ( C `  i
) ) )
190187, 189oveq12d 5876 . . . . . . . . . . 11  |-  ( k  =  i  ->  (
( ( 1  -  t )  x.  ( B `  k )
)  +  ( t  x.  ( C `  k ) ) )  =  ( ( ( 1  -  t )  x.  ( B `  i ) )  +  ( t  x.  ( C `  i )
) ) )
191185, 190eqeq12d 2297 . . . . . . . . . 10  |-  ( k  =  i  ->  (
( A `  k
)  =  ( ( ( 1  -  t
)  x.  ( B `
 k ) )  +  ( t  x.  ( C `  k
) ) )  <->  ( A `  i )  =  ( ( ( 1  -  t )  x.  ( B `  i )
)  +  ( t  x.  ( C `  i ) ) ) ) )
192191rspccva 2883 . . . . . . . . 9  |-  ( ( 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 ) ) ) )
193 oveq2 5866 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) ) )
194 oveq2 5866 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) ) )
195193, 194oveq12d 5876 . . . . . . . . . 10  |-  ( ( 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 ) ) ) ) ) )
196195breq1d 4033 . . . . . . . . 9  |-  ( ( 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 ) )
197192, 196syl 15 . . . . . . . 8  |-  ( ( 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 ) )
198197ralbidva 2559 . . . . . . 7  |-  ( 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
) )
199 fveq2 5525 . . . . . . . . . . . 12  |-  ( k  =  j  ->  ( A `  k )  =  ( A `  j ) )
200 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  ( B `  k )  =  ( B `  j ) )
201200oveq2d 5874 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  (
( 1  -  t
)  x.  ( B `
 k ) )  =  ( ( 1  -  t )  x.  ( B `  j
) ) )
202 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( k  =  j  ->  ( C `  k )  =  ( C `  j ) )
203202oveq2d 5874 . . . . . . . . . . . . 13  |-  ( k  =  j  ->  (
t  x.  ( C `
 k ) )  =  ( t  x.  ( C `  j
) ) )
204201, 203oveq12d 5876 . . . . . . . . . . . 12  |-  ( k  =  j  ->  (
( ( 1  -  t )  x.  ( B `  k )
)  +  ( t  x.  ( C `  k ) ) )  =  ( ( ( 1  -  t )  x.  ( B `  j ) )  +  ( t  x.  ( C `  j )
) ) )
205199, 204eqeq12d 2297 . . . . . . . . . . 11  |-  ( k  =  j  ->  (
( A `  k
)  =  ( ( ( 1  -  t
)  x.  ( B `
 k ) )  +  ( t  x.  ( C `  k
) ) )  <->  ( A `  j )  =  ( ( ( 1  -  t )  x.  ( B `  j )
)  +  ( t  x.  ( C `  j ) ) ) ) )
206205rspccva 2883 . . . . . . . . . 10  |-  ( ( 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 ) ) ) )
207 oveq2 5866 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) ) )
208193, 207oveqan12d 5877 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) ) )
209 oveq2 5866 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) ) )
210209, 194oveqan12rd 5878 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) ) )
211208, 210eqeq12d 2297 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) ) ) )
212192, 206, 211syl2an 463 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) ) ) )
213212anandis 803 . . . . . . . 8  |-  ( ( 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
) ) ) ) ) ) )
2142132ralbidva 2583 . . . . . . 7  |-  ( 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 )
) ) ) ) ) )
215198, 214anbi12d 691 . . . . . 6  |-  ( 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 ) ) ) ) ) ) ) )
216215biimprcd 216 . . . . 5  |-  ( ( 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 )
) ) ) ) )
21792, 184, 216syl2anc 642 . . . 4  |-  ( ( ( 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