eenglngeehlnmlem1

		Ref	Expression
	Assertion	eenglngeehlnmlem1	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \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)) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ k = t \to 1 - k = 1 - t$
2	1	oveq1d	$⊢ k = t \to (1 - k) x (i) = (1 - t) x (i)$
3		oveq1	$⊢ k = t \to k y (i) = t y (i)$
4	2 3	oveq12d	$⊢ k = t \to (1 - k) x (i) + k y (i) = (1 - t) x (i) + t y (i)$
5	4	eqeq2d	$⊢ k = t \to (p (i) = (1 - k) x (i) + k y (i) \leftrightarrow p (i) = (1 - t) x (i) + t y (i))$
6	5	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))$
7	6	cbvrexvw	$⊢ \exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)$
8		unitssre	$⊢ [0, 1] \subseteq ℝ$
9		ssrexv	$⊢ [0, 1] \subseteq ℝ \to (\exists t \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
10	8 9	mp1i	$⊢ ((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 [0, 1] \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
11	7 10	syl5bi	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to (\exists k \in [0, 1] \forall i \in (1 \dots N) p (i) = (1 - k) x (i) + k y (i) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
12		0re	$⊢ 0 \in ℝ$
13		1xr	$⊢ 1 \in ℝ^{*}$
14		elico2	$⊢ (0 \in ℝ \land 1 \in ℝ^{*}) \to (l \in [0, 1) \leftrightarrow (l \in ℝ \land 0 \leq l \land l < 1))$
15	12 13 14	mp2an	$⊢ l \in [0, 1) \leftrightarrow (l \in ℝ \land 0 \leq l \land l < 1)$
16		simp1	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to l \in ℝ$
17		1red	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to 1 \in ℝ$
18	17 16	resubcld	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to 1 - l \in ℝ$
19		1cnd	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to 1 \in ℂ$
20	16	recnd	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to l \in ℂ$
21		ltne	$⊢ (l \in ℝ \land l < 1) \to 1 \neq l$
22	21	3adant2	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to 1 \neq l$
23	19 20 22	subne0d	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to 1 - l \neq 0$
24	16 18 23	redivcld	$⊢ (l \in ℝ \land 0 \leq l \land l < 1) \to \frac{l}{1 - l} \in ℝ$
25	15 24	sylbi	$⊢ l \in [0, 1) \to \frac{l}{1 - l} \in ℝ$
26	25	ad2antlr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)) \to \frac{l}{1 - l} \in ℝ$
27	26	renegcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)) \to - \frac{l}{1 - l} \in ℝ$
28		oveq2	$⊢ t = - \frac{l}{1 - l} \to 1 - t = 1 - (- \frac{l}{1 - l})$
29	28	oveq1d	$⊢ t = - \frac{l}{1 - l} \to (1 - t) x (i) = (1 - (- \frac{l}{1 - l})) x (i)$
30		oveq1	$⊢ t = - \frac{l}{1 - l} \to t y (i) = (- \frac{l}{1 - l}) y (i)$
31	29 30	oveq12d	$⊢ t = - \frac{l}{1 - l} \to (1 - t) x (i) + t y (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i)$
32	31	eqeq2d	$⊢ t = - \frac{l}{1 - l} \to (p (i) = (1 - t) x (i) + t y (i) \leftrightarrow p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
33	32	ralbidv	$⊢ t = - \frac{l}{1 - l} \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \leftrightarrow \forall i \in (1 \dots N) p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
34	33	adantl	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)) \land t = - \frac{l}{1 - l}) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \leftrightarrow \forall i \in (1 \dots N) p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
35		eqcom	$⊢ x (i) = (1 - l) p (i) + l y (i) \leftrightarrow (1 - l) p (i) + l y (i) = x (i)$
36		elmapi	$⊢ x \in (ℝ^{(1 \dots N)}) \to x : (1 \dots N) ⟶ ℝ$
37	36	3ad2ant2	$⊢ (N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \to x : (1 \dots N) ⟶ ℝ$
38	37	ad2antrr	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \to x : (1 \dots N) ⟶ ℝ$
39	38	ffvelrnda	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to x (i) \in ℝ$
40	39	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to x (i) \in ℂ$
41	15 16	sylbi	$⊢ l \in [0, 1) \to l \in ℝ$
42	41	ad2antlr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to l \in ℝ$
43	42	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to l \in ℂ$
44		eldifi	$⊢ y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) \to y \in (ℝ^{(1 \dots N)})$
45		elmapi	$⊢ y \in (ℝ^{(1 \dots N)}) \to y : (1 \dots N) ⟶ ℝ$
46	44 45	syl	$⊢ y \in ((ℝ^{(1 \dots N)}) ∖ \{x\}) \to y : (1 \dots N) ⟶ ℝ$
47	46	3ad2ant3	$⊢ (N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \to y : (1 \dots N) ⟶ ℝ$
48	47	ad2antrr	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \to y : (1 \dots N) ⟶ ℝ$
49	48	ffvelrnda	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to y (i) \in ℝ$
50	49	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to y (i) \in ℂ$
51	43 50	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to l y (i) \in ℂ$
52		1cnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to 1 \in ℂ$
53	52 43	subcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to 1 - l \in ℂ$
54		elmapi	$⊢ p \in (ℝ^{(1 \dots N)}) \to p : (1 \dots N) ⟶ ℝ$
55	54	ad2antlr	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \to p : (1 \dots N) ⟶ ℝ$
56	55	ffvelrnda	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to p (i) \in ℝ$
57	56	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to p (i) \in ℂ$
58	53 57	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (1 - l) p (i) \in ℂ$
59	40 51 58	subadd2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (x (i) - l y (i) = (1 - l) p (i) \leftrightarrow (1 - l) p (i) + l y (i) = x (i))$
60	35 59	bitr4id	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (x (i) = (1 - l) p (i) + l y (i) \leftrightarrow x (i) - l y (i) = (1 - l) p (i))$
61		eqcom	$⊢ x (i) - l y (i) = (1 - l) p (i) \leftrightarrow (1 - l) p (i) = x (i) - l y (i)$
62	40 51	subcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to x (i) - l y (i) \in ℂ$
63	15 22	sylbi	$⊢ l \in [0, 1) \to 1 \neq l$
64	63	ad2antlr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to 1 \neq l$
65	52 43 64	subne0d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to 1 - l \neq 0$
66	62 53 57 65	divmuld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{x (i) - l y (i)}{1 - l} = p (i) \leftrightarrow (1 - l) p (i) = x (i) - l y (i))$
67	61 66	bitr4id	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (x (i) - l y (i) = (1 - l) p (i) \leftrightarrow \frac{x (i) - l y (i)}{1 - l} = p (i))$
68		eqcom	$⊢ \frac{x (i) - l y (i)}{1 - l} = p (i) \leftrightarrow p (i) = \frac{x (i) - l y (i)}{1 - l}$
69	40 51 53 65	divsubdird	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{x (i) - l y (i)}{1 - l} = (\frac{x (i)}{1 - l}) - (\frac{l y (i)}{1 - l})$
70	40 53 65	divrec2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{x (i)}{1 - l} = (\frac{1}{1 - l}) x (i)$
71	43 50 53 65	div23d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{l y (i)}{1 - l} = (\frac{l}{1 - l}) y (i)$
72	70 71	oveq12d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{x (i)}{1 - l}) - (\frac{l y (i)}{1 - l}) = (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i)$
73	69 72	eqtrd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{x (i) - l y (i)}{1 - l} = (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i)$
74	73	eqeq2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (p (i) = \frac{x (i) - l y (i)}{1 - l} \leftrightarrow p (i) = (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i))$
75	68 74	syl5bb	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{x (i) - l y (i)}{1 - l} = p (i) \leftrightarrow p (i) = (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i))$
76	43 53 65	divcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{l}{1 - l} \in ℂ$
77	76 50	mulneg1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (- \frac{l}{1 - l}) y (i) = - (\frac{l}{1 - l}) y (i)$
78	77	eqcomd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to - (\frac{l}{1 - l}) y (i) = (- \frac{l}{1 - l}) y (i)$
79	78	oveq2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{1}{1 - l}) x (i) + (- (\frac{l}{1 - l}) y (i)) = (\frac{1}{1 - l}) x (i) + (- \frac{l}{1 - l}) y (i)$
80	53 65	reccld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{1}{1 - l} \in ℂ$
81	80 40	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{1}{1 - l}) x (i) \in ℂ$
82	76 50	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{l}{1 - l}) y (i) \in ℂ$
83	81 82	negsubd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{1}{1 - l}) x (i) + (- (\frac{l}{1 - l}) y (i)) = (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i)$
84	52 76	subnegd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to 1 - (- \frac{l}{1 - l}) = 1 + (\frac{l}{1 - l})$
85		muldivdir	$⊢ (1 \in ℂ \land l \in ℂ \land (1 - l \in ℂ \land 1 - l \neq 0)) \to \frac{(1 - l) \cdot 1 + l}{1 - l} = 1 + (\frac{l}{1 - l})$
86	52 43 53 65 85	syl112anc	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{(1 - l) \cdot 1 + l}{1 - l} = 1 + (\frac{l}{1 - l})$
87	53	mulid1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (1 - l) \cdot 1 = 1 - l$
88	87	oveq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (1 - l) \cdot 1 + l = 1 - l + l$
89	52 43	npcand	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to 1 - l + l = 1$
90	88 89	eqtrd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (1 - l) \cdot 1 + l = 1$
91	90	oveq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{(1 - l) \cdot 1 + l}{1 - l} = \frac{1}{1 - l}$
92	84 86 91	3eqtr2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to 1 - (- \frac{l}{1 - l}) = \frac{1}{1 - l}$
93	92	eqcomd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to \frac{1}{1 - l} = 1 - (- \frac{l}{1 - l})$
94	93	oveq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{1}{1 - l}) x (i) = (1 - (- \frac{l}{1 - l})) x (i)$
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 l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{1}{1 - l}) x (i) + (- \frac{l}{1 - l}) y (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i)$
96	79 83 95	3eqtr3d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i)$
97	96	eqeq2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (p (i) = (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i) \leftrightarrow p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
98	97	biimpd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (p (i) = (\frac{1}{1 - l}) x (i) - (\frac{l}{1 - l}) y (i) \to p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
99	75 98	sylbid	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (\frac{x (i) - l y (i)}{1 - l} = p (i) \to p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
100	67 99	sylbid	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (x (i) - l y (i) = (1 - l) p (i) \to p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
101	60 100	sylbid	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land i \in (1 \dots N)) \to (x (i) = (1 - l) p (i) + l y (i) \to p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
102	101	ralimdva	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \to (\forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \to \forall i \in (1 \dots N) p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i))$
103	102	imp	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)) \to \forall i \in (1 \dots N) p (i) = (1 - (- \frac{l}{1 - l})) x (i) + (- \frac{l}{1 - l}) y (i)$
104	27 34 103	rspcedvd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land l \in [0, 1)) \land \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i)) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)$
105	104	rexlimdva2	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to (\exists l \in [0, 1) \forall i \in (1 \dots N) x (i) = (1 - l) p (i) + l y (i) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
106		0xr	$⊢ 0 \in ℝ^{*}$
107		1re	$⊢ 1 \in ℝ$
108		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (m \in (0, 1] \leftrightarrow (m \in ℝ \land 0 < m \land m \leq 1))$
109	106 107 108	mp2an	$⊢ m \in (0, 1] \leftrightarrow (m \in ℝ \land 0 < m \land m \leq 1)$
110		simp1	$⊢ (m \in ℝ \land 0 < m \land m \leq 1) \to m \in ℝ$
111		gt0ne0	$⊢ (m \in ℝ \land 0 < m) \to m \neq 0$
112	111	3adant3	$⊢ (m \in ℝ \land 0 < m \land m \leq 1) \to m \neq 0$
113	110 112	rereccld	$⊢ (m \in ℝ \land 0 < m \land m \leq 1) \to \frac{1}{m} \in ℝ$
114	109 113	sylbi	$⊢ m \in (0, 1] \to \frac{1}{m} \in ℝ$
115	114	ad2antlr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)) \to \frac{1}{m} \in ℝ$
116		oveq2	$⊢ t = \frac{1}{m} \to 1 - t = 1 - (\frac{1}{m})$
117	116	oveq1d	$⊢ t = \frac{1}{m} \to (1 - t) x (i) = (1 - (\frac{1}{m})) x (i)$
118		oveq1	$⊢ t = \frac{1}{m} \to t y (i) = (\frac{1}{m}) y (i)$
119	117 118	oveq12d	$⊢ t = \frac{1}{m} \to (1 - t) x (i) + t y (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i)$
120	119	eqeq2d	$⊢ t = \frac{1}{m} \to (p (i) = (1 - t) x (i) + t y (i) \leftrightarrow p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i))$
121	120	ralbidv	$⊢ t = \frac{1}{m} \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \leftrightarrow \forall i \in (1 \dots N) p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i))$
122	121	adantl	$⊢ (((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)) \land t = \frac{1}{m}) \to (\forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i) \leftrightarrow \forall i \in (1 \dots N) p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i))$
123		eqcom	$⊢ y (i) = (1 - m) x (i) + m p (i) \leftrightarrow (1 - m) x (i) + m p (i) = y (i)$
124	47	ad2antrr	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \to y : (1 \dots N) ⟶ ℝ$
125	124	ffvelrnda	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to y (i) \in ℝ$
126	125	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to y (i) \in ℂ$
127		1cnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to 1 \in ℂ$
128	109 110	sylbi	$⊢ m \in (0, 1] \to m \in ℝ$
129	128	recnd	$⊢ m \in (0, 1] \to m \in ℂ$
130	129	ad2antlr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to m \in ℂ$
131	127 130	subcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to 1 - m \in ℂ$
132	37	ad2antrr	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \to x : (1 \dots N) ⟶ ℝ$
133	132	ffvelrnda	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to x (i) \in ℝ$
134	133	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to x (i) \in ℂ$
135	131 134	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (1 - m) x (i) \in ℂ$
136	126 135	negsubd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to y (i) + (- (1 - m) x (i)) = y (i) - (1 - m) x (i)$
137	131 134	mulneg1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (- (1 - m)) x (i) = - (1 - m) x (i)$
138	127 130	negsubdi2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to - (1 - m) = m - 1$
139	138	oveq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (- (1 - m)) x (i) = (m - 1) x (i)$
140	137 139	eqtr3d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to - (1 - m) x (i) = (m - 1) x (i)$
141	140	oveq2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to y (i) + (- (1 - m) x (i)) = y (i) + (m - 1) x (i)$
142	136 141	eqtr3d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to y (i) - (1 - m) x (i) = y (i) + (m - 1) x (i)$
143	142	eqeq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (y (i) - (1 - m) x (i) = m p (i) \leftrightarrow y (i) + (m - 1) x (i) = m p (i))$
144	54	ad2antlr	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \to p : (1 \dots N) ⟶ ℝ$
145	144	ffvelrnda	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to p (i) \in ℝ$
146	145	recnd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to p (i) \in ℂ$
147	130 146	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to m p (i) \in ℂ$
148	126 135 147	subaddd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (y (i) - (1 - m) x (i) = m p (i) \leftrightarrow (1 - m) x (i) + m p (i) = y (i))$
149		eqcom	$⊢ \frac{y (i) + (m - 1) x (i)}{m} = p (i) \leftrightarrow p (i) = \frac{y (i) + (m - 1) x (i)}{m}$
150	149	a1i	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{y (i) + (m - 1) x (i)}{m} = p (i) \leftrightarrow p (i) = \frac{y (i) + (m - 1) x (i)}{m})$
151	130 127	subcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to m - 1 \in ℂ$
152	151 134	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (m - 1) x (i) \in ℂ$
153	126 152	addcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to y (i) + (m - 1) x (i) \in ℂ$
154		elioc1	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (m \in (0, 1] \leftrightarrow (m \in ℝ^{*} \land 0 < m \land m \leq 1))$
155	106 13 154	mp2an	$⊢ m \in (0, 1] \leftrightarrow (m \in ℝ^{*} \land 0 < m \land m \leq 1)$
156	12	a1i	$⊢ m \in ℝ^{*} \to 0 \in ℝ$
157	156	anim1i	$⊢ (m \in ℝ^{*} \land 0 < m) \to (0 \in ℝ \land 0 < m)$
158	157	3adant3	$⊢ (m \in ℝ^{*} \land 0 < m \land m \leq 1) \to (0 \in ℝ \land 0 < m)$
159		ltne	$⊢ (0 \in ℝ \land 0 < m) \to m \neq 0$
160	158 159	syl	$⊢ (m \in ℝ^{*} \land 0 < m \land m \leq 1) \to m \neq 0$
161	155 160	sylbi	$⊢ m \in (0, 1] \to m \neq 0$
162	161	ad2antlr	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to m \neq 0$
163	153 146 130 162	divmul2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{y (i) + (m - 1) x (i)}{m} = p (i) \leftrightarrow y (i) + (m - 1) x (i) = m p (i))$
164	126 152 130 162	divdird	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{y (i) + (m - 1) x (i)}{m} = (\frac{y (i)}{m}) + (\frac{(m - 1) x (i)}{m})$
165	126 130 162	divrec2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{y (i)}{m} = (\frac{1}{m}) y (i)$
166	151 134 130 162	div23d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{(m - 1) x (i)}{m} = (\frac{m - 1}{m}) x (i)$
167	130 127 130 162	divsubdird	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{m - 1}{m} = (\frac{m}{m}) - (\frac{1}{m})$
168	167	oveq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{m - 1}{m}) x (i) = ((\frac{m}{m}) - (\frac{1}{m})) x (i)$
169	166 168	eqtrd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{(m - 1) x (i)}{m} = ((\frac{m}{m}) - (\frac{1}{m})) x (i)$
170	165 169	oveq12d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{y (i)}{m}) + (\frac{(m - 1) x (i)}{m}) = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i)$
171	164 170	eqtrd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{y (i) + (m - 1) x (i)}{m} = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i)$
172	171	eqeq2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (p (i) = \frac{y (i) + (m - 1) x (i)}{m} \leftrightarrow p (i) = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i))$
173	150 163 172	3bitr3d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (y (i) + (m - 1) x (i) = m p (i) \leftrightarrow p (i) = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i))$
174	143 148 173	3bitr3d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to ((1 - m) x (i) + m p (i) = y (i) \leftrightarrow p (i) = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i))$
175	123 174	syl5bb	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (y (i) = (1 - m) x (i) + m p (i) \leftrightarrow p (i) = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i))$
176	130 162	reccld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{1}{m} \in ℂ$
177	176 126	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{1}{m}) y (i) \in ℂ$
178	127 176	subcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to 1 - (\frac{1}{m}) \in ℂ$
179	178 134	mulcld	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (1 - (\frac{1}{m})) x (i) \in ℂ$
180	130 162	dividd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to \frac{m}{m} = 1$
181	180	oveq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{m}{m}) - (\frac{1}{m}) = 1 - (\frac{1}{m})$
182	181	oveq1d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to ((\frac{m}{m}) - (\frac{1}{m})) x (i) = (1 - (\frac{1}{m})) x (i)$
183	182	oveq2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i) = (\frac{1}{m}) y (i) + (1 - (\frac{1}{m})) x (i)$
184	177 179 183	comraddd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i)$
185	184	eqeq2d	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (p (i) = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i) \leftrightarrow p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i))$
186	185	biimpd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (p (i) = (\frac{1}{m}) y (i) + ((\frac{m}{m}) - (\frac{1}{m})) x (i) \to p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i))$
187	175 186	sylbid	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land i \in (1 \dots N)) \to (y (i) = (1 - m) x (i) + m p (i) \to p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i))$
188	187	ralimdva	$⊢ (((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \to (\forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \to \forall i \in (1 \dots N) p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i))$
189	188	imp	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)) \to \forall i \in (1 \dots N) p (i) = (1 - (\frac{1}{m})) x (i) + (\frac{1}{m}) y (i)$
190	115 122 189	rspcedvd	$⊢ ((((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \land m \in (0, 1]) \land \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i)) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i)$
191	190	rexlimdva2	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \to (\exists m \in (0, 1] \forall i \in (1 \dots N) y (i) = (1 - m) x (i) + m p (i) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$
192	11 105 191	3jaod	$⊢ ((N \in ℕ \land x \in (ℝ^{(1 \dots N)}) \land y \in ((ℝ^{(1 \dots N)}) ∖ \{x\})) \land p \in (ℝ^{(1 \dots N)})) \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)) \to \exists t \in ℝ \forall i \in (1 \dots N) p (i) = (1 - t) x (i) + t y (i))$

Metamath Proof Explorer

Theorem eenglngeehlnmlem1

Proof