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 mullidd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) ∧ ( 𝐾 ∈ ℝ ∧ ( 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 mullidd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) ∧ ( 𝐾 ∈ ℝ ∧ 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 ) )