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 ) ) ) ) ) ) |