Metamath Proof Explorer

Theorem colinearalglem4

Description: Lemma for colinearalg . Prove a disjunction that will be needed in the final proof. (Contributed by Scott Fenton, 27-Jun-2013)

Ref Expression
Assertion colinearalglem4 
|- ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( A. i e. ( 1 ... N ) ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 ) )

Proof

Step Hyp Ref Expression
1 relin01 
 |-  ( K e. RR -> ( K <_ 0 \/ ( 0 <_ K /\ K <_ 1 ) \/ 1 <_ K ) )
2 1 adantl 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( K <_ 0 \/ ( 0 <_ K /\ K <_ 1 ) \/ 1 <_ K ) )
3 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
4 3 adantlr 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
5 fveere 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. RR )
6 5 adantll 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. RR )
7 4 6 jca 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) )
8 simprl 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> K e. RR )
9 8 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> K e. CC )
10 resubcl 
 |-  ( ( ( C ` i ) e. RR /\ ( A ` i ) e. RR ) -> ( ( C ` i ) - ( A ` i ) ) e. RR )
11 10 ancoms 
 |-  ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) -> ( ( C ` i ) - ( A ` i ) ) e. RR )
12 11 adantr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( C ` i ) - ( A ` i ) ) e. RR )
13 12 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( C ` i ) - ( A ` i ) ) e. CC )
14 9 13 13 mulassd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( K x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
15 8 12 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( K x. ( ( C ` i ) - ( A ` i ) ) ) e. RR )
16 15 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( K x. ( ( C ` i ) - ( A ` i ) ) ) e. CC )
17 recn 
 |-  ( ( A ` i ) e. RR -> ( A ` i ) e. CC )
18 17 ad2antrr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( A ` i ) e. CC )
19 16 18 pncand 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) = ( K x. ( ( C ` i ) - ( A ` i ) ) ) )
20 19 oveq1d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) x. ( ( C ` i ) - ( A ` i ) ) ) )
21 13 sqvald 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) = ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) )
22 21 oveq2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( K x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) = ( K x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
23 14 20 22 3eqtr4d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( K x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
24 simprr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> K <_ 0 )
25 12 sqge0d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> 0 <_ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) )
26 24 25 jca 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( K <_ 0 /\ 0 <_ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
27 26 orcd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( K <_ 0 /\ 0 <_ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) \/ ( 0 <_ K /\ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) <_ 0 ) ) )
28 12 resqcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) e. RR )
29 mulle0b 
 |-  ( ( K e. RR /\ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) e. RR ) -> ( ( K x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) <_ 0 <-> ( ( K <_ 0 /\ 0 <_ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) \/ ( 0 <_ K /\ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) <_ 0 ) ) ) )
30 8 28 29 syl2anc 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( K x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) <_ 0 <-> ( ( K <_ 0 /\ 0 <_ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) \/ ( 0 <_ K /\ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) <_ 0 ) ) ) )
31 27 30 mpbird 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( K x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) <_ 0 )
32 23 31 eqbrtrd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 )
33 7 32 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) /\ ( K e. RR /\ K <_ 0 ) ) -> ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 )
34 33 an32s 
 |-  ( ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( K e. RR /\ K <_ 0 ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 )
35 34 ralrimiva 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( K e. RR /\ K <_ 0 ) ) -> A. i e. ( 1 ... N ) ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 )
36 35 expr 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( K <_ 0 -> A. i e. ( 1 ... N ) ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 ) )
37 recn 
 |-  ( ( C ` i ) e. RR -> ( C ` i ) e. CC )
38 37 ad2antlr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( C ` i ) e. CC )
39 17 ad2antrr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( A ` i ) e. CC )
40 simprl 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> K e. RR )
41 11 adantr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( C ` i ) - ( A ` i ) ) e. RR )
42 40 41 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( K x. ( ( C ` i ) - ( A ` i ) ) ) e. RR )
43 42 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( K x. ( ( C ` i ) - ( A ` i ) ) ) e. CC )
44 38 39 43 sub32d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( A ` i ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( ( C ` i ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) - ( A ` i ) ) )
45 ax-1cn 
 |-  1 e. CC
46 40 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> K e. CC )
47 41 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( C ` i ) - ( A ` i ) ) e. CC )
48 subdir 
 |-  ( ( 1 e. CC /\ K e. CC /\ ( ( C ` i ) - ( A ` i ) ) e. CC ) -> ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) )
49 45 46 47 48 mp3an2i 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) )
50 47 mullidd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( C ` i ) - ( A ` i ) ) )
51 50 oveq1d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( ( C ` i ) - ( A ` i ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) )
52 49 51 eqtr2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( A ` i ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) )
53 38 43 39 subsub4d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) - ( A ` i ) ) = ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) )
54 44 52 53 3eqtr3rd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) = ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) )
55 39 39 43 sub32d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( A ` i ) - ( A ` i ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( ( A ` i ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) - ( A ` i ) ) )
56 39 subidd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( A ` i ) - ( A ` i ) ) = 0 )
57 56 oveq1d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( A ` i ) - ( A ` i ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( 0 - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) )
58 df-neg 
 |-  -u ( K x. ( ( C ` i ) - ( A ` i ) ) ) = ( 0 - ( K x. ( ( C ` i ) - ( A ` i ) ) ) )
59 57 58 eqtr4di 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( A ` i ) - ( A ` i ) ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = -u ( K x. ( ( C ` i ) - ( A ` i ) ) ) )
60 39 43 39 subsub4d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( A ` i ) - ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) - ( A ` i ) ) = ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) )
61 55 59 60 3eqtr3rd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) = -u ( K x. ( ( C ` i ) - ( A ` i ) ) ) )
62 54 61 oveq12d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) = ( ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) x. -u ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) )
63 1re 
 |-  1 e. RR
64 resubcl 
 |-  ( ( 1 e. RR /\ K e. RR ) -> ( 1 - K ) e. RR )
65 63 64 mpan 
 |-  ( K e. RR -> ( 1 - K ) e. RR )
66 65 ad2antrl 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( 1 - K ) e. RR )
67 66 41 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) e. RR )
68 67 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) e. CC )
69 68 43 mulneg2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) x. -u ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = -u ( ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) x. ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) )
70 66 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( 1 - K ) e. CC )
71 70 47 46 47 mul4d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) x. ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
72 71 negeqd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> -u ( ( ( 1 - K ) x. ( ( C ` i ) - ( A ` i ) ) ) x. ( K x. ( ( C ` i ) - ( A ` i ) ) ) ) = -u ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
73 62 69 72 3eqtrd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) = -u ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
74 66 40 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( 1 - K ) x. K ) e. RR )
75 41 resqcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) e. RR )
76 simpl 
 |-  ( ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) -> K e. RR )
77 63 76 64 sylancr 
 |-  ( ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) -> ( 1 - K ) e. RR )
78 subge0 
 |-  ( ( 1 e. RR /\ K e. RR ) -> ( 0 <_ ( 1 - K ) <-> K <_ 1 ) )
79 63 78 mpan 
 |-  ( K e. RR -> ( 0 <_ ( 1 - K ) <-> K <_ 1 ) )
80 79 biimpar 
 |-  ( ( K e. RR /\ K <_ 1 ) -> 0 <_ ( 1 - K ) )
81 80 adantrl 
 |-  ( ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) -> 0 <_ ( 1 - K ) )
82 simprl 
 |-  ( ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) -> 0 <_ K )
83 77 76 81 82 mulge0d 
 |-  ( ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) -> 0 <_ ( ( 1 - K ) x. K ) )
84 83 adantl 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> 0 <_ ( ( 1 - K ) x. K ) )
85 41 sqge0d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> 0 <_ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) )
86 74 75 84 85 mulge0d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> 0 <_ ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
87 47 sqvald 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) = ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) )
88 87 oveq2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) = ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
89 86 88 breqtrd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> 0 <_ ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
90 41 41 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) e. RR )
91 74 90 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) e. RR )
92 91 le0neg2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( 0 <_ ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) <-> -u ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) <_ 0 ) )
93 89 92 mpbid 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> -u ( ( ( 1 - K ) x. K ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) <_ 0 )
94 73 93 eqbrtrd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 )
95 7 94 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 )
96 95 an32s 
 |-  ( ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 )
97 96 ralrimiva 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( K e. RR /\ ( 0 <_ K /\ K <_ 1 ) ) ) -> A. i e. ( 1 ... N ) ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 )
98 97 expr 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( ( 0 <_ K /\ K <_ 1 ) -> A. i e. ( 1 ... N ) ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 ) )
99 37 ad2antlr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( C ` i ) e. CC )
100 17 ad2antrr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( A ` i ) e. CC )
101 99 100 negsubdi2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> -u ( ( C ` i ) - ( A ` i ) ) = ( ( A ` i ) - ( C ` i ) ) )
102 101 oveq1d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( -u ( ( C ` i ) - ( A ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( ( A ` i ) - ( C ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
103 simplr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( C ` i ) e. RR )
104 simpll 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( A ` i ) e. RR )
105 103 104 10 syl2anc 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( C ` i ) - ( A ` i ) ) e. RR )
106 105 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( C ` i ) - ( A ` i ) ) e. CC )
107 peano2rem 
 |-  ( K e. RR -> ( K - 1 ) e. RR )
108 107 ad2antrl 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( K - 1 ) e. RR )
109 108 105 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) e. RR )
110 109 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) e. CC )
111 106 110 mulneg1d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( -u ( ( C ` i ) - ( A ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) = -u ( ( ( C ` i ) - ( A ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
112 108 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( K - 1 ) e. CC )
113 106 112 106 mul12d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( C ` i ) - ( A ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
114 106 sqvald 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) = ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) )
115 114 oveq2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) = ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) ) )
116 113 115 eqtr4d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( C ` i ) - ( A ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
117 116 negeqd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> -u ( ( ( C ` i ) - ( A ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) = -u ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
118 111 117 eqtrd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( -u ( ( C ` i ) - ( A ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) = -u ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
119 simprl 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> K e. RR )
120 119 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> K e. CC )
121 subdir 
 |-  ( ( K e. CC /\ 1 e. CC /\ ( ( C ` i ) - ( A ` i ) ) e. CC ) -> ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) - ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) ) )
122 45 121 mp3an2 
 |-  ( ( K e. CC /\ ( ( C ` i ) - ( A ` i ) ) e. CC ) -> ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) - ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) ) )
123 120 106 122 syl2anc 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) - ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) ) )
124 106 mullidd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( C ` i ) - ( A ` i ) ) )
125 124 oveq2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) - ( 1 x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) - ( ( C ` i ) - ( A ` i ) ) ) )
126 119 105 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( K x. ( ( C ` i ) - ( A ` i ) ) ) e. RR )
127 126 recnd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( K x. ( ( C ` i ) - ( A ` i ) ) ) e. CC )
128 127 99 100 subsub3d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) - ( ( C ` i ) - ( A ` i ) ) ) = ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) )
129 123 125 128 3eqtrd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) = ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) )
130 129 oveq2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( A ` i ) - ( C ` i ) ) x. ( ( K - 1 ) x. ( ( C ` i ) - ( A ` i ) ) ) ) = ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) )
131 102 118 130 3eqtr3rd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) = -u ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
132 105 resqcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) e. RR )
133 simprr 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> 1 <_ K )
134 subge0 
 |-  ( ( K e. RR /\ 1 e. RR ) -> ( 0 <_ ( K - 1 ) <-> 1 <_ K ) )
135 63 134 mpan2 
 |-  ( K e. RR -> ( 0 <_ ( K - 1 ) <-> 1 <_ K ) )
136 135 ad2antrl 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( 0 <_ ( K - 1 ) <-> 1 <_ K ) )
137 133 136 mpbird 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> 0 <_ ( K - 1 ) )
138 105 sqge0d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> 0 <_ ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) )
139 108 132 137 138 mulge0d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> 0 <_ ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) )
140 108 132 remulcld 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) e. RR )
141 140 le0neg2d 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( 0 <_ ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) <-> -u ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) <_ 0 ) )
142 139 141 mpbid 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> -u ( ( K - 1 ) x. ( ( ( C ` i ) - ( A ` i ) ) ^ 2 ) ) <_ 0 )
143 131 142 eqbrtrd 
 |-  ( ( ( ( A ` i ) e. RR /\ ( C ` i ) e. RR ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 )
144 7 143 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) /\ ( K e. RR /\ 1 <_ K ) ) -> ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 )
145 144 an32s 
 |-  ( ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( K e. RR /\ 1 <_ K ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 )
146 145 ralrimiva 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( K e. RR /\ 1 <_ K ) ) -> A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 )
147 146 expr 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( 1 <_ K -> A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 ) )
148 36 98 147 3orim123d 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( ( K <_ 0 \/ ( 0 <_ K /\ K <_ 1 ) \/ 1 <_ K ) -> ( A. i e. ( 1 ... N ) ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 ) ) )
149 2 148 mpd 
 |-  ( ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ K e. RR ) -> ( A. i e. ( 1 ... N ) ( ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( A ` i ) ) x. ( ( C ` i ) - ( A ` i ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( C ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) x. ( ( A ` i ) - ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) ) ) <_ 0 \/ A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( C ` i ) ) x. ( ( ( K x. ( ( C ` i ) - ( A ` i ) ) ) + ( A ` i ) ) - ( C ` i ) ) ) <_ 0 ) )