colinearalglem4

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

		Ref	Expression
	Assertion	colinearalglem4	$⊢ ((A \in 𝔼 (N) \land C \in 𝔼 (N)) \land K \in ℝ) \to (\forall i \in (1 \dots N) (K (C (i) - A (i)) + A (i) - A (i)) (C (i) - A (i)) \leq 0 \lor \forall i \in (1 \dots N) (C (i) - (K (C (i) - A (i)) + A (i))) (A (i) - (K (C (i) - A (i)) + A (i))) \leq 0 \lor \forall i \in (1 \dots N) (A (i) - C (i)) (K (C (i) - A (i)) + A (i) - C (i)) \leq 0)$

Proof

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

Metamath Proof Explorer

Theorem colinearalglem4

Proof