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