eenglngeehlnmlem2

		Ref	Expression
	Assertion	eenglngeehlnmlem2	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to (\exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to 0 \in ℝ$
2		1red	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to 1 \in ℝ$
3		simpr	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to t \in ℝ$
4		reorelicc	$⊢ (0 \in ℝ \land 1 \in ℝ \land t \in ℝ) \to (t < 0 \lor t \in [0, 1] \lor 1 < t)$
5	1 2 3 4	syl3anc	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (t < 0 \lor t \in [0, 1] \lor 1 < t)$
6		0xr	$⊢ 0 \in ℝ^{*}$
7	6	a1i	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 0 \in ℝ^{*}$
8		1xr	$⊢ 1 \in ℝ^{*}$
9	8	a1i	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 1 \in ℝ^{*}$
10		simpl	$⊢ (t \in ℝ \land t < 0) \to t \in ℝ$
11	10	recnd	$⊢ (t \in ℝ \land t < 0) \to t \in ℂ$
12		0red	$⊢ (t \in ℝ \land t < 0) \to 0 \in ℝ$
13		1red	$⊢ (t \in ℝ \land t < 0) \to 1 \in ℝ$
14		simpr	$⊢ (t \in ℝ \land t < 0) \to t < 0$
15		0lt1	$⊢ 0 < 1$
16	15	a1i	$⊢ (t \in ℝ \land t < 0) \to 0 < 1$
17	10 12 13 14 16	lttrd	$⊢ (t \in ℝ \land t < 0) \to t < 1$
18	10 17	ltned	$⊢ (t \in ℝ \land t < 0) \to t \neq 1$
19		1subrec1sub	$⊢ (t \in ℂ \land t \neq 1) \to 1 - (\frac{1}{1 - t}) = \frac{t}{t - 1}$
20	11 18 19	syl2anc	$⊢ (t \in ℝ \land t < 0) \to 1 - (\frac{1}{1 - t}) = \frac{t}{t - 1}$
21	10 13	resubcld	$⊢ (t \in ℝ \land t < 0) \to t - 1 \in ℝ$
22		1cnd	$⊢ (t \in ℝ \land t < 0) \to 1 \in ℂ$
23	11 22 18	subne0d	$⊢ (t \in ℝ \land t < 0) \to t - 1 \neq 0$
24	10 21 23	redivcld	$⊢ (t \in ℝ \land t < 0) \to \frac{t}{t - 1} \in ℝ$
25	24	rexrd	$⊢ (t \in ℝ \land t < 0) \to \frac{t}{t - 1} \in ℝ^{*}$
26	20 25	eqeltrd	$⊢ (t \in ℝ \land t < 0) \to 1 - (\frac{1}{1 - t}) \in ℝ^{*}$
27	26	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 1 - (\frac{1}{1 - t}) \in ℝ^{*}$
28	10	renegcld	$⊢ (t \in ℝ \land t < 0) \to - t \in ℝ$
29	10 13	sublt0d	$⊢ (t \in ℝ \land t < 0) \to (t - 1 < 0 \leftrightarrow t < 1)$
30	17 29	mpbird	$⊢ (t \in ℝ \land t < 0) \to t - 1 < 0$
31	21 30	negelrpd	$⊢ (t \in ℝ \land t < 0) \to - (t - 1) \in ℝ^{+}$
32	10 12 14	ltled	$⊢ (t \in ℝ \land t < 0) \to t \leq 0$
33	10	le0neg1d	$⊢ (t \in ℝ \land t < 0) \to (t \leq 0 \leftrightarrow 0 \leq - t)$
34	32 33	mpbid	$⊢ (t \in ℝ \land t < 0) \to 0 \leq - t$
35	28 31 34	divge0d	$⊢ (t \in ℝ \land t < 0) \to 0 \leq \frac{- t}{- (t - 1)}$
36	21	recnd	$⊢ (t \in ℝ \land t < 0) \to t - 1 \in ℂ$
37	11 36 23	div2negd	$⊢ (t \in ℝ \land t < 0) \to \frac{- t}{- (t - 1)} = \frac{t}{t - 1}$
38	20 37	eqtr4d	$⊢ (t \in ℝ \land t < 0) \to 1 - (\frac{1}{1 - t}) = \frac{- t}{- (t - 1)}$
39	35 38	breqtrrd	$⊢ (t \in ℝ \land t < 0) \to 0 \leq 1 - (\frac{1}{1 - t})$
40	39	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 0 \leq 1 - (\frac{1}{1 - t})$
41		1red	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 1 \in ℝ$
42	13 10	resubcld	$⊢ (t \in ℝ \land t < 0) \to 1 - t \in ℝ$
43	10 13	posdifd	$⊢ (t \in ℝ \land t < 0) \to (t < 1 \leftrightarrow 0 < 1 - t)$
44	17 43	mpbid	$⊢ (t \in ℝ \land t < 0) \to 0 < 1 - t$
45	42 44	elrpd	$⊢ (t \in ℝ \land t < 0) \to 1 - t \in ℝ^{+}$
46	45	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 1 - t \in ℝ^{+}$
47	46	rpreccld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to \frac{1}{1 - t} \in ℝ^{+}$
48	41 47	ltsubrpd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 1 - (\frac{1}{1 - t}) < 1$
49	7 9 27 40 48	elicod	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to 1 - (\frac{1}{1 - t}) \in [0, 1)$
50		oveq2	$⊢ l = 1 - (\frac{1}{1 - t}) \to 1 - l = 1 - (1 - (\frac{1}{1 - t}))$
51	50	oveq1d	$⊢ l = 1 - (\frac{1}{1 - t}) \to (1 - l) p (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i)$
52		oveq1	$⊢ l = 1 - (\frac{1}{1 - t}) \to l y (i) = (1 - (\frac{1}{1 - t})) y (i)$
53	51 52	oveq12d	$⊢ l = 1 - (\frac{1}{1 - t}) \to (1 - l) p (i) + l y (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i)$
54	53	eqeq2d	$⊢ l = 1 - (\frac{1}{1 - t}) \to (x (i) = (1 - l) p (i) + l y (i) \leftrightarrow x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i))$
55	54	ralbidv	$⊢ l = 1 - (\frac{1}{1 - t}) \to (\forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \forall i \in (1 \dots N) x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i))$
56	55	adantl	$⊢ ((((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \land l = 1 - (\frac{1}{1 - t})) \to (\forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \leftrightarrow \forall i \in (1 \dots N) x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i))$
57	22 11	subcld	$⊢ (t \in ℝ \land t < 0) \to 1 - t \in ℂ$
58	10 17	gtned	$⊢ (t \in ℝ \land t < 0) \to 1 \neq t$
59	22 11 58	subne0d	$⊢ (t \in ℝ \land t < 0) \to 1 - t \neq 0$
60	57 59	reccld	$⊢ (t \in ℝ \land t < 0) \to \frac{1}{1 - t} \in ℂ$
61	22 60	nncand	$⊢ (t \in ℝ \land t < 0) \to 1 - (1 - (\frac{1}{1 - t})) = \frac{1}{1 - t}$
62	61 60	eqeltrd	$⊢ (t \in ℝ \land t < 0) \to 1 - (1 - (\frac{1}{1 - t})) \in ℂ$
63	22 60	subcld	$⊢ (t \in ℝ \land t < 0) \to 1 - (\frac{1}{1 - t}) \in ℂ$
64	16	gt0ne0d	$⊢ (t \in ℝ \land t < 0) \to 1 \neq 0$
65	36 11	subeq0ad	$⊢ (t \in ℝ \land t < 0) \to (t - 1 - t = 0 \leftrightarrow t - 1 = t)$
66	11 22 11	sub32d	$⊢ (t \in ℝ \land t < 0) \to t - 1 - t = t - t - 1$
67	66	eqeq1d	$⊢ (t \in ℝ \land t < 0) \to (t - 1 - t = 0 \leftrightarrow t - t - 1 = 0)$
68	11	subidd	$⊢ (t \in ℝ \land t < 0) \to t - t = 0$
69	68	oveq1d	$⊢ (t \in ℝ \land t < 0) \to t - t - 1 = 0 - 1$
70	69	eqeq1d	$⊢ (t \in ℝ \land t < 0) \to (t - t - 1 = 0 \leftrightarrow 0 - 1 = 0)$
71		0cnd	$⊢ (t \in ℝ \land t < 0) \to 0 \in ℂ$
72	71 22 71	subaddd	$⊢ (t \in ℝ \land t < 0) \to (0 - 1 = 0 \leftrightarrow 1 + 0 = 0)$
73	22	addid1d	$⊢ (t \in ℝ \land t < 0) \to 1 + 0 = 1$
74	73	eqeq1d	$⊢ (t \in ℝ \land t < 0) \to (1 + 0 = 0 \leftrightarrow 1 = 0)$
75	72 74	bitrd	$⊢ (t \in ℝ \land t < 0) \to (0 - 1 = 0 \leftrightarrow 1 = 0)$
76	67 70 75	3bitrd	$⊢ (t \in ℝ \land t < 0) \to (t - 1 - t = 0 \leftrightarrow 1 = 0)$
77	65 76	bitr3d	$⊢ (t \in ℝ \land t < 0) \to (t - 1 = t \leftrightarrow 1 = 0)$
78	77	necon3bid	$⊢ (t \in ℝ \land t < 0) \to (t - 1 \neq t \leftrightarrow 1 \neq 0)$
79	64 78	mpbird	$⊢ (t \in ℝ \land t < 0) \to t - 1 \neq t$
80	20	eqeq2d	$⊢ (t \in ℝ \land t < 0) \to (1 = 1 - (\frac{1}{1 - t}) \leftrightarrow 1 = \frac{t}{t - 1})$
81		eqcom	$⊢ 1 = \frac{t}{t - 1} \leftrightarrow \frac{t}{t - 1} = 1$
82	11 36 22 23	divmuld	$⊢ (t \in ℝ \land t < 0) \to (\frac{t}{t - 1} = 1 \leftrightarrow (t - 1) \cdot 1 = t)$
83	81 82	syl5bb	$⊢ (t \in ℝ \land t < 0) \to (1 = \frac{t}{t - 1} \leftrightarrow (t - 1) \cdot 1 = t)$
84	36	mulid1d	$⊢ (t \in ℝ \land t < 0) \to (t - 1) \cdot 1 = t - 1$
85	84	eqeq1d	$⊢ (t \in ℝ \land t < 0) \to ((t - 1) \cdot 1 = t \leftrightarrow t - 1 = t)$
86	80 83 85	3bitrd	$⊢ (t \in ℝ \land t < 0) \to (1 = 1 - (\frac{1}{1 - t}) \leftrightarrow t - 1 = t)$
87	86	necon3bid	$⊢ (t \in ℝ \land t < 0) \to (1 \neq 1 - (\frac{1}{1 - t}) \leftrightarrow t - 1 \neq t)$
88	79 87	mpbird	$⊢ (t \in ℝ \land t < 0) \to 1 \neq 1 - (\frac{1}{1 - t})$
89	22 63 88	subne0d	$⊢ (t \in ℝ \land t < 0) \to 1 - (1 - (\frac{1}{1 - t})) \neq 0$
90	61	oveq1d	$⊢ (t \in ℝ \land t < 0) \to (1 - (1 - (\frac{1}{1 - t}))) (1 - t) = (\frac{1}{1 - t}) (1 - t)$
91	57 59	recid2d	$⊢ (t \in ℝ \land t < 0) \to (\frac{1}{1 - t}) (1 - t) = 1$
92	90 91	eqtrd	$⊢ (t \in ℝ \land t < 0) \to (1 - (1 - (\frac{1}{1 - t}))) (1 - t) = 1$
93	62 57 89 92	mvllmuld	$⊢ (t \in ℝ \land t < 0) \to 1 - t = \frac{1}{1 - (1 - (\frac{1}{1 - t}))}$
94	93	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - t = \frac{1}{1 - (1 - (\frac{1}{1 - t}))}$
95	94	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (1 - t) x (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i)$
96	20	oveq1d	$⊢ (t \in ℝ \land t < 0) \to 1 - (\frac{1}{1 - t}) - 1 = (\frac{t}{t - 1}) - 1$
97	20 96	oveq12d	$⊢ (t \in ℝ \land t < 0) \to \frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1} = \frac{\frac{t}{t - 1}}{(\frac{t}{t - 1}) - 1}$
98		subdivcomb2	$⊢ (t \in ℂ \land 1 \in ℂ \land (t - 1 \in ℂ \land t - 1 \neq 0)) \to \frac{t - (t - 1) \cdot 1}{t - 1} = (\frac{t}{t - 1}) - 1$
99	11 22 36 23 98	syl112anc	$⊢ (t \in ℝ \land t < 0) \to \frac{t - (t - 1) \cdot 1}{t - 1} = (\frac{t}{t - 1}) - 1$
100	84	oveq2d	$⊢ (t \in ℝ \land t < 0) \to t - (t - 1) \cdot 1 = t - (t - 1)$
101	11 22	nncand	$⊢ (t \in ℝ \land t < 0) \to t - (t - 1) = 1$
102	100 101	eqtrd	$⊢ (t \in ℝ \land t < 0) \to t - (t - 1) \cdot 1 = 1$
103	102	oveq1d	$⊢ (t \in ℝ \land t < 0) \to \frac{t - (t - 1) \cdot 1}{t - 1} = \frac{1}{t - 1}$
104	99 103	eqtr3d	$⊢ (t \in ℝ \land t < 0) \to (\frac{t}{t - 1}) - 1 = \frac{1}{t - 1}$
105	104	oveq1d	$⊢ (t \in ℝ \land t < 0) \to ((\frac{t}{t - 1}) - 1) t = (\frac{1}{t - 1}) t$
106	11 36 23	divrec2d	$⊢ (t \in ℝ \land t < 0) \to \frac{t}{t - 1} = (\frac{1}{t - 1}) t$
107	105 106	eqtr4d	$⊢ (t \in ℝ \land t < 0) \to ((\frac{t}{t - 1}) - 1) t = \frac{t}{t - 1}$
108	20 63	eqeltrrd	$⊢ (t \in ℝ \land t < 0) \to \frac{t}{t - 1} \in ℂ$
109	108 22	subcld	$⊢ (t \in ℝ \land t < 0) \to (\frac{t}{t - 1}) - 1 \in ℂ$
110	79	necomd	$⊢ (t \in ℝ \land t < 0) \to t \neq t - 1$
111	11 36 23 110	divne1d	$⊢ (t \in ℝ \land t < 0) \to \frac{t}{t - 1} \neq 1$
112	108 22 111	subne0d	$⊢ (t \in ℝ \land t < 0) \to (\frac{t}{t - 1}) - 1 \neq 0$
113	108 109 11 112	divmuld	$⊢ (t \in ℝ \land t < 0) \to (\frac{\frac{t}{t - 1}}{(\frac{t}{t - 1}) - 1} = t \leftrightarrow ((\frac{t}{t - 1}) - 1) t = \frac{t}{t - 1})$
114	107 113	mpbird	$⊢ (t \in ℝ \land t < 0) \to \frac{\frac{t}{t - 1}}{(\frac{t}{t - 1}) - 1} = t$
115	97 114	eqtr2d	$⊢ (t \in ℝ \land t < 0) \to t = \frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}$
116	115	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to t = \frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}$
117	116	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to t y (i) = (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i)$
118	95 117	oveq12d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (1 - t) x (i) + t y (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i)$
119	118	eqeq2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (p (i) = (1 - t) x (i) + t y (i) \leftrightarrow p (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i))$
120	119	biimpd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (p (i) = (1 - t) x (i) + t y (i) \to p (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i))$
121		eqcom	$⊢ x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i) \leftrightarrow (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i) = x (i)$
122		elmapi	$⊢ x \in (ℝ^{(1 \dots N)}) \to x : (1 \dots N) ⟶ ℝ$
123	122	3ad2ant2	$⊢ (N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \to x : (1 \dots N) ⟶ ℝ$
124	123	adantr	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to x : (1 \dots N) ⟶ ℝ$
125	124	ad2antrr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \to x : (1 \dots N) ⟶ ℝ$
126	125	ffvelrnda	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to x (i) \in ℝ$
127	126	recnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to x (i) \in ℂ$
128		1cnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 \in ℂ$
129	11	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to t \in ℂ$
130	128 129	subcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - t \in ℂ$
131	58	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 \neq t$
132	128 129 131	subne0d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - t \neq 0$
133	130 132	reccld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{1}{1 - t} \in ℂ$
134	128 133	subcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - (\frac{1}{1 - t}) \in ℂ$
135		eldifi	$⊢ y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) \to y \in (ℝ^{(1 \dots N)})$
136		elmapi	$⊢ y \in (ℝ^{(1 \dots N)}) \to y : (1 \dots N) ⟶ ℝ$
137	135 136	syl	$⊢ y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) \to y : (1 \dots N) ⟶ ℝ$
138	137	3ad2ant3	$⊢ (N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \to y : (1 \dots N) ⟶ ℝ$
139	138	adantr	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to y : (1 \dots N) ⟶ ℝ$
140	139	ad2antrr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \to y : (1 \dots N) ⟶ ℝ$
141	140	ffvelrnda	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to y (i) \in ℝ$
142	141	recnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to y (i) \in ℂ$
143	134 142	mulcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (1 - (\frac{1}{1 - t})) y (i) \in ℂ$
144	62	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - (1 - (\frac{1}{1 - t})) \in ℂ$
145		elmapi	$⊢ p \in (ℝ^{(1 \dots N)}) \to p : (1 \dots N) ⟶ ℝ$
146	145	adantl	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to p : (1 \dots N) ⟶ ℝ$
147	146	ad2antrr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \to p : (1 \dots N) ⟶ ℝ$
148	147	ffvelrnda	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to p (i) \in ℝ$
149	148	recnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to p (i) \in ℂ$
150	144 149	mulcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (1 - (1 - (\frac{1}{1 - t}))) p (i) \in ℂ$
151	127 143 150	subadd2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (x (i) - (1 - (\frac{1}{1 - t})) y (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) \leftrightarrow (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i) = x (i))$
152	121 151	bitr4id	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i) \leftrightarrow x (i) - (1 - (\frac{1}{1 - t})) y (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i))$
153		eqcom	$⊢ x (i) - (1 - (\frac{1}{1 - t})) y (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) \leftrightarrow (1 - (1 - (\frac{1}{1 - t}))) p (i) = x (i) - (1 - (\frac{1}{1 - t})) y (i)$
154	127 143	subcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to x (i) - (1 - (\frac{1}{1 - t})) y (i) \in ℂ$
155	89	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - (1 - (\frac{1}{1 - t})) \neq 0$
156	154 144 149 155	divmuld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (\frac{x (i) - (1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} = p (i) \leftrightarrow (1 - (1 - (\frac{1}{1 - t}))) p (i) = x (i) - (1 - (\frac{1}{1 - t})) y (i))$
157		eqcom	$⊢ \frac{x (i) - (1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} = p (i) \leftrightarrow p (i) = \frac{x (i) - (1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))}$
158	127 143 144 155	divsubdird	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{x (i) - (1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} = (\frac{x (i)}{1 - (1 - (\frac{1}{1 - t}))}) - (\frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))})$
159	127 144 155	divcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{x (i)}{1 - (1 - (\frac{1}{1 - t}))} \in ℂ$
160	143 144 155	divcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} \in ℂ$
161	159 160	negsubd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (\frac{x (i)}{1 - (1 - (\frac{1}{1 - t}))}) + (- \frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))}) = (\frac{x (i)}{1 - (1 - (\frac{1}{1 - t}))}) - (\frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))})$
162	127 144 155	divrec2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{x (i)}{1 - (1 - (\frac{1}{1 - t}))} = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i)$
163	143 144 155	divneg2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to - \frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} = \frac{(1 - (\frac{1}{1 - t})) y (i)}{- (1 - (1 - (\frac{1}{1 - t})))}$
164	128 134	negsubdi2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to - (1 - (1 - (\frac{1}{1 - t}))) = 1 - (\frac{1}{1 - t}) - 1$
165	164	oveq2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{(1 - (\frac{1}{1 - t})) y (i)}{- (1 - (1 - (\frac{1}{1 - t})))} = \frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (\frac{1}{1 - t}) - 1}$
166	134 128	subcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - (\frac{1}{1 - t}) - 1 \in ℂ$
167	88	necomd	$⊢ (t \in ℝ \land t < 0) \to 1 - (\frac{1}{1 - t}) \neq 1$
168	63 22 167	subne0d	$⊢ (t \in ℝ \land t < 0) \to 1 - (\frac{1}{1 - t}) - 1 \neq 0$
169	168	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to 1 - (\frac{1}{1 - t}) - 1 \neq 0$
170	134 142 166 169	div23d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (\frac{1}{1 - t}) - 1} = (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i)$
171	163 165 170	3eqtrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to - \frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} = (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i)$
172	162 171	oveq12d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (\frac{x (i)}{1 - (1 - (\frac{1}{1 - t}))}) + (- \frac{(1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))}) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i)$
173	158 161 172	3eqtr2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to \frac{x (i) - (1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i)$
174	173	eqeq2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (p (i) = \frac{x (i) - (1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} \leftrightarrow p (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i))$
175	157 174	syl5bb	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (\frac{x (i) - (1 - (\frac{1}{1 - t})) y (i)}{1 - (1 - (\frac{1}{1 - t}))} = p (i) \leftrightarrow p (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i))$
176	156 175	bitr3d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to ((1 - (1 - (\frac{1}{1 - t}))) p (i) = x (i) - (1 - (\frac{1}{1 - t})) y (i) \leftrightarrow p (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i))$
177	153 176	syl5bb	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (x (i) - (1 - (\frac{1}{1 - t})) y (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) \leftrightarrow p (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i))$
178	152 177	bitrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i) \leftrightarrow p (i) = (\frac{1}{1 - (1 - (\frac{1}{1 - t}))}) x (i) + (\frac{1 - (\frac{1}{1 - t})}{1 - (\frac{1}{1 - t}) - 1}) y (i))$
179	120 178	sylibrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land i \in (1 \dots N)) \to (p (i) = (1 - t) x (i) + t y (i) \to x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i))$
180	179	ralimdva	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to \forall i \in (1 \dots N) x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i))$
181	180	imp	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to \forall i \in (1 \dots N) x (i) = (1 - (1 - (\frac{1}{1 - t}))) p (i) + (1 - (\frac{1}{1 - t})) y (i)$
182	49 56 181	rspcedvd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)$
183	182	3mix2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land t < 0) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
184	183	exp31	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (t < 0 \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))))$
185	184	com23	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (t < 0 \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))))$
186	185	imp	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to (t < 0 \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
187		simpr	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \land t \in [0, 1]) \to t \in [0, 1]$
188		oveq2	$⊢ k = t \to 1 - k = 1 - t$
189	188	oveq1d	$⊢ k = t \to (1 - k) x (i) = (1 - t) x (i)$
190		oveq1	$⊢ k = t \to k y (i) = t y (i)$
191	189 190	oveq12d	$⊢ k = t \to (1 - k) x (i) + k y (i) = (1 - t) x (i) + t y (i)$
192	191	eqeq2d	$⊢ k = t \to (p (i) = (1 - k) x (i) + k y (i) \leftrightarrow p (i) = (1 - t) x (i) + t y (i))$
193	192	ralbidv	$⊢ k = t \to (\forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \leftrightarrow \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
194	193	adantl	$⊢ ((((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \land t \in [0, 1]) \land k = t) \to (\forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \leftrightarrow \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
195		simplr	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \land t \in [0, 1]) \to \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)$
196	187 194 195	rspcedvd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \land t \in [0, 1]) \to \exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i)$
197	196	3mix1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \land t \in [0, 1]) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
198	197	ex	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to (t \in [0, 1] \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
199		1red	$⊢ (t \in ℝ \land 1 < t) \to 1 \in ℝ$
200		simpl	$⊢ (t \in ℝ \land 1 < t) \to t \in ℝ$
201		0red	$⊢ (t \in ℝ \land 1 < t) \to 0 \in ℝ$
202	15	a1i	$⊢ (t \in ℝ \land 1 < t) \to 0 < 1$
203		simpr	$⊢ (t \in ℝ \land 1 < t) \to 1 < t$
204	201 199 200 202 203	lttrd	$⊢ (t \in ℝ \land 1 < t) \to 0 < t$
205	204	gt0ne0d	$⊢ (t \in ℝ \land 1 < t) \to t \neq 0$
206	199 200 205	redivcld	$⊢ (t \in ℝ \land 1 < t) \to \frac{1}{t} \in ℝ$
207	200 204	recgt0d	$⊢ (t \in ℝ \land 1 < t) \to 0 < \frac{1}{t}$
208		recgt1i	$⊢ (t \in ℝ \land 1 < t) \to (0 < \frac{1}{t} \land \frac{1}{t} < 1)$
209	206	adantr	$⊢ ((t \in ℝ \land 1 < t) \land (0 < \frac{1}{t} \land \frac{1}{t} < 1)) \to \frac{1}{t} \in ℝ$
210		1red	$⊢ ((t \in ℝ \land 1 < t) \land (0 < \frac{1}{t} \land \frac{1}{t} < 1)) \to 1 \in ℝ$
211		simprr	$⊢ ((t \in ℝ \land 1 < t) \land (0 < \frac{1}{t} \land \frac{1}{t} < 1)) \to \frac{1}{t} < 1$
212	209 210 211	ltled	$⊢ ((t \in ℝ \land 1 < t) \land (0 < \frac{1}{t} \land \frac{1}{t} < 1)) \to \frac{1}{t} \leq 1$
213	208 212	mpdan	$⊢ (t \in ℝ \land 1 < t) \to \frac{1}{t} \leq 1$
214	206 207 213	3jca	$⊢ (t \in ℝ \land 1 < t) \to (\frac{1}{t} \in ℝ \land 0 < \frac{1}{t} \land \frac{1}{t} \leq 1)$
215		1re	$⊢ 1 \in ℝ$
216	6 215	pm3.2i	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ)$
217		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (\frac{1}{t} \in (0, 1] \leftrightarrow (\frac{1}{t} \in ℝ \land 0 < \frac{1}{t} \land \frac{1}{t} \leq 1))$
218	216 217	mp1i	$⊢ (t \in ℝ \land 1 < t) \to (\frac{1}{t} \in (0, 1] \leftrightarrow (\frac{1}{t} \in ℝ \land 0 < \frac{1}{t} \land \frac{1}{t} \leq 1))$
219	214 218	mpbird	$⊢ (t \in ℝ \land 1 < t) \to \frac{1}{t} \in (0, 1]$
220	219	ad4ant23	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to \frac{1}{t} \in (0, 1]$
221		oveq2	$⊢ m = \frac{1}{t} \to 1 - m = 1 - (\frac{1}{t})$
222	221	oveq1d	$⊢ m = \frac{1}{t} \to (1 - m) x (i) = (1 - (\frac{1}{t})) x (i)$
223		oveq1	$⊢ m = \frac{1}{t} \to m p (i) = (\frac{1}{t}) p (i)$
224	222 223	oveq12d	$⊢ m = \frac{1}{t} \to (1 - m) x (i) + m p (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i)$
225	224	eqeq2d	$⊢ m = \frac{1}{t} \to (y (i) = (1 - m) x (i) + m p (i) \leftrightarrow y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i))$
226	225	ralbidv	$⊢ m = \frac{1}{t} \to (\forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i))$
227	226	adantl	$⊢ ((((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \land m = \frac{1}{t}) \to (\forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \leftrightarrow \forall i \in (1 \dots N) y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i))$
228		simplr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to t \in ℝ$
229	228	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to t \in ℂ$
230	229	adantr	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to t \in ℂ$
231	204	ex	$⊢ t \in ℝ \to (1 < t \to 0 < t)$
232		gt0ne0	$⊢ (t \in ℝ \land 0 < t) \to t \neq 0$
233	232	ex	$⊢ t \in ℝ \to (0 < t \to t \neq 0)$
234	231 233	syld	$⊢ t \in ℝ \to (1 < t \to t \neq 0)$
235	234	adantl	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (1 < t \to t \neq 0)$
236	235	imp	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to t \neq 0$
237	236	adantr	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to t \neq 0$
238	230 237	reccld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{1}{t} \in ℂ$
239		1cnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to 1 \in ℂ$
240	230 237	recne0d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{1}{t} \neq 0$
241	238 239 238 240	divsubdird	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{(\frac{1}{t}) - 1}{\frac{1}{t}} = (\frac{\frac{1}{t}}{\frac{1}{t}}) - (\frac{1}{\frac{1}{t}})$
242	238 240	dividd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{\frac{1}{t}}{\frac{1}{t}} = 1$
243	230 237	recrecd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{1}{\frac{1}{t}} = t$
244	242 243	oveq12d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{\frac{1}{t}}{\frac{1}{t}}) - (\frac{1}{\frac{1}{t}}) = 1 - t$
245	241 244	eqtr2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to 1 - t = \frac{(\frac{1}{t}) - 1}{\frac{1}{t}}$
246	245	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (1 - t) x (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i)$
247	229 236	recrecd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to \frac{1}{\frac{1}{t}} = t$
248	247	eqcomd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to t = \frac{1}{\frac{1}{t}}$
249	248	adantr	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to t = \frac{1}{\frac{1}{t}}$
250	249	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to t y (i) = (\frac{1}{\frac{1}{t}}) y (i)$
251	246 250	oveq12d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (1 - t) x (i) + t y (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i)$
252	251	eqeq2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (p (i) = (1 - t) x (i) + t y (i) \leftrightarrow p (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i))$
253	252	biimpd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (p (i) = (1 - t) x (i) + t y (i) \to p (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i))$
254		eqcom	$⊢ y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i) \leftrightarrow (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i) = y (i)$
255	139	ad2antrr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to y : (1 \dots N) ⟶ ℝ$
256	255	ffvelrnda	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to y (i) \in ℝ$
257	256	recnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to y (i) \in ℂ$
258	239 238	subcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to 1 - (\frac{1}{t}) \in ℂ$
259	124	ad2antrr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to x : (1 \dots N) ⟶ ℝ$
260	259	ffvelrnda	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to x (i) \in ℝ$
261	260	recnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to x (i) \in ℂ$
262	258 261	mulcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (1 - (\frac{1}{t})) x (i) \in ℂ$
263	146	ad2antrr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to p : (1 \dots N) ⟶ ℝ$
264	263	ffvelrnda	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to p (i) \in ℝ$
265	264	recnd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to p (i) \in ℂ$
266	238 265	mulcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{1}{t}) p (i) \in ℂ$
267	257 262 266	subaddd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (y (i) - (1 - (\frac{1}{t})) x (i) = (\frac{1}{t}) p (i) \leftrightarrow (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i) = y (i))$
268	254 267	bitr4id	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i) \leftrightarrow y (i) - (1 - (\frac{1}{t})) x (i) = (\frac{1}{t}) p (i))$
269		eqcom	$⊢ y (i) - (1 - (\frac{1}{t})) x (i) = (\frac{1}{t}) p (i) \leftrightarrow (\frac{1}{t}) p (i) = y (i) - (1 - (\frac{1}{t})) x (i)$
270	257 262	subcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to y (i) - (1 - (\frac{1}{t})) x (i) \in ℂ$
271	270 238 265 240	divmuld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = p (i) \leftrightarrow (\frac{1}{t}) p (i) = y (i) - (1 - (\frac{1}{t})) x (i))$
272	269 271	bitr4id	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (y (i) - (1 - (\frac{1}{t})) x (i) = (\frac{1}{t}) p (i) \leftrightarrow \frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = p (i))$
273		eqcom	$⊢ \frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = p (i) \leftrightarrow p (i) = \frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}}$
274	257 262 238 240	divsubdird	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = (\frac{y (i)}{\frac{1}{t}}) - (\frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}})$
275	257 238 240	divcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{y (i)}{\frac{1}{t}} \in ℂ$
276	262 238 240	divcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} \in ℂ$
277	275 276	negsubd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{y (i)}{\frac{1}{t}}) + (- \frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}}) = (\frac{y (i)}{\frac{1}{t}}) - (\frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}})$
278	262 238 240	divnegd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to - \frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = \frac{- (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}}$
279	258 261	mulneg1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (- (1 - (\frac{1}{t}))) x (i) = - (1 - (\frac{1}{t})) x (i)$
280	279	eqcomd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to - (1 - (\frac{1}{t})) x (i) = (- (1 - (\frac{1}{t}))) x (i)$
281	280	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{- (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = \frac{(- (1 - (\frac{1}{t}))) x (i)}{\frac{1}{t}}$
282	239 238	negsubdi2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to - (1 - (\frac{1}{t})) = (\frac{1}{t}) - 1$
283	282	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (- (1 - (\frac{1}{t}))) x (i) = ((\frac{1}{t}) - 1) x (i)$
284	283	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{(- (1 - (\frac{1}{t}))) x (i)}{\frac{1}{t}} = \frac{((\frac{1}{t}) - 1) x (i)}{\frac{1}{t}}$
285	238 239	subcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{1}{t}) - 1 \in ℂ$
286	285 261 238 240	div23d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{((\frac{1}{t}) - 1) x (i)}{\frac{1}{t}} = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i)$
287	284 286	eqtrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{(- (1 - (\frac{1}{t}))) x (i)}{\frac{1}{t}} = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i)$
288	278 281 287	3eqtrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to - \frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i)$
289	288	oveq2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{y (i)}{\frac{1}{t}}) + (- \frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}}) = (\frac{y (i)}{\frac{1}{t}}) + (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i)$
290	257 238 240	divrec2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{y (i)}{\frac{1}{t}} = (\frac{1}{\frac{1}{t}}) y (i)$
291	290	oveq1d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{y (i)}{\frac{1}{t}}) + (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) = (\frac{1}{\frac{1}{t}}) y (i) + (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i)$
292	238 240	reccld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{1}{\frac{1}{t}} \in ℂ$
293	292 257	mulcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{1}{\frac{1}{t}}) y (i) \in ℂ$
294	285 238 240	divcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{(\frac{1}{t}) - 1}{\frac{1}{t}} \in ℂ$
295	294 261	mulcld	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) \in ℂ$
296	293 295	addcomd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{1}{\frac{1}{t}}) y (i) + (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i)$
297	289 291 296	3eqtrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{y (i)}{\frac{1}{t}}) + (- \frac{(1 - (\frac{1}{t})) x (i)}{\frac{1}{t}}) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i)$
298	274 277 297	3eqtr2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to \frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i)$
299	298	eqeq2d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (p (i) = \frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} \leftrightarrow p (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i))$
300	273 299	syl5bb	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (\frac{y (i) - (1 - (\frac{1}{t})) x (i)}{\frac{1}{t}} = p (i) \leftrightarrow p (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i))$
301	268 272 300	3bitrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i) \leftrightarrow p (i) = (\frac{(\frac{1}{t}) - 1}{\frac{1}{t}}) x (i) + (\frac{1}{\frac{1}{t}}) y (i))$
302	253 301	sylibrd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land i \in (1 \dots N)) \to (p (i) = (1 - t) x (i) + t y (i) \to y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i))$
303	302	ralimdva	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to \forall i \in (1 \dots N) y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i))$
304	303	imp	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to \forall i \in (1 \dots N) y (i) = (1 - (\frac{1}{t})) x (i) + (\frac{1}{t}) p (i)$
305	220 227 304	rspcedvd	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)$
306	305	3mix3d	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land 1 < t) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))$
307	306	exp31	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (1 < t \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))))$
308	307	com23	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (1 < t \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))))$
309	308	imp	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to (1 < t \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
310	186 198 309	3jaod	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \land \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)) \to ((t < 0 \lor t \in [0, 1] \lor 1 < t) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
311	310	ex	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to ((t < 0 \lor t \in [0, 1] \lor 1 < t) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i))))$
312	5 311	mpid	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land t \in ℝ) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$
313	312	rexlimdva	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to (\exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \lor \exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \lor \exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)))$

Metamath Proof Explorer

Theorem eenglngeehlnmlem2

Proof