brbtwn2

Description: Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013)

		Ref	Expression
	Assertion	brbtwn2	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (A Btwn ⟨B, C⟩ \leftrightarrow (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))))$

Proof

Step	Hyp	Ref	Expression
1		brbtwn	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (A Btwn ⟨B, C⟩ \leftrightarrow \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k))$
2		fveere	$⊢ (B \in 𝔼 (N) \land i \in (1 \dots N)) \to B (i) \in ℝ$
3	2	3ad2antl2	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land i \in (1 \dots N)) \to B (i) \in ℝ$
4		fveere	$⊢ (C \in 𝔼 (N) \land i \in (1 \dots N)) \to C (i) \in ℝ$
5	4	3ad2antl3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land i \in (1 \dots N)) \to C (i) \in ℝ$
6	3 5	jca	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land i \in (1 \dots N)) \to (B (i) \in ℝ \land C (i) \in ℝ)$
7		resubcl	$⊢ (B (i) \in ℝ \land C (i) \in ℝ) \to B (i) - C (i) \in ℝ$
8	7	3adant3	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to B (i) - C (i) \in ℝ$
9	8	recnd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to B (i) - C (i) \in ℂ$
10	9	sqvald	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to {(B (i) - C (i))}^{2} = (B (i) - C (i)) (B (i) - C (i))$
11	10	oveq2d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (- (1 - t)) {(B (i) - C (i))}^{2} = t (- (1 - t)) (B (i) - C (i)) (B (i) - C (i))$
12		elicc01	$⊢ t \in [0, 1] \leftrightarrow (t \in ℝ \land 0 \leq t \land t \leq 1)$
13	12	simp1bi	$⊢ t \in [0, 1] \to t \in ℝ$
14	13	recnd	$⊢ t \in [0, 1] \to t \in ℂ$
15	14	3ad2ant3	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t \in ℂ$
16		1re	$⊢ 1 \in ℝ$
17		resubcl	$⊢ (1 \in ℝ \land t \in ℝ) \to 1 - t \in ℝ$
18	16 13 17	sylancr	$⊢ t \in [0, 1] \to 1 - t \in ℝ$
19	18	3ad2ant3	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 1 - t \in ℝ$
20	19	recnd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 1 - t \in ℂ$
21	20	negcld	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to - (1 - t) \in ℂ$
22	15 9 21 9	mul4d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (B (i) - C (i)) (- (1 - t)) (B (i) - C (i)) = t (- (1 - t)) (B (i) - C (i)) (B (i) - C (i))$
23		recn	$⊢ B (i) \in ℝ \to B (i) \in ℂ$
24	23	3ad2ant1	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to B (i) \in ℂ$
25		recn	$⊢ C (i) \in ℝ \to C (i) \in ℂ$
26	25	3ad2ant2	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to C (i) \in ℂ$
27	15 24 26	subdid	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (B (i) - C (i)) = t B (i) - t C (i)$
28		ax-1cn	$⊢ 1 \in ℂ$
29		subdir	$⊢ (1 \in ℂ \land 1 - t \in ℂ \land B (i) \in ℂ) \to (1 - (1 - t)) B (i) = 1 B (i) - (1 - t) B (i)$
30	28 20 24 29	mp3an2i	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - (1 - t)) B (i) = 1 B (i) - (1 - t) B (i)$
31		nncan	$⊢ (1 \in ℂ \land t \in ℂ) \to 1 - (1 - t) = t$
32	28 15 31	sylancr	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 1 - (1 - t) = t$
33	32	oveq1d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - (1 - t)) B (i) = t B (i)$
34	24	mulid2d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 1 B (i) = B (i)$
35	34	oveq1d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 1 B (i) - (1 - t) B (i) = B (i) - (1 - t) B (i)$
36	30 33 35	3eqtr3d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t B (i) = B (i) - (1 - t) B (i)$
37	36	oveq1d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t B (i) - t C (i) = B (i) - (1 - t) B (i) - t C (i)$
38		simp1	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to B (i) \in ℝ$
39	19 38	remulcld	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) B (i) \in ℝ$
40	39	recnd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) B (i) \in ℂ$
41	13	3ad2ant3	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t \in ℝ$
42		simp2	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to C (i) \in ℝ$
43	41 42	remulcld	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t C (i) \in ℝ$
44	43	recnd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t C (i) \in ℂ$
45	24 40 44	subsub4d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to B (i) - (1 - t) B (i) - t C (i) = B (i) - ((1 - t) B (i) + t C (i))$
46	27 37 45	3eqtrd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (B (i) - C (i)) = B (i) - ((1 - t) B (i) + t C (i))$
47	20 9	mulneg1d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (- (1 - t)) (B (i) - C (i)) = - (1 - t) (B (i) - C (i))$
48	20 24 26	subdid	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) (B (i) - C (i)) = (1 - t) B (i) - (1 - t) C (i)$
49		subdir	$⊢ (1 \in ℂ \land t \in ℂ \land C (i) \in ℂ) \to (1 - t) C (i) = 1 C (i) - t C (i)$
50	28 15 26 49	mp3an2i	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) C (i) = 1 C (i) - t C (i)$
51	26	mulid2d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 1 C (i) = C (i)$
52	51	oveq1d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 1 C (i) - t C (i) = C (i) - t C (i)$
53	50 52	eqtrd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) C (i) = C (i) - t C (i)$
54	53	oveq2d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) B (i) - (1 - t) C (i) = (1 - t) B (i) - (C (i) - t C (i))$
55	40 26 44	subsub3d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) B (i) - (C (i) - t C (i)) = (1 - t) B (i) + t C (i) - C (i)$
56	48 54 55	3eqtrd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) (B (i) - C (i)) = (1 - t) B (i) + t C (i) - C (i)$
57	56	negeqd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to - (1 - t) (B (i) - C (i)) = - ((1 - t) B (i) + t C (i) - C (i))$
58	39 43	readdcld	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) B (i) + t C (i) \in ℝ$
59	58	recnd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (1 - t) B (i) + t C (i) \in ℂ$
60	59 26	negsubdi2d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to - ((1 - t) B (i) + t C (i) - C (i)) = C (i) - ((1 - t) B (i) + t C (i))$
61	47 57 60	3eqtrd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (- (1 - t)) (B (i) - C (i)) = C (i) - ((1 - t) B (i) + t C (i))$
62	46 61	oveq12d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (B (i) - C (i)) (- (1 - t)) (B (i) - C (i)) = (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i)))$
63	11 22 62	3eqtr2rd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) = t (- (1 - t)) {(B (i) - C (i))}^{2}$
64	15 20	mulneg2d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (- (1 - t)) = - t (1 - t)$
65	64	oveq1d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (- (1 - t)) {(B (i) - C (i))}^{2} = (- t (1 - t)) {(B (i) - C (i))}^{2}$
66	41 19	remulcld	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (1 - t) \in ℝ$
67	66	recnd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (1 - t) \in ℂ$
68	8	resqcld	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to {(B (i) - C (i))}^{2} \in ℝ$
69	68	recnd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to {(B (i) - C (i))}^{2} \in ℂ$
70	67 69	mulneg1d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (- t (1 - t)) {(B (i) - C (i))}^{2} = - t (1 - t) {(B (i) - C (i))}^{2}$
71	65 70	eqtrd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (- (1 - t)) {(B (i) - C (i))}^{2} = - t (1 - t) {(B (i) - C (i))}^{2}$
72	12	simp2bi	$⊢ t \in [0, 1] \to 0 \leq t$
73	12	simp3bi	$⊢ t \in [0, 1] \to t \leq 1$
74		subge0	$⊢ (1 \in ℝ \land t \in ℝ) \to (0 \leq 1 - t \leftrightarrow t \leq 1)$
75	16 13 74	sylancr	$⊢ t \in [0, 1] \to (0 \leq 1 - t \leftrightarrow t \leq 1)$
76	73 75	mpbird	$⊢ t \in [0, 1] \to 0 \leq 1 - t$
77	13 18 72 76	mulge0d	$⊢ t \in [0, 1] \to 0 \leq t (1 - t)$
78	77	3ad2ant3	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 0 \leq t (1 - t)$
79	8	sqge0d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 0 \leq {(B (i) - C (i))}^{2}$
80	66 68 78 79	mulge0d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to 0 \leq t (1 - t) {(B (i) - C (i))}^{2}$
81	66 68	remulcld	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (1 - t) {(B (i) - C (i))}^{2} \in ℝ$
82	81	le0neg2d	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (0 \leq t (1 - t) {(B (i) - C (i))}^{2} \leftrightarrow - t (1 - t) {(B (i) - C (i))}^{2} \leq 0)$
83	80 82	mpbid	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to - t (1 - t) {(B (i) - C (i))}^{2} \leq 0$
84	71 83	eqbrtrd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to t (- (1 - t)) {(B (i) - C (i))}^{2} \leq 0$
85	63 84	eqbrtrd	$⊢ (B (i) \in ℝ \land C (i) \in ℝ \land t \in [0, 1]) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0$
86	85	3expa	$⊢ ((B (i) \in ℝ \land C (i) \in ℝ) \land t \in [0, 1]) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0$
87	6 86	sylan	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land i \in (1 \dots N)) \land t \in [0, 1]) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0$
88	87	an32s	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land t \in [0, 1]) \land i \in (1 \dots N)) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0$
89	88	ralrimiva	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land t \in [0, 1]) \to \forall i \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0$
90		fveecn	$⊢ (B \in 𝔼 (N) \land i \in (1 \dots N)) \to B (i) \in ℂ$
91		fveecn	$⊢ (C \in 𝔼 (N) \land i \in (1 \dots N)) \to C (i) \in ℂ$
92	90 91	anim12i	$⊢ ((B \in 𝔼 (N) \land i \in (1 \dots N)) \land (C \in 𝔼 (N) \land i \in (1 \dots N))) \to (B (i) \in ℂ \land C (i) \in ℂ)$
93	92	anandirs	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N)) \land i \in (1 \dots N)) \to (B (i) \in ℂ \land C (i) \in ℂ)$
94		fveecn	$⊢ (B \in 𝔼 (N) \land j \in (1 \dots N)) \to B (j) \in ℂ$
95		fveecn	$⊢ (C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℂ$
96	94 95	anim12i	$⊢ ((B \in 𝔼 (N) \land j \in (1 \dots N)) \land (C \in 𝔼 (N) \land j \in (1 \dots N))) \to (B (j) \in ℂ \land C (j) \in ℂ)$
97	96	anandirs	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to (B (j) \in ℂ \land C (j) \in ℂ)$
98	93 97	anim12dan	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (i \in (1 \dots N) \land j \in (1 \dots N))) \to ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ))$
99	98	3adantl1	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (i \in (1 \dots N) \land j \in (1 \dots N))) \to ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ))$
100		subcl	$⊢ (B (i) \in ℂ \land C (i) \in ℂ) \to B (i) - C (i) \in ℂ$
101	100	3ad2ant1	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (i) - C (i) \in ℂ$
102		subcl	$⊢ (C (j) \in ℂ \land B (j) \in ℂ) \to C (j) - B (j) \in ℂ$
103	102	ancoms	$⊢ (B (j) \in ℂ \land C (j) \in ℂ) \to C (j) - B (j) \in ℂ$
104	103	3ad2ant2	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (j) - B (j) \in ℂ$
105	101 104	mulcomd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (B (i) - C (i)) (C (j) - B (j)) = (C (j) - B (j)) (B (i) - C (i))$
106		simp2r	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (j) \in ℂ$
107		simp2l	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (j) \in ℂ$
108		simp1l	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (i) \in ℂ$
109		simp1r	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (i) \in ℂ$
110		mulsub2	$⊢ ((C (j) \in ℂ \land B (j) \in ℂ) \land (B (i) \in ℂ \land C (i) \in ℂ)) \to (C (j) - B (j)) (B (i) - C (i)) = (B (j) - C (j)) (C (i) - B (i))$
111	106 107 108 109 110	syl22anc	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (C (j) - B (j)) (B (i) - C (i)) = (B (j) - C (j)) (C (i) - B (i))$
112	105 111	eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (B (i) - C (i)) (C (j) - B (j)) = (B (j) - C (j)) (C (i) - B (i))$
113	112	oveq2d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (1 - t) (B (i) - C (i)) (C (j) - B (j)) = t (1 - t) (B (j) - C (j)) (C (i) - B (i))$
114		simp3	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t \in ℂ$
115		subcl	$⊢ (1 \in ℂ \land t \in ℂ) \to 1 - t \in ℂ$
116	28 115	mpan	$⊢ t \in ℂ \to 1 - t \in ℂ$
117	116	3ad2ant3	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 - t \in ℂ$
118	114 117 101 104	mul4d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (1 - t) (B (i) - C (i)) (C (j) - B (j)) = t (B (i) - C (i)) (1 - t) (C (j) - B (j))$
119	114 108 109	subdid	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (B (i) - C (i)) = t B (i) - t C (i)$
120	28 117 108 29	mp3an2i	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - (1 - t)) B (i) = 1 B (i) - (1 - t) B (i)$
121	28 31	mpan	$⊢ t \in ℂ \to 1 - (1 - t) = t$
122	121	3ad2ant3	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 - (1 - t) = t$
123	122	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - (1 - t)) B (i) = t B (i)$
124	108	mulid2d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 B (i) = B (i)$
125	124	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 B (i) - (1 - t) B (i) = B (i) - (1 - t) B (i)$
126	120 123 125	3eqtr3d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t B (i) = B (i) - (1 - t) B (i)$
127	126	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t B (i) - t C (i) = B (i) - (1 - t) B (i) - t C (i)$
128	117 108	mulcld	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) B (i) \in ℂ$
129	114 109	mulcld	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t C (i) \in ℂ$
130	108 128 129	subsub4d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (i) - (1 - t) B (i) - t C (i) = B (i) - ((1 - t) B (i) + t C (i))$
131	119 127 130	3eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (B (i) - C (i)) = B (i) - ((1 - t) B (i) + t C (i))$
132	117 106 107	subdid	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) (C (j) - B (j)) = (1 - t) C (j) - (1 - t) B (j)$
133		subdir	$⊢ (1 \in ℂ \land t \in ℂ \land C (j) \in ℂ) \to (1 - t) C (j) = 1 C (j) - t C (j)$
134	28 114 106 133	mp3an2i	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) C (j) = 1 C (j) - t C (j)$
135	106	mulid2d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 C (j) = C (j)$
136	135	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 C (j) - t C (j) = C (j) - t C (j)$
137	134 136	eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) C (j) = C (j) - t C (j)$
138	137	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) C (j) - (1 - t) B (j) = C (j) - t C (j) - (1 - t) B (j)$
139	132 138	eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) (C (j) - B (j)) = C (j) - t C (j) - (1 - t) B (j)$
140	114 106	mulcld	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t C (j) \in ℂ$
141	117 107	mulcld	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) B (j) \in ℂ$
142	106 140 141	sub32d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (j) - t C (j) - (1 - t) B (j) = C (j) - (1 - t) B (j) - t C (j)$
143	106 141 140	subsub4d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (j) - (1 - t) B (j) - t C (j) = C (j) - ((1 - t) B (j) + t C (j))$
144	139 142 143	3eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) (C (j) - B (j)) = C (j) - ((1 - t) B (j) + t C (j))$
145	131 144	oveq12d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (B (i) - C (i)) (1 - t) (C (j) - B (j)) = (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j)))$
146	118 145	eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (1 - t) (B (i) - C (i)) (C (j) - B (j)) = (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j)))$
147		subcl	$⊢ (B (j) \in ℂ \land C (j) \in ℂ) \to B (j) - C (j) \in ℂ$
148	147	3ad2ant2	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (j) - C (j) \in ℂ$
149		subcl	$⊢ (C (i) \in ℂ \land B (i) \in ℂ) \to C (i) - B (i) \in ℂ$
150	149	ancoms	$⊢ (B (i) \in ℂ \land C (i) \in ℂ) \to C (i) - B (i) \in ℂ$
151	150	3ad2ant1	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (i) - B (i) \in ℂ$
152	114 117 148 151	mul4d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (1 - t) (B (j) - C (j)) (C (i) - B (i)) = t (B (j) - C (j)) (1 - t) (C (i) - B (i))$
153	114 107 106	subdid	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (B (j) - C (j)) = t B (j) - t C (j)$
154		subdir	$⊢ (1 \in ℂ \land 1 - t \in ℂ \land B (j) \in ℂ) \to (1 - (1 - t)) B (j) = 1 B (j) - (1 - t) B (j)$
155	28 117 107 154	mp3an2i	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - (1 - t)) B (j) = 1 B (j) - (1 - t) B (j)$
156	122	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - (1 - t)) B (j) = t B (j)$
157	107	mulid2d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 B (j) = B (j)$
158	157	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 B (j) - (1 - t) B (j) = B (j) - (1 - t) B (j)$
159	155 156 158	3eqtr3rd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (j) - (1 - t) B (j) = t B (j)$
160	159	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (j) - (1 - t) B (j) - t C (j) = t B (j) - t C (j)$
161	107 141 140	subsub4d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to B (j) - (1 - t) B (j) - t C (j) = B (j) - ((1 - t) B (j) + t C (j))$
162	153 160 161	3eqtr2d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (B (j) - C (j)) = B (j) - ((1 - t) B (j) + t C (j))$
163	117 109 108	subdid	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) (C (i) - B (i)) = (1 - t) C (i) - (1 - t) B (i)$
164	28 114 109 49	mp3an2i	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) C (i) = 1 C (i) - t C (i)$
165	109	mulid2d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 C (i) = C (i)$
166	165	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to 1 C (i) - t C (i) = C (i) - t C (i)$
167	164 166	eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) C (i) = C (i) - t C (i)$
168	167	oveq1d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) C (i) - (1 - t) B (i) = C (i) - t C (i) - (1 - t) B (i)$
169	109 129 128	sub32d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (i) - t C (i) - (1 - t) B (i) = C (i) - (1 - t) B (i) - t C (i)$
170	109 128 129	subsub4d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (i) - (1 - t) B (i) - t C (i) = C (i) - ((1 - t) B (i) + t C (i))$
171	169 170	eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to C (i) - t C (i) - (1 - t) B (i) = C (i) - ((1 - t) B (i) + t C (i))$
172	163 168 171	3eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (1 - t) (C (i) - B (i)) = C (i) - ((1 - t) B (i) + t C (i))$
173	162 172	oveq12d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (B (j) - C (j)) (1 - t) (C (i) - B (i)) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
174	152 173	eqtrd	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to t (1 - t) (B (j) - C (j)) (C (i) - B (i)) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
175	113 146 174	3eqtr3d	$⊢ ((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ) \land t \in ℂ) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
176	175	3expa	$⊢ (((B (i) \in ℂ \land C (i) \in ℂ) \land (B (j) \in ℂ \land C (j) \in ℂ)) \land t \in ℂ) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
177	99 14 176	syl2an	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (i \in (1 \dots N) \land j \in (1 \dots N))) \land t \in [0, 1]) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
178	177	an32s	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land t \in [0, 1]) \land (i \in (1 \dots N) \land j \in (1 \dots N))) \to (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
179	178	ralrimivva	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land t \in [0, 1]) \to \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
180		fveq2	$⊢ k = i \to A (k) = A (i)$
181		fveq2	$⊢ k = i \to B (k) = B (i)$
182	181	oveq2d	$⊢ k = i \to (1 - t) B (k) = (1 - t) B (i)$
183		fveq2	$⊢ k = i \to C (k) = C (i)$
184	183	oveq2d	$⊢ k = i \to t C (k) = t C (i)$
185	182 184	oveq12d	$⊢ k = i \to (1 - t) B (k) + t C (k) = (1 - t) B (i) + t C (i)$
186	180 185	eqeq12d	$⊢ k = i \to (A (k) = (1 - t) B (k) + t C (k) \leftrightarrow A (i) = (1 - t) B (i) + t C (i))$
187	186	rspccva	$⊢ (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \land i \in (1 \dots N)) \to A (i) = (1 - t) B (i) + t C (i)$
188		oveq2	$⊢ A (i) = (1 - t) B (i) + t C (i) \to B (i) - A (i) = B (i) - ((1 - t) B (i) + t C (i))$
189		oveq2	$⊢ A (i) = (1 - t) B (i) + t C (i) \to C (i) - A (i) = C (i) - ((1 - t) B (i) + t C (i))$
190	188 189	oveq12d	$⊢ A (i) = (1 - t) B (i) + t C (i) \to (B (i) - A (i)) (C (i) - A (i)) = (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i)))$
191	190	breq1d	$⊢ A (i) = (1 - t) B (i) + t C (i) \to ((B (i) - A (i)) (C (i) - A (i)) \leq 0 \leftrightarrow (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0)$
192	187 191	syl	$⊢ (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \land i \in (1 \dots N)) \to ((B (i) - A (i)) (C (i) - A (i)) \leq 0 \leftrightarrow (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0)$
193	192	ralbidva	$⊢ \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \to (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \leftrightarrow \forall i \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0)$
194		fveq2	$⊢ k = j \to A (k) = A (j)$
195		fveq2	$⊢ k = j \to B (k) = B (j)$
196	195	oveq2d	$⊢ k = j \to (1 - t) B (k) = (1 - t) B (j)$
197		fveq2	$⊢ k = j \to C (k) = C (j)$
198	197	oveq2d	$⊢ k = j \to t C (k) = t C (j)$
199	196 198	oveq12d	$⊢ k = j \to (1 - t) B (k) + t C (k) = (1 - t) B (j) + t C (j)$
200	194 199	eqeq12d	$⊢ k = j \to (A (k) = (1 - t) B (k) + t C (k) \leftrightarrow A (j) = (1 - t) B (j) + t C (j))$
201	200	rspccva	$⊢ (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \land j \in (1 \dots N)) \to A (j) = (1 - t) B (j) + t C (j)$
202		oveq2	$⊢ A (j) = (1 - t) B (j) + t C (j) \to C (j) - A (j) = C (j) - ((1 - t) B (j) + t C (j))$
203	188 202	oveqan12d	$⊢ (A (i) = (1 - t) B (i) + t C (i) \land A (j) = (1 - t) B (j) + t C (j)) \to (B (i) - A (i)) (C (j) - A (j)) = (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j)))$
204		oveq2	$⊢ A (j) = (1 - t) B (j) + t C (j) \to B (j) - A (j) = B (j) - ((1 - t) B (j) + t C (j))$
205	204 189	oveqan12rd	$⊢ (A (i) = (1 - t) B (i) + t C (i) \land A (j) = (1 - t) B (j) + t C (j)) \to (B (j) - A (j)) (C (i) - A (i)) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))$
206	203 205	eqeq12d	$⊢ (A (i) = (1 - t) B (i) + t C (i) \land A (j) = (1 - t) B (j) + t C (j)) \to ((B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \leftrightarrow (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i))))$
207	187 201 206	syl2an	$⊢ ((\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \land i \in (1 \dots N)) \land (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \land j \in (1 \dots N))) \to ((B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \leftrightarrow (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i))))$
208	207	anandis	$⊢ (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \land (i \in (1 \dots N) \land j \in (1 \dots N))) \to ((B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \leftrightarrow (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i))))$
209	208	2ralbidva	$⊢ \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \to (\forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \leftrightarrow \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i))))$
210	193 209	anbi12d	$⊢ \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \to ((\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \leftrightarrow (\forall i \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))))$
211	210	biimprcd	$⊢ (\forall i \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (i) - ((1 - t) B (i) + t C (i))) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - ((1 - t) B (i) + t C (i))) (C (j) - ((1 - t) B (j) + t C (j))) = (B (j) - ((1 - t) B (j) + t C (j))) (C (i) - ((1 - t) B (i) + t C (i)))) \to (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \to (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))))$
212	89 179 211	syl2anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land t \in [0, 1]) \to (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \to (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))))$
213	212	rexlimdva	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (\exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \to (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))))$
214		fveere	$⊢ (A \in 𝔼 (N) \land i \in (1 \dots N)) \to A (i) \in ℝ$
215	214	3ad2antl1	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land i \in (1 \dots N)) \to A (i) \in ℝ$
216		mulsuble0b	$⊢ (B (i) \in ℝ \land A (i) \in ℝ \land C (i) \in ℝ) \to ((B (i) - A (i)) (C (i) - A (i)) \leq 0 \leftrightarrow ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
217	3 215 5 216	syl3anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land i \in (1 \dots N)) \to ((B (i) - A (i)) (C (i) - A (i)) \leq 0 \leftrightarrow ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
218	217	ralbidva	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \leftrightarrow \forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
219	218	anbi1d	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to ((\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \leftrightarrow (\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))))$
220		simpl2	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \to B \in 𝔼 (N)$
221		simpl1	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \to A \in 𝔼 (N)$
222		eqeefv	$⊢ (B \in 𝔼 (N) \land A \in 𝔼 (N)) \to (B = A \leftrightarrow \forall i \in (1 \dots N) B (i) = A (i))$
223	220 221 222	syl2anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \to (B = A \leftrightarrow \forall i \in (1 \dots N) B (i) = A (i))$
224	3	adantlr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \land i \in (1 \dots N)) \to B (i) \in ℝ$
225	215	adantlr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \land i \in (1 \dots N)) \to A (i) \in ℝ$
226	224 225	letri3d	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \land i \in (1 \dots N)) \to (B (i) = A (i) \leftrightarrow (B (i) \leq A (i) \land A (i) \leq B (i)))$
227		pm4.25	$⊢ (B (i) \leq A (i) \land A (i) \leq B (i)) \leftrightarrow ((B (i) \leq A (i) \land A (i) \leq B (i)) \lor (B (i) \leq A (i) \land A (i) \leq B (i)))$
228		fveq1	$⊢ B = C \to B (i) = C (i)$
229	228	breq2d	$⊢ B = C \to (A (i) \leq B (i) \leftrightarrow A (i) \leq C (i))$
230	229	anbi2d	$⊢ B = C \to ((B (i) \leq A (i) \land A (i) \leq B (i)) \leftrightarrow (B (i) \leq A (i) \land A (i) \leq C (i)))$
231	228	breq1d	$⊢ B = C \to (B (i) \leq A (i) \leftrightarrow C (i) \leq A (i))$
232	231	anbi1d	$⊢ B = C \to ((B (i) \leq A (i) \land A (i) \leq B (i)) \leftrightarrow (C (i) \leq A (i) \land A (i) \leq B (i)))$
233	230 232	orbi12d	$⊢ B = C \to (((B (i) \leq A (i) \land A (i) \leq B (i)) \lor (B (i) \leq A (i) \land A (i) \leq B (i))) \leftrightarrow ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
234	233	ad2antlr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \land i \in (1 \dots N)) \to (((B (i) \leq A (i) \land A (i) \leq B (i)) \lor (B (i) \leq A (i) \land A (i) \leq B (i))) \leftrightarrow ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
235	227 234	syl5bb	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \land i \in (1 \dots N)) \to ((B (i) \leq A (i) \land A (i) \leq B (i)) \leftrightarrow ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
236	226 235	bitrd	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \land i \in (1 \dots N)) \to (B (i) = A (i) \leftrightarrow ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
237	236	ralbidva	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \to (\forall i \in (1 \dots N) B (i) = A (i) \leftrightarrow \forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
238	223 237	bitrd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \to (B = A \leftrightarrow \forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))))$
239	238	biimprd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \to (\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \to B = A)$
240	239	adantrd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land B = C) \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to B = A)$
241	240	ex	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B = C \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to B = A))$
242		0elunit	$⊢ 0 \in [0, 1]$
243		fveecn	$⊢ (A \in 𝔼 (N) \land k \in (1 \dots N)) \to A (k) \in ℂ$
244	243	3ad2antl1	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land k \in (1 \dots N)) \to A (k) \in ℂ$
245		fveecn	$⊢ (B \in 𝔼 (N) \land k \in (1 \dots N)) \to B (k) \in ℂ$
246	245	3ad2antl2	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land k \in (1 \dots N)) \to B (k) \in ℂ$
247		fveecn	$⊢ (C \in 𝔼 (N) \land k \in (1 \dots N)) \to C (k) \in ℂ$
248	247	3ad2antl3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land k \in (1 \dots N)) \to C (k) \in ℂ$
249	244 246 248	3jca	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land k \in (1 \dots N)) \to (A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ)$
250		mulid2	$⊢ B (k) \in ℂ \to 1 B (k) = B (k)$
251		mul02	$⊢ C (k) \in ℂ \to 0 \cdot C (k) = 0$
252	250 251	oveqan12d	$⊢ (B (k) \in ℂ \land C (k) \in ℂ) \to 1 B (k) + 0 \cdot C (k) = B (k) + 0$
253		addid1	$⊢ B (k) \in ℂ \to B (k) + 0 = B (k)$
254	253	adantr	$⊢ (B (k) \in ℂ \land C (k) \in ℂ) \to B (k) + 0 = B (k)$
255	252 254	eqtrd	$⊢ (B (k) \in ℂ \land C (k) \in ℂ) \to 1 B (k) + 0 \cdot C (k) = B (k)$
256	255	3adant1	$⊢ (A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \to 1 B (k) + 0 \cdot C (k) = B (k)$
257	256	adantr	$⊢ ((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (B = C \land B = A)) \to 1 B (k) + 0 \cdot C (k) = B (k)$
258		fveq1	$⊢ B = A \to B (k) = A (k)$
259	258	ad2antll	$⊢ ((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (B = C \land B = A)) \to B (k) = A (k)$
260	257 259	eqtr2d	$⊢ ((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (B = C \land B = A)) \to A (k) = 1 B (k) + 0 \cdot C (k)$
261	249 260	sylan	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land k \in (1 \dots N)) \land (B = C \land B = A)) \to A (k) = 1 B (k) + 0 \cdot C (k)$
262	261	an32s	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (B = C \land B = A)) \land k \in (1 \dots N)) \to A (k) = 1 B (k) + 0 \cdot C (k)$
263	262	ralrimiva	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (B = C \land B = A)) \to \forall k \in (1 \dots N) A (k) = 1 B (k) + 0 \cdot C (k)$
264		oveq2	$⊢ t = 0 \to 1 - t = 1 - 0$
265		1m0e1	$⊢ 1 - 0 = 1$
266	264 265	eqtrdi	$⊢ t = 0 \to 1 - t = 1$
267	266	oveq1d	$⊢ t = 0 \to (1 - t) B (k) = 1 B (k)$
268		oveq1	$⊢ t = 0 \to t C (k) = 0 \cdot C (k)$
269	267 268	oveq12d	$⊢ t = 0 \to (1 - t) B (k) + t C (k) = 1 B (k) + 0 \cdot C (k)$
270	269	eqeq2d	$⊢ t = 0 \to (A (k) = (1 - t) B (k) + t C (k) \leftrightarrow A (k) = 1 B (k) + 0 \cdot C (k))$
271	270	ralbidv	$⊢ t = 0 \to (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \leftrightarrow \forall k \in (1 \dots N) A (k) = 1 B (k) + 0 \cdot C (k))$
272	271	rspcev	$⊢ (0 \in [0, 1] \land \forall k \in (1 \dots N) A (k) = 1 B (k) + 0 \cdot C (k)) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k)$
273	242 263 272	sylancr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (B = C \land B = A)) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k)$
274	273	exp32	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B = C \to (B = A \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k)))$
275	241 274	syldd	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B = C \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k)))$
276		eqeefv	$⊢ (B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B = C \leftrightarrow \forall p \in (1 \dots N) B (p) = C (p))$
277	276	3adant1	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B = C \leftrightarrow \forall p \in (1 \dots N) B (p) = C (p))$
278	277	necon3abid	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B \neq C \leftrightarrow \neg \forall p \in (1 \dots N) B (p) = C (p))$
279		df-ne	$⊢ B (p) \neq C (p) \leftrightarrow \neg B (p) = C (p)$
280	279	rexbii	$⊢ \exists p \in (1 \dots N) B (p) \neq C (p) \leftrightarrow \exists p \in (1 \dots N) \neg B (p) = C (p)$
281		rexnal	$⊢ \exists p \in (1 \dots N) \neg B (p) = C (p) \leftrightarrow \neg \forall p \in (1 \dots N) B (p) = C (p)$
282	280 281	bitri	$⊢ \exists p \in (1 \dots N) B (p) \neq C (p) \leftrightarrow \neg \forall p \in (1 \dots N) B (p) = C (p)$
283	278 282	bitr4di	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B \neq C \leftrightarrow \exists p \in (1 \dots N) B (p) \neq C (p))$
284		fveq2	$⊢ i = p \to B (i) = B (p)$
285		fveq2	$⊢ i = p \to A (i) = A (p)$
286	284 285	breq12d	$⊢ i = p \to (B (i) \leq A (i) \leftrightarrow B (p) \leq A (p))$
287		fveq2	$⊢ i = p \to C (i) = C (p)$
288	285 287	breq12d	$⊢ i = p \to (A (i) \leq C (i) \leftrightarrow A (p) \leq C (p))$
289	286 288	anbi12d	$⊢ i = p \to ((B (i) \leq A (i) \land A (i) \leq C (i)) \leftrightarrow (B (p) \leq A (p) \land A (p) \leq C (p)))$
290	287 285	breq12d	$⊢ i = p \to (C (i) \leq A (i) \leftrightarrow C (p) \leq A (p))$
291	285 284	breq12d	$⊢ i = p \to (A (i) \leq B (i) \leftrightarrow A (p) \leq B (p))$
292	290 291	anbi12d	$⊢ i = p \to ((C (i) \leq A (i) \land A (i) \leq B (i)) \leftrightarrow (C (p) \leq A (p) \land A (p) \leq B (p)))$
293	289 292	orbi12d	$⊢ i = p \to (((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \leftrightarrow ((B (p) \leq A (p) \land A (p) \leq C (p)) \lor (C (p) \leq A (p) \land A (p) \leq B (p))))$
294	293	rspcv	$⊢ p \in (1 \dots N) \to (\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \to ((B (p) \leq A (p) \land A (p) \leq C (p)) \lor (C (p) \leq A (p) \land A (p) \leq B (p))))$
295	294	ad2antrl	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \to ((B (p) \leq A (p) \land A (p) \leq C (p)) \lor (C (p) \leq A (p) \land A (p) \leq B (p))))$
296		simprr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to A (p) \leq C (p)$
297		simp1	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to A \in 𝔼 (N)$
298		simpl	$⊢ (p \in (1 \dots N) \land B (p) \neq C (p)) \to p \in (1 \dots N)$
299		fveere	$⊢ (A \in 𝔼 (N) \land p \in (1 \dots N)) \to A (p) \in ℝ$
300	297 298 299	syl2an	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to A (p) \in ℝ$
301		simp3	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to C \in 𝔼 (N)$
302		fveere	$⊢ (C \in 𝔼 (N) \land p \in (1 \dots N)) \to C (p) \in ℝ$
303	301 298 302	syl2an	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to C (p) \in ℝ$
304		simpl2	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to B \in 𝔼 (N)$
305		simprl	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to p \in (1 \dots N)$
306		fveere	$⊢ (B \in 𝔼 (N) \land p \in (1 \dots N)) \to B (p) \in ℝ$
307	304 305 306	syl2anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to B (p) \in ℝ$
308	300 303 307	lesub1d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (A (p) \leq C (p) \leftrightarrow A (p) - B (p) \leq C (p) - B (p))$
309	308	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to (A (p) \leq C (p) \leftrightarrow A (p) - B (p) \leq C (p) - B (p))$
310	296 309	mpbid	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to A (p) - B (p) \leq C (p) - B (p)$
311	300 307	resubcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to A (p) - B (p) \in ℝ$
312	311	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to A (p) - B (p) \in ℝ$
313		simprl	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to B (p) \leq A (p)$
314	300 307	subge0d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (0 \leq A (p) - B (p) \leftrightarrow B (p) \leq A (p))$
315	314	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to (0 \leq A (p) - B (p) \leftrightarrow B (p) \leq A (p))$
316	313 315	mpbird	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to 0 \leq A (p) - B (p)$
317	303 307	resubcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to C (p) - B (p) \in ℝ$
318	317	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to C (p) - B (p) \in ℝ$
319		letr	$⊢ (B (p) \in ℝ \land A (p) \in ℝ \land C (p) \in ℝ) \to ((B (p) \leq A (p) \land A (p) \leq C (p)) \to B (p) \leq C (p))$
320	307 300 303 319	syl3anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to ((B (p) \leq A (p) \land A (p) \leq C (p)) \to B (p) \leq C (p))$
321	320	imp	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to B (p) \leq C (p)$
322		simplrr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to B (p) \neq C (p)$
323	322	necomd	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to C (p) \neq B (p)$
324	307 303	ltlend	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (B (p) < C (p) \leftrightarrow (B (p) \leq C (p) \land C (p) \neq B (p)))$
325	324	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to (B (p) < C (p) \leftrightarrow (B (p) \leq C (p) \land C (p) \neq B (p)))$
326	321 323 325	mpbir2and	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to B (p) < C (p)$
327	307 303	posdifd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (B (p) < C (p) \leftrightarrow 0 < C (p) - B (p))$
328	327	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to (B (p) < C (p) \leftrightarrow 0 < C (p) - B (p))$
329	326 328	mpbid	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to 0 < C (p) - B (p)$
330		divelunit	$⊢ ((A (p) - B (p) \in ℝ \land 0 \leq A (p) - B (p)) \land (C (p) - B (p) \in ℝ \land 0 < C (p) - B (p))) \to (\frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1] \leftrightarrow A (p) - B (p) \leq C (p) - B (p))$
331	312 316 318 329 330	syl22anc	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to (\frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1] \leftrightarrow A (p) - B (p) \leq C (p) - B (p))$
332	310 331	mpbird	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (B (p) \leq A (p) \land A (p) \leq C (p))) \to \frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1]$
333	300	recnd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to A (p) \in ℂ$
334	307	recnd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to B (p) \in ℂ$
335	303	recnd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to C (p) \in ℂ$
336		simprr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to B (p) \neq C (p)$
337	336	necomd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to C (p) \neq B (p)$
338	333 334 335 334 337	div2subd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to \frac{A (p) - B (p)}{C (p) - B (p)} = \frac{B (p) - A (p)}{B (p) - C (p)}$
339	338	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to \frac{A (p) - B (p)}{C (p) - B (p)} = \frac{B (p) - A (p)}{B (p) - C (p)}$
340		simprl	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to C (p) \leq A (p)$
341	303 300 307	lesub2d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (C (p) \leq A (p) \leftrightarrow B (p) - A (p) \leq B (p) - C (p))$
342	341	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to (C (p) \leq A (p) \leftrightarrow B (p) - A (p) \leq B (p) - C (p))$
343	340 342	mpbid	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to B (p) - A (p) \leq B (p) - C (p)$
344	307 300	resubcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to B (p) - A (p) \in ℝ$
345	344	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to B (p) - A (p) \in ℝ$
346		simprr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to A (p) \leq B (p)$
347	307 300	subge0d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (0 \leq B (p) - A (p) \leftrightarrow A (p) \leq B (p))$
348	347	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to (0 \leq B (p) - A (p) \leftrightarrow A (p) \leq B (p))$
349	346 348	mpbird	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to 0 \leq B (p) - A (p)$
350	307 303	resubcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to B (p) - C (p) \in ℝ$
351	350	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to B (p) - C (p) \in ℝ$
352		letr	$⊢ (C (p) \in ℝ \land A (p) \in ℝ \land B (p) \in ℝ) \to ((C (p) \leq A (p) \land A (p) \leq B (p)) \to C (p) \leq B (p))$
353	303 300 307 352	syl3anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to ((C (p) \leq A (p) \land A (p) \leq B (p)) \to C (p) \leq B (p))$
354	353	imp	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to C (p) \leq B (p)$
355		simplrr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to B (p) \neq C (p)$
356	303 307	ltlend	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (C (p) < B (p) \leftrightarrow (C (p) \leq B (p) \land B (p) \neq C (p)))$
357	356	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to (C (p) < B (p) \leftrightarrow (C (p) \leq B (p) \land B (p) \neq C (p)))$
358	354 355 357	mpbir2and	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to C (p) < B (p)$
359	303 307	posdifd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (C (p) < B (p) \leftrightarrow 0 < B (p) - C (p))$
360	359	adantr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to (C (p) < B (p) \leftrightarrow 0 < B (p) - C (p))$
361	358 360	mpbid	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to 0 < B (p) - C (p)$
362		divelunit	$⊢ ((B (p) - A (p) \in ℝ \land 0 \leq B (p) - A (p)) \land (B (p) - C (p) \in ℝ \land 0 < B (p) - C (p))) \to (\frac{B (p) - A (p)}{B (p) - C (p)} \in [0, 1] \leftrightarrow B (p) - A (p) \leq B (p) - C (p))$
363	345 349 351 361 362	syl22anc	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to (\frac{B (p) - A (p)}{B (p) - C (p)} \in [0, 1] \leftrightarrow B (p) - A (p) \leq B (p) - C (p))$
364	343 363	mpbird	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to \frac{B (p) - A (p)}{B (p) - C (p)} \in [0, 1]$
365	339 364	eqeltrd	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land (C (p) \leq A (p) \land A (p) \leq B (p))) \to \frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1]$
366	332 365	jaodan	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \land ((B (p) \leq A (p) \land A (p) \leq C (p)) \lor (C (p) \leq A (p) \land A (p) \leq B (p)))) \to \frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1]$
367	366	ex	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (((B (p) \leq A (p) \land A (p) \leq C (p)) \lor (C (p) \leq A (p) \land A (p) \leq B (p))) \to \frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1])$
368	295 367	syld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \to \frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1])$
369		simp2l	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to p \in (1 \dots N)$
370		simp3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to k \in (1 \dots N)$
371	284 285	oveq12d	$⊢ i = p \to B (i) - A (i) = B (p) - A (p)$
372	371	oveq1d	$⊢ i = p \to (B (i) - A (i)) (C (j) - A (j)) = (B (p) - A (p)) (C (j) - A (j))$
373	287 285	oveq12d	$⊢ i = p \to C (i) - A (i) = C (p) - A (p)$
374	373	oveq2d	$⊢ i = p \to (B (j) - A (j)) (C (i) - A (i)) = (B (j) - A (j)) (C (p) - A (p))$
375	372 374	eqeq12d	$⊢ i = p \to ((B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \leftrightarrow (B (p) - A (p)) (C (j) - A (j)) = (B (j) - A (j)) (C (p) - A (p)))$
376		fveq2	$⊢ j = k \to C (j) = C (k)$
377		fveq2	$⊢ j = k \to A (j) = A (k)$
378	376 377	oveq12d	$⊢ j = k \to C (j) - A (j) = C (k) - A (k)$
379	378	oveq2d	$⊢ j = k \to (B (p) - A (p)) (C (j) - A (j)) = (B (p) - A (p)) (C (k) - A (k))$
380		fveq2	$⊢ j = k \to B (j) = B (k)$
381	380 377	oveq12d	$⊢ j = k \to B (j) - A (j) = B (k) - A (k)$
382	381	oveq1d	$⊢ j = k \to (B (j) - A (j)) (C (p) - A (p)) = (B (k) - A (k)) (C (p) - A (p))$
383	379 382	eqeq12d	$⊢ j = k \to ((B (p) - A (p)) (C (j) - A (j)) = (B (j) - A (j)) (C (p) - A (p)) \leftrightarrow (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p)))$
384	375 383	rspc2v	$⊢ (p \in (1 \dots N) \land k \in (1 \dots N)) \to (\forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \to (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p)))$
385	369 370 384	syl2anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to (\forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \to (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p)))$
386		simp11	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to A \in 𝔼 (N)$
387	386 370 243	syl2anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to A (k) \in ℂ$
388		simp12	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to B \in 𝔼 (N)$
389	388 370 245	syl2anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to B (k) \in ℂ$
390		simp13	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to C \in 𝔼 (N)$
391	390 370 247	syl2anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to C (k) \in ℂ$
392	333	3adant3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to A (p) \in ℂ$
393	334	3adant3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to B (p) \in ℂ$
394	335	3adant3	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to C (p) \in ℂ$
395		simp2r	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to B (p) \neq C (p)$
396	395	necomd	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to C (p) \neq B (p)$
397		simpl23	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (p) \in ℂ$
398		simpl21	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to A (p) \in ℂ$
399	397 398	subcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (p) - A (p) \in ℂ$
400		simpl12	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to B (k) \in ℂ$
401	399 400	mulcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - A (p)) B (k) \in ℂ$
402		simpl22	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to B (p) \in ℂ$
403	398 402	subcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to A (p) - B (p) \in ℂ$
404		simpl13	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (k) \in ℂ$
405	403 404	mulcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (A (p) - B (p)) C (k) \in ℂ$
406	397 402	subcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (p) - B (p) \in ℂ$
407		simpl3	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (p) \neq B (p)$
408	397 402 407	subne0d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (p) - B (p) \neq 0$
409	401 405 406 408	divdird	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{(C (p) - A (p)) B (k) + (A (p) - B (p)) C (k)}{C (p) - B (p)} = (\frac{(C (p) - A (p)) B (k)}{C (p) - B (p)}) + (\frac{(A (p) - B (p)) C (k)}{C (p) - B (p)})$
410		npncan2	$⊢ (B (p) \in ℂ \land A (p) \in ℂ) \to (B (p) - A (p)) + A (p) - B (p) = 0$
411	402 398 410	syl2anc	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) + A (p) - B (p) = 0$
412	411	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to ((B (p) - A (p)) + A (p) - B (p)) C (k) = 0 \cdot C (k)$
413	402 398	subcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to B (p) - A (p) \in ℂ$
414	413 403 404	adddird	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to ((B (p) - A (p)) + A (p) - B (p)) C (k) = (B (p) - A (p)) C (k) + (A (p) - B (p)) C (k)$
415	404	mul02d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to 0 \cdot C (k) = 0$
416	412 414 415	3eqtr3d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (A (p) - B (p)) C (k) = 0$
417	416	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (A (p) - B (p)) C (k) + (C (p) - B (p)) A (k) = 0 + (C (p) - B (p)) A (k)$
418	413 404	mulcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) \in ℂ$
419		simpl11	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to A (k) \in ℂ$
420	406 419	mulcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - B (p)) A (k) \in ℂ$
421	418 405 420	add32d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (A (p) - B (p)) C (k) + (C (p) - B (p)) A (k) = (B (p) - A (p)) C (k) + (C (p) - B (p)) A (k) + (A (p) - B (p)) C (k)$
422	420	addid2d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to 0 + (C (p) - B (p)) A (k) = (C (p) - B (p)) A (k)$
423	417 421 422	3eqtr3rd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - B (p)) A (k) = (B (p) - A (p)) C (k) + (C (p) - B (p)) A (k) + (A (p) - B (p)) C (k)$
424	399 419	mulcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - A (p)) A (k) \in ℂ$
425	413 419	mulcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) A (k) \in ℂ$
426	418 424 425	addsubd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (C (p) - A (p)) A (k) - (B (p) - A (p)) A (k) = (B (p) - A (p)) C (k) - (B (p) - A (p)) A (k) + (C (p) - A (p)) A (k)$
427	397 402 398	nnncan2d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (p) - A (p) - (B (p) - A (p)) = C (p) - B (p)$
428	427	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - A (p) - (B (p) - A (p))) A (k) = (C (p) - B (p)) A (k)$
429	399 413 419	subdird	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - A (p) - (B (p) - A (p))) A (k) = (C (p) - A (p)) A (k) - (B (p) - A (p)) A (k)$
430	428 429	eqtr3d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - B (p)) A (k) = (C (p) - A (p)) A (k) - (B (p) - A (p)) A (k)$
431	430	oveq2d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (C (p) - B (p)) A (k) = (B (p) - A (p)) C (k) + (C (p) - A (p)) A (k) - (B (p) - A (p)) A (k)$
432	418 424 425	addsubassd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (C (p) - A (p)) A (k) - (B (p) - A (p)) A (k) = (B (p) - A (p)) C (k) + (C (p) - A (p)) A (k) - (B (p) - A (p)) A (k)$
433	431 432	eqtr4d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (C (p) - B (p)) A (k) = (B (p) - A (p)) C (k) + (C (p) - A (p)) A (k) - (B (p) - A (p)) A (k)$
434	413 404 419	subdid	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) (C (k) - A (k)) = (B (p) - A (p)) C (k) - (B (p) - A (p)) A (k)$
435	434	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) (C (k) - A (k)) + (C (p) - A (p)) A (k) = (B (p) - A (p)) C (k) - (B (p) - A (p)) A (k) + (C (p) - A (p)) A (k)$
436	426 433 435	3eqtr4d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (C (p) - B (p)) A (k) = (B (p) - A (p)) (C (k) - A (k)) + (C (p) - A (p)) A (k)$
437	436	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) C (k) + (C (p) - B (p)) A (k) + (A (p) - B (p)) C (k) = (B (p) - A (p)) (C (k) - A (k)) + (C (p) - A (p)) A (k) + (A (p) - B (p)) C (k)$
438	423 437	eqtrd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - B (p)) A (k) = (B (p) - A (p)) (C (k) - A (k)) + (C (p) - A (p)) A (k) + (A (p) - B (p)) C (k)$
439		simpr	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))$
440	439	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) (C (k) - A (k)) + (C (p) - A (p)) A (k) = (B (k) - A (k)) (C (p) - A (p)) + (C (p) - A (p)) A (k)$
441	440	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (p) - A (p)) (C (k) - A (k)) + (C (p) - A (p)) A (k) + (A (p) - B (p)) C (k) = (B (k) - A (k)) (C (p) - A (p)) + (C (p) - A (p)) A (k) + (A (p) - B (p)) C (k)$
442	400 419	subcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to B (k) - A (k) \in ℂ$
443	442 399	mulcomd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (k) - A (k)) (C (p) - A (p)) = (C (p) - A (p)) (B (k) - A (k))$
444	443	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (k) - A (k)) (C (p) - A (p)) + (C (p) - A (p)) A (k) = (C (p) - A (p)) (B (k) - A (k)) + (C (p) - A (p)) A (k)$
445	399 442 419	adddid	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - A (p)) (B (k) - A (k) + A (k)) = (C (p) - A (p)) (B (k) - A (k)) + (C (p) - A (p)) A (k)$
446	400 419	npcand	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to B (k) - A (k) + A (k) = B (k)$
447	446	oveq2d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - A (p)) (B (k) - A (k) + A (k)) = (C (p) - A (p)) B (k)$
448	444 445 447	3eqtr2d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (k) - A (k)) (C (p) - A (p)) + (C (p) - A (p)) A (k) = (C (p) - A (p)) B (k)$
449	448	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (B (k) - A (k)) (C (p) - A (p)) + (C (p) - A (p)) A (k) + (A (p) - B (p)) C (k) = (C (p) - A (p)) B (k) + (A (p) - B (p)) C (k)$
450	438 441 449	3eqtrd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - B (p)) A (k) = (C (p) - A (p)) B (k) + (A (p) - B (p)) C (k)$
451	401 405	addcld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (C (p) - A (p)) B (k) + (A (p) - B (p)) C (k) \in ℂ$
452	451 406 419 408	divmuld	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (\frac{(C (p) - A (p)) B (k) + (A (p) - B (p)) C (k)}{C (p) - B (p)} = A (k) \leftrightarrow (C (p) - B (p)) A (k) = (C (p) - A (p)) B (k) + (A (p) - B (p)) C (k))$
453	450 452	mpbird	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{(C (p) - A (p)) B (k) + (A (p) - B (p)) C (k)}{C (p) - B (p)} = A (k)$
454	399 400 406 408	div23d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{(C (p) - A (p)) B (k)}{C (p) - B (p)} = (\frac{C (p) - A (p)}{C (p) - B (p)}) B (k)$
455	406 403 406 408	divsubdird	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{C (p) - B (p) - (A (p) - B (p))}{C (p) - B (p)} = (\frac{C (p) - B (p)}{C (p) - B (p)}) - (\frac{A (p) - B (p)}{C (p) - B (p)})$
456	397 398 402	nnncan2d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to C (p) - B (p) - (A (p) - B (p)) = C (p) - A (p)$
457	456	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{C (p) - B (p) - (A (p) - B (p))}{C (p) - B (p)} = \frac{C (p) - A (p)}{C (p) - B (p)}$
458	406 408	dividd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{C (p) - B (p)}{C (p) - B (p)} = 1$
459	458	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (\frac{C (p) - B (p)}{C (p) - B (p)}) - (\frac{A (p) - B (p)}{C (p) - B (p)}) = 1 - (\frac{A (p) - B (p)}{C (p) - B (p)})$
460	455 457 459	3eqtr3d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{C (p) - A (p)}{C (p) - B (p)} = 1 - (\frac{A (p) - B (p)}{C (p) - B (p)})$
461	460	oveq1d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (\frac{C (p) - A (p)}{C (p) - B (p)}) B (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k)$
462	454 461	eqtrd	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{(C (p) - A (p)) B (k)}{C (p) - B (p)} = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k)$
463	403 404 406 408	div23d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to \frac{(A (p) - B (p)) C (k)}{C (p) - B (p)} = (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)$
464	462 463	oveq12d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to (\frac{(C (p) - A (p)) B (k)}{C (p) - B (p)}) + (\frac{(A (p) - B (p)) C (k)}{C (p) - B (p)}) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)$
465	409 453 464	3eqtr3d	$⊢ (((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \land (B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p))) \to A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)$
466	465	ex	$⊢ ((A (k) \in ℂ \land B (k) \in ℂ \land C (k) \in ℂ) \land (A (p) \in ℂ \land B (p) \in ℂ \land C (p) \in ℂ) \land C (p) \neq B (p)) \to ((B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p)) \to A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k))$
467	387 389 391 392 393 394 396 466	syl331anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to ((B (p) - A (p)) (C (k) - A (k)) = (B (k) - A (k)) (C (p) - A (p)) \to A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k))$
468	385 467	syld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p)) \land k \in (1 \dots N)) \to (\forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \to A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k))$
469	468	3expia	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (k \in (1 \dots N) \to (\forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \to A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)))$
470	469	com23	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (\forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \to (k \in (1 \dots N) \to A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)))$
471	470	ralrimdv	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to (\forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i)) \to \forall k \in (1 \dots N) A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k))$
472	368 471	anim12d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to (\frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1] \land \forall k \in (1 \dots N) A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)))$
473		oveq2	$⊢ t = \frac{A (p) - B (p)}{C (p) - B (p)} \to 1 - t = 1 - (\frac{A (p) - B (p)}{C (p) - B (p)})$
474	473	oveq1d	$⊢ t = \frac{A (p) - B (p)}{C (p) - B (p)} \to (1 - t) B (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k)$
475		oveq1	$⊢ t = \frac{A (p) - B (p)}{C (p) - B (p)} \to t C (k) = (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)$
476	474 475	oveq12d	$⊢ t = \frac{A (p) - B (p)}{C (p) - B (p)} \to (1 - t) B (k) + t C (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)$
477	476	eqeq2d	$⊢ t = \frac{A (p) - B (p)}{C (p) - B (p)} \to (A (k) = (1 - t) B (k) + t C (k) \leftrightarrow A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k))$
478	477	ralbidv	$⊢ t = \frac{A (p) - B (p)}{C (p) - B (p)} \to (\forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \leftrightarrow \forall k \in (1 \dots N) A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k))$
479	478	rspcev	$⊢ (\frac{A (p) - B (p)}{C (p) - B (p)} \in [0, 1] \land \forall k \in (1 \dots N) A (k) = (1 - (\frac{A (p) - B (p)}{C (p) - B (p)})) B (k) + (\frac{A (p) - B (p)}{C (p) - B (p)}) C (k)) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k)$
480	472 479	syl6	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (p \in (1 \dots N) \land B (p) \neq C (p))) \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k))$
481	480	rexlimdvaa	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (\exists p \in (1 \dots N) B (p) \neq C (p) \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k)))$
482	283 481	sylbid	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B \neq C \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k)))$
483	275 482	pm2.61dne	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to ((\forall i \in (1 \dots N) ((B (i) \leq A (i) \land A (i) \leq C (i)) \lor (C (i) \leq A (i) \land A (i) \leq B (i))) \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k))$
484	219 483	sylbid	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to ((\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))) \to \exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k))$
485	213 484	impbid	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (\exists t \in [0, 1] \forall k \in (1 \dots N) A (k) = (1 - t) B (k) + t C (k) \leftrightarrow (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))))$
486	1 485	bitrd	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \to (A Btwn ⟨B, C⟩ \leftrightarrow (\forall i \in (1 \dots N) (B (i) - A (i)) (C (i) - A (i)) \leq 0 \land \forall i \in (1 \dots N) \forall j \in (1 \dots N) (B (i) - A (i)) (C (j) - A (j)) = (B (j) - A (j)) (C (i) - A (i))))$

Metamath Proof Explorer

Theorem brbtwn2

Proof