Theorem colinearalglem4 25789

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

Assertion

Ref	Expression
colinearalglem4	⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0))

Distinct variable groups:   𝐴,𝑖   𝐶,𝑖   𝑖,𝐾   𝑖,𝑁

Proof of Theorem colinearalglem4

Step	Hyp	Ref	Expression
1		relin01 10552	. . 3 ⊢ (𝐾 ∈ ℝ → (𝐾 ≤ 0 ∨ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1) ∨ 1 ≤ 𝐾))
2	1	adantl 482	. 2 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → (𝐾 ≤ 0 ∨ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1) ∨ 1 ≤ 𝐾))
3		fveere 25781	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
4	3	adantlr 751	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
5		fveere 25781	. . . . . . . . 9 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
6	5	adantll 750	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
7	4, 6	jca 554	. . . . . . 7 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ))
8		simprl 794	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → 𝐾 ∈ ℝ)
9	8	recnd 10068	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → 𝐾 ∈ ℂ)
10		resubcl 10345	. . . . . . . . . . . . 13 ⊢ (((𝐶‘𝑖) ∈ ℝ ∧ (𝐴‘𝑖) ∈ ℝ) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℝ)
11	10	ancoms 469	. . . . . . . . . . . 12 ⊢ (((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℝ)
12	11	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℝ)
13	12	recnd 10068	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ)
14	9, 13, 13	mulassd 10063	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = (𝐾 · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
15	8, 12	remulcld 10070	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℝ)
16	15	recnd 10068	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ)
17		recn 10026	. . . . . . . . . . . 12 ⊢ ((𝐴‘𝑖) ∈ ℝ → (𝐴‘𝑖) ∈ ℂ)
18	17	ad2antrr 762	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (𝐴‘𝑖) ∈ ℂ)
19	16, 18	pncand 10393	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) = (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))))
20	19	oveq1d 6665	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) · ((𝐶‘𝑖) − (𝐴‘𝑖))))
21	13	sqvald 13005	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) = (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))
22	21	oveq2d 6666	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (𝐾 · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) = (𝐾 · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
23	14, 20, 22	3eqtr4d 2666	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = (𝐾 · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
24		simprr 796	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → 𝐾 ≤ 0)
25	12	sqge0d 13036	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → 0 ≤ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2))
26	24, 25	jca 554	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (𝐾 ≤ 0 ∧ 0 ≤ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
27	26	orcd 407	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((𝐾 ≤ 0 ∧ 0 ≤ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ∨ (0 ≤ 𝐾 ∧ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) ≤ 0)))
28	12	resqcld 13035	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℝ)
29		mulle0b 10894	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℝ ∧ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℝ) → ((𝐾 · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ≤ 0 ↔ ((𝐾 ≤ 0 ∧ 0 ≤ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ∨ (0 ≤ 𝐾 ∧ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) ≤ 0))))
30	8, 28, 29	syl2anc 693	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((𝐾 · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ≤ 0 ↔ ((𝐾 ≤ 0 ∧ 0 ≤ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ∨ (0 ≤ 𝐾 ∧ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) ≤ 0))))
31	27, 30	mpbird 247	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → (𝐾 · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ≤ 0)
32	23, 31	eqbrtrd 4675	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)
33	7, 32	sylan 488	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)
34	33	an32s 846	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)
35	34	ralrimiva 2966	. . . 4 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ≤ 0)) → ∀𝑖 ∈ (1...𝑁)((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)
36	35	expr 643	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → (𝐾 ≤ 0 → ∀𝑖 ∈ (1...𝑁)((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0))
37		recn 10026	. . . . . . . . . . . . 13 ⊢ ((𝐶‘𝑖) ∈ ℝ → (𝐶‘𝑖) ∈ ℂ)
38	37	ad2antlr 763	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (𝐶‘𝑖) ∈ ℂ)
39	17	ad2antrr 762	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (𝐴‘𝑖) ∈ ℂ)
40		simprl 794	. . . . . . . . . . . . . 14 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → 𝐾 ∈ ℝ)
41	11	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℝ)
42	40, 41	remulcld 10070	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℝ)
43	42	recnd 10068	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ)
44	38, 39, 43	sub32d 10424	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − (𝐴‘𝑖)) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = (((𝐶‘𝑖) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) − (𝐴‘𝑖)))
45	40	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → 𝐾 ∈ ℂ)
46	41	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ)
47		ax-1cn 9994	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
48		subdir 10464	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) → ((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((1 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
49	47, 48	mp3an1 1411	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℂ ∧ ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) → ((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((1 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
50	45, 46, 49	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((1 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
51	46	mulid2d 10058	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (1 · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((𝐶‘𝑖) − (𝐴‘𝑖)))
52	51	oveq1d 6665	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((1 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = (((𝐶‘𝑖) − (𝐴‘𝑖)) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
53	50, 52	eqtr2d 2657	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − (𝐴‘𝑖)) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = ((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))))
54	38, 43, 39	subsub4d 10423	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) − (𝐴‘𝑖)) = ((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))))
55	44, 53, 54	3eqtr3rd 2665	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) = ((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))))
56	39, 39, 43	sub32d 10424	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐴‘𝑖) − (𝐴‘𝑖)) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = (((𝐴‘𝑖) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) − (𝐴‘𝑖)))
57	39	subidd 10380	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((𝐴‘𝑖) − (𝐴‘𝑖)) = 0)
58	57	oveq1d 6665	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐴‘𝑖) − (𝐴‘𝑖)) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = (0 − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
59		df-neg 10269	. . . . . . . . . . . 12 ⊢ -(𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) = (0 − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))))
60	58, 59	syl6eqr 2674	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐴‘𝑖) − (𝐴‘𝑖)) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = -(𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))))
61	39, 43, 39	subsub4d 10423	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐴‘𝑖) − (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) − (𝐴‘𝑖)) = ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))))
62	56, 60, 61	3eqtr3rd 2665	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) = -(𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))))
63	55, 62	oveq12d 6668	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) = (((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) · -(𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
64		1re 10039	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
65		resubcl 10345	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (1 − 𝐾) ∈ ℝ)
66	64, 65	mpan 706	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℝ → (1 − 𝐾) ∈ ℝ)
67	66	ad2antrl 764	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (1 − 𝐾) ∈ ℝ)
68	67, 41	remulcld 10070	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℝ)
69	68	recnd 10068	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ)
70	69, 43	mulneg2d 10484	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) · -(𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = -(((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) · (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
71	67	recnd 10068	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (1 − 𝐾) ∈ ℂ)
72	71, 46, 45, 46	mul4d 10248	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) · (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = (((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
73	72	negeqd 10275	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → -(((1 − 𝐾) · ((𝐶‘𝑖) − (𝐴‘𝑖))) · (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = -(((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
74	63, 70, 73	3eqtrd 2660	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) = -(((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
75	67, 40	remulcld 10070	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ((1 − 𝐾) · 𝐾) ∈ ℝ)
76	41	resqcld 13035	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℝ)
77		simpl 473	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1)) → 𝐾 ∈ ℝ)
78	64, 77, 65	sylancr 695	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1)) → (1 − 𝐾) ∈ ℝ)
79		subge0 10541	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (0 ≤ (1 − 𝐾) ↔ 𝐾 ≤ 1))
80	64, 79	mpan 706	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℝ → (0 ≤ (1 − 𝐾) ↔ 𝐾 ≤ 1))
81	80	biimpar 502	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ ℝ ∧ 𝐾 ≤ 1) → 0 ≤ (1 − 𝐾))
82	81	adantrl 752	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1)) → 0 ≤ (1 − 𝐾))
83		simprl 794	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1)) → 0 ≤ 𝐾)
84	78, 77, 82, 83	mulge0d 10604	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1)) → 0 ≤ ((1 − 𝐾) · 𝐾))
85	84	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → 0 ≤ ((1 − 𝐾) · 𝐾))
86	41	sqge0d 13036	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → 0 ≤ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2))
87	75, 76, 85, 86	mulge0d 10604	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → 0 ≤ (((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
88	46	sqvald 13005	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) = (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))
89	88	oveq2d 6666	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) = (((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
90	87, 89	breqtrd 4679	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → 0 ≤ (((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
91	41, 41	remulcld 10070	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℝ)
92	75, 91	remulcld 10070	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∈ ℝ)
93	92	le0neg2d 10600	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (0 ≤ (((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ↔ -(((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ≤ 0))
94	90, 93	mpbid 222	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → -(((1 − 𝐾) · 𝐾) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ≤ 0)
95	74, 94	eqbrtrd 4675	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)
96	7, 95	sylan 488	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → (((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)
97	96	an32s 846	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)
98	97	ralrimiva 2966	. . . 4 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐾 ∈ ℝ ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1))) → ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)
99	98	expr 643	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → ((0 ≤ 𝐾 ∧ 𝐾 ≤ 1) → ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0))
100	37	ad2antlr 763	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐶‘𝑖) ∈ ℂ)
101	17	ad2antrr 762	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐴‘𝑖) ∈ ℂ)
102	100, 101	negsubdi2d 10408	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → -((𝐶‘𝑖) − (𝐴‘𝑖)) = ((𝐴‘𝑖) − (𝐶‘𝑖)))
103	102	oveq1d 6665	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (-((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = (((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
104		simplr 792	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐶‘𝑖) ∈ ℝ)
105		simpll 790	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐴‘𝑖) ∈ ℝ)
106	104, 105, 10	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℝ)
107	106	recnd 10068	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ)
108		peano2rem 10348	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
109	108	ad2antrl 764	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐾 − 1) ∈ ℝ)
110	109, 106	remulcld 10070	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℝ)
111	110	recnd 10068	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ)
112	107, 111	mulneg1d 10483	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (-((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = -(((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
113	109	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐾 − 1) ∈ ℂ)
114	107, 113, 107	mul12d 10245	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = ((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
115	107	sqvald 13005	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) = (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))
116	115	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) = ((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
117	114, 116	eqtr4d 2659	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = ((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
118	117	negeqd 10275	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → -(((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = -((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
119	112, 118	eqtrd 2656	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (-((𝐶‘𝑖) − (𝐴‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = -((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
120		simprl 794	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → 𝐾 ∈ ℝ)
121	120	recnd 10068	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → 𝐾 ∈ ℂ)
122		subdir 10464	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) → ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (1 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
123	47, 122	mp3an2 1412	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℂ ∧ ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) → ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (1 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
124	121, 107, 123	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (1 · ((𝐶‘𝑖) − (𝐴‘𝑖)))))
125	107	mulid2d 10058	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (1 · ((𝐶‘𝑖) − (𝐴‘𝑖))) = ((𝐶‘𝑖) − (𝐴‘𝑖)))
126	125	oveq2d 6666	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − (1 · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − ((𝐶‘𝑖) − (𝐴‘𝑖))))
127	120, 106	remulcld 10070	. . . . . . . . . . . . 13 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℝ)
128	127	recnd 10068	. . . . . . . . . . . 12 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ)
129	128, 100, 101	subsub3d 10422	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) − ((𝐶‘𝑖) − (𝐴‘𝑖))) = (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖)))
130	124, 126, 129	3eqtrd 2660	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖)))
131	130	oveq2d 6666	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐾 − 1) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) = (((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))))
132	103, 119, 131	3eqtr3rd 2665	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) = -((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
133	106	resqcld 13035	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐶‘𝑖) − (𝐴‘𝑖))↑2) ∈ ℝ)
134		simprr 796	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → 1 ≤ 𝐾)
135		subge0 10541	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (0 ≤ (𝐾 − 1) ↔ 1 ≤ 𝐾))
136	64, 135	mpan2 707	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℝ → (0 ≤ (𝐾 − 1) ↔ 1 ≤ 𝐾))
137	136	ad2antrl 764	. . . . . . . . . . 11 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (0 ≤ (𝐾 − 1) ↔ 1 ≤ 𝐾))
138	134, 137	mpbird 247	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → 0 ≤ (𝐾 − 1))
139	106	sqge0d 13036	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → 0 ≤ (((𝐶‘𝑖) − (𝐴‘𝑖))↑2))
140	109, 133, 138, 139	mulge0d 10604	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → 0 ≤ ((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)))
141	109, 133	remulcld 10070	. . . . . . . . . 10 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ∈ ℝ)
142	141	le0neg2d 10600	. . . . . . . . 9 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (0 ≤ ((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ↔ -((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ≤ 0))
143	140, 142	mpbid 222	. . . . . . . 8 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → -((𝐾 − 1) · (((𝐶‘𝑖) − (𝐴‘𝑖))↑2)) ≤ 0)
144	132, 143	eqbrtrd 4675	. . . . . . 7 ⊢ ((((𝐴‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)
145	7, 144	sylan 488	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → (((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)
146	145	an32s 846	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)
147	146	ralrimiva 2966	. . . 4 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐾 ∈ ℝ ∧ 1 ≤ 𝐾)) → ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)
148	147	expr 643	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → (1 ≤ 𝐾 → ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0))
149	36, 99, 148	3orim123d 1407	. 2 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → ((𝐾 ≤ 0 ∨ (0 ≤ 𝐾 ∧ 𝐾 ≤ 1) ∨ 1 ≤ 𝐾) → (∀𝑖 ∈ (1...𝑁)((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)))
150	2, 149	mpd 15	1 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝐾 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)((((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − ((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · (((𝐾 · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0))

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∨ w3o 1036   = wceq 1483   ∈ wcel 1990  ∀wral 2912   class class class wbr 4653  ‘cfv 5888  (class class class)co 6650  ℂcc 9934  ℝcr 9935  0cc0 9936  1c1 9937   + caddc 9939   · cmul 9941   ≤ cle 10075   − cmin 10266  -cneg 10267  2c2 11070  ...cfz 12326  ↑cexp 12860  𝔼cee 25768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-n0 11293  df-z 11378  df-uz 11688  df-seq 12802  df-exp 12861  df-ee 25771

This theorem is referenced by:  colinearalg  25790