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 ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐾 ∈ ℝ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐾 · ( ( 𝐶𝑖 ) − ( 𝐴𝑖 ) ) ) + ( 𝐴𝑖 ) ) − ( 𝐴𝑖 ) ) · ( ( 𝐶𝑖 ) − ( 𝐴𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶𝑖 ) − ( ( 𝐾 · ( ( 𝐶𝑖 ) − ( 𝐴𝑖 ) ) ) + ( 𝐴𝑖 ) ) ) · ( ( 𝐴𝑖 ) − ( ( 𝐾 · ( ( 𝐶𝑖 ) − ( 𝐴𝑖 ) ) ) + ( 𝐴𝑖 ) ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴𝑖 ) − ( 𝐶𝑖 ) ) · ( ( ( 𝐾 · ( ( 𝐶𝑖 ) − ( 𝐴𝑖 ) ) ) + ( 𝐴𝑖 ) ) − ( 𝐶𝑖 ) ) ) ≤ 0 ) )

Proof

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