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