eenglngeehlnmlem2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > eenglngeehlnmlem2		Structured version Visualization version GIF version

Theorem eenglngeehlnmlem2 49229

Description: Lemma 2 for eenglngeehlnm 49230. (Contributed by AV, 15-Feb-2023.)

**Assertion**
Ref	Expression
eenglngeehlnmlem2	⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → (∃𝑡 ∈ ℝ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))

Distinct variable group: 𝑖,𝑁,𝑘,𝑙,𝑚,𝑝,𝑡,𝑥,𝑦

**Proof of Theorem eenglngeehlnmlem2**
Step	Hyp	Ref	Expression
1		0red 11138	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
2		1red 11136	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
3		simpr 485	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
4		reorelicc 49201	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
5	1, 2, 3, 4	syl3anc 1379	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
6		0xr 11183	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
7	6	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ∈ ℝ^*)
8		1xr 11195	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ^*
9	8	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈ ℝ^*)
10		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈ ℝ)
11	10	recnd 11164	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈ ℂ)
12		0red 11138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℝ)
13		1red 11136	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℝ)
14		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 0)
15		0lt1 11663	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
16	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < 1)
17	10, 12, 13, 14, 16	lttrd 11298	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 1)
18	10, 17	ltned 11273	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ 1)
19		1subrec1sub 49196	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 1) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
20	11, 18, 19	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
21	10, 13	resubcld 11569	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℝ)
22		1cnd 11130	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℂ)
23	11, 22, 18	subne0d 11505	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 0)
24	10, 21, 23	redivcld 11974	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ)
25	24	rexrd 11186	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ^*)
26	20, 25	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ∈ ℝ^*)
27	26	ad4ant23 759	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈ ℝ^*)
28	10	renegcld 11568	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -𝑡 ∈ ℝ)
29	10, 13	sublt0d 11767	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) < 0 ↔ 𝑡 < 1))
30	17, 29	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) < 0)
31	21, 30	negelrpd 12969	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -(𝑡 − 1) ∈ ℝ⁺)
32	10, 12, 14	ltled 11285	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≤ 0)
33	10	le0neg1d 11712	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 ≤ 0 ↔ 0 ≤ -𝑡))
34	32, 33	mpbid 233	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ -𝑡)
35	28, 31, 34	divge0d 13017	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (-𝑡 / -(𝑡 − 1)))
36	21	recnd 11164	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℂ)
37	11, 36, 23	div2negd 11937	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (-𝑡 / -(𝑡 − 1)) = (𝑡 / (𝑡 − 1)))
38	20, 37	eqtr4d 2777	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (-𝑡 / -(𝑡 − 1)))
39	35, 38	breqtrrd 5100	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (1 − (1 / (1 − 𝑡))))
40	39	ad4ant23 759	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ≤ (1 − (1 / (1 − 𝑡))))
41		1red 11136	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈ ℝ)
42	13, 10	resubcld 11569	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ)
43	10, 13	posdifd 11728	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 < 1 ↔ 0 < (1 − 𝑡)))
44	17, 43	mpbid 233	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < (1 − 𝑡))
45	42, 44	elrpd 12974	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ⁺)
46	45	ad4ant23 759	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − 𝑡) ∈ ℝ⁺)
47	46	rpreccld 12987	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / (1 − 𝑡)) ∈ ℝ⁺)
48	41, 47	ltsubrpd 13009	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) < 1)
49	7, 9, 27, 40, 48	elicod 13339	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈ (0[,)1))
50		oveq2 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (1 − 𝑙) = (1 − (1 − (1 / (1 − 𝑡)))))
51	50	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → ((1 − 𝑙) · (𝑝‘𝑖)) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)))
52		oveq1 7363	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (𝑙 · (𝑦‘𝑖)) = ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))
53	51, 52	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
54	53	eqeq2d 2750	. . . . . . . . . . . 12 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → ((𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
55	54	ralbidv 3162	. . . . . . . . . . 11 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
56	55	adantl 482	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑙 = (1 − (1 / (1 − 𝑡)))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
57	22, 11	subcld 11496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℂ)
58	10, 17	gtned 11272	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 𝑡)
59	22, 11, 58	subne0d 11505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ≠ 0)
60	57, 59	reccld 11915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 / (1 − 𝑡)) ∈ ℂ)
61	22, 60	nncand 11501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) = (1 / (1 − 𝑡)))
62	61, 60	eqeltrd 2839	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ∈ ℂ)
63	22, 60	subcld 11496	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
64	16	gt0ne0d 11705	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 0)
65	36, 11	subeq0ad 11506	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ (𝑡 − 1) = 𝑡))
66	11, 22, 11	sub32d 11528	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) − 𝑡) = ((𝑡 − 𝑡) − 1))
67	66	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ ((𝑡 − 𝑡) − 1) = 0))
68	11	subidd 11484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 𝑡) = 0)
69	68	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 𝑡) − 1) = (0 − 1))
70	69	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 𝑡) − 1) = 0 ↔ (0 − 1) = 0))
71		0cnd 11128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℂ)
72	71, 22, 71	subaddd 11514	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) = 0 ↔ (1 + 0) = 0))
73	22	addridd 11337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 + 0) = 1)
74	73	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 + 0) = 0 ↔ 1 = 0))
75	72, 74	bitrd 280	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) = 0 ↔ 1 = 0))
76	67, 70, 75	3bitrd 306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ 1 = 0))
77	65, 76	bitr3d 282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) = 𝑡 ↔ 1 = 0))
78	77	necon3bid 2978	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) ≠ 𝑡 ↔ 1 ≠ 0))
79	64, 78	mpbird 258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 𝑡)
80	20	eqeq2d 2750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ 1 = (𝑡 / (𝑡 − 1))))
81		eqcom 2746	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 = (𝑡 / (𝑡 − 1)) ↔ (𝑡 / (𝑡 − 1)) = 1)
82	11, 36, 22, 23	divmuld 11944	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) = 1 ↔ ((𝑡 − 1) · 1) = 𝑡))
83	81, 82	bitrid 284	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (𝑡 / (𝑡 − 1)) ↔ ((𝑡 − 1) · 1) = 𝑡))
84	36	mulridd 11153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) · 1) = (𝑡 − 1))
85	84	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) · 1) = 𝑡 ↔ (𝑡 − 1) = 𝑡))
86	80, 83, 85	3bitrd 306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) = 𝑡))
87	86	necon3bid 2978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 ≠ (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) ≠ 𝑡))
88	79, 87	mpbird 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ (1 − (1 / (1 − 𝑡))))
89	22, 63, 88	subne0d 11505	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ≠ 0)
90	61	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = ((1 / (1 − 𝑡)) · (1 − 𝑡)))
91	57, 59	recid2d 11918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 / (1 − 𝑡)) · (1 − 𝑡)) = 1)
92	90, 91	eqtrd 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = 1)
93	62, 57, 89, 92	mvllmuld 11978	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) = (1 / (1 − (1 − (1 / (1 − 𝑡))))))
94	93	ad4ant23 759	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (1 / (1 − (1 − (1 / (1 − 𝑡))))))
95	94	oveq1d 7371	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
96	20	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) − 1) = ((𝑡 / (𝑡 − 1)) − 1))
97	20, 96	oveq12d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) = ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)))
98		subdivcomb2 11842	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((𝑡 − 1) ∈ ℂ ∧ (𝑡 − 1) ≠ 0)) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
99	11, 22, 36, 23, 98	syl112anc 1382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
100	84	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = (𝑡 − (𝑡 − 1)))
101	11, 22	nncand 11501	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − (𝑡 − 1)) = 1)
102	100, 101	eqtrd 2774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = 1)
103	102	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = (1 / (𝑡 − 1)))
104	99, 103	eqtr3d 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) = (1 / (𝑡 − 1)))
105	104	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = ((1 / (𝑡 − 1)) · 𝑡))
106	11, 36, 23	divrec2d 11926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) = ((1 / (𝑡 − 1)) · 𝑡))
107	105, 106	eqtr4d 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1)))
108	20, 63	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℂ)
109	108, 22	subcld 11496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ∈ ℂ)
110	79	necomd 2989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ (𝑡 − 1))
111	11, 36, 23, 110	divne1d 11933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ≠ 1)
112	108, 22, 111	subne0d 11505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ≠ 0)
113	108, 109, 11, 112	divmuld 11944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡 ↔ (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1))))
114	107, 113	mpbird 258	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡)
115	97, 114	eqtr2d 2775	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 = ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)))
116	115	ad4ant23 759	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)))
117	116	oveq1d 7371	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))
118	95, 117	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖))))
119	118	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
120	119	biimpd 230	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
121		eqcom 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = (𝑥‘𝑖))
122		elmapi 8786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶ℝ)
123	122	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) → 𝑥:(1...𝑁)⟶ℝ)
124	123	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑥:(1...𝑁)⟶ℝ)
125	124	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑥:(1...𝑁)⟶ℝ)
126	125	ffvelcdmda 7025	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
127	126	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
128		1cnd 11130	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ)
129	11	ad4ant23 759	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
130	128, 129	subcld 11496	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
131	58	ad4ant23 759	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ≠ 𝑡)
132	128, 129, 131	subne0d 11505	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ≠ 0)
133	130, 132	reccld 11915	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 − 𝑡)) ∈ ℂ)
134	128, 133	subcld 11496	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
135		eldifi 4061	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥}) → 𝑦 ∈ (ℝ ↑_m (1...𝑁)))
136		elmapi 8786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ℝ ↑_m (1...𝑁)) → 𝑦:(1...𝑁)⟶ℝ)
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥}) → 𝑦:(1...𝑁)⟶ℝ)
138	137	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) → 𝑦:(1...𝑁)⟶ℝ)
139	138	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑦:(1...𝑁)⟶ℝ)
140	139	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑦:(1...𝑁)⟶ℝ)
141	140	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
142	141	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
143	134, 142	mulcld 11156	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) ∈ ℂ)
144	62	ad4ant23 759	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1 − 𝑡)))) ∈ ℂ)
145		elmapi 8786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ (ℝ ↑_m (1...𝑁)) → 𝑝:(1...𝑁)⟶ℝ)
146	145	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑝:(1...𝑁)⟶ℝ)
147	146	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑝:(1...𝑁)⟶ℝ)
148	147	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
149	148	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
150	144, 149	mulcld 11156	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ∈ ℂ)
151	127, 143, 150	subadd2d 11515	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ↔ (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = (𝑥‘𝑖)))
152	121, 151	bitr4id 291	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖))))
153		eqcom 2746	. . . . . . . . . . . . . . 15 ⊢ (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ↔ ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
154	127, 143	subcld 11496	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ∈ ℂ)
155	89	ad4ant23 759	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1 − 𝑡)))) ≠ 0)
156	154, 144, 149, 155	divmuld 11944	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (𝑝‘𝑖) ↔ ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
157		eqcom 2746	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))))
158	127, 143, 144, 155	divsubdird 11961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) − (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡)))))))
159	127, 144, 155	divcld 11922	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
160	143, 144, 155	divcld 11922	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
161	159, 160	negsubd 11502	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) + -(((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡)))))) = (((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) − (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡)))))))
162	127, 144, 155	divrec2d 11926	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
163	143, 144, 155	divneg2d 11936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡))))) = (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / -(1 − (1 − (1 / (1 − 𝑡))))))
164	128, 134	negsubdi2d 11512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 − (1 / (1 − 𝑡)))) = ((1 − (1 / (1 − 𝑡))) − 1))
165	164	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / -(1 − (1 − (1 / (1 − 𝑡))))) = (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / ((1 − (1 / (1 − 𝑡))) − 1)))
166	134, 128	subcld 11496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ∈ ℂ)
167	88	necomd 2989	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ≠ 1)
168	63, 22, 167	subne0d 11505	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) − 1) ≠ 0)
169	168	ad4ant23 759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ≠ 0)
170	134, 142, 166, 169	div23d 11959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / ((1 − (1 / (1 − 𝑡))) − 1)) = (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))
171	163, 165, 170	3eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡))))) = (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))
172	162, 171	oveq12d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) + -(((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡)))))) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖))))
173	158, 161, 172	3eqtr2d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖))))
174	173	eqeq2d 2750	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
175	157, 174	bitrid 284	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
176	156, 175	bitr3d 282	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
177	153, 176	bitrid 284	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
178	152, 177	bitrd 280	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
179	120, 178	sylibrd 260	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
180	179	ralimdva 3151	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
181	180	imp 407	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
182	49, 56, 181	rspcedvd 3562	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))
183	182	3mix2d 1344	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
184	183	exp31 420	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))))
185	184	com23 86	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑡 < 0 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))))
186	185	imp 407	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (𝑡 < 0 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
187		simpr 485	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
188		oveq2 7364	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑡 → (1 − 𝑘) = (1 − 𝑡))
189	188	oveq1d 7371	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → ((1 − 𝑘) · (𝑥‘𝑖)) = ((1 − 𝑡) · (𝑥‘𝑖)))
190		oveq1 7363	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → (𝑘 · (𝑦‘𝑖)) = (𝑡 · (𝑦‘𝑖)))
191	189, 190	oveq12d 7374	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑡 → (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
192	191	eqeq2d 2750	. . . . . . . . . 10 ⊢ (𝑘 = 𝑡 → ((𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
193	192	ralbidv 3162	. . . . . . . . 9 ⊢ (𝑘 = 𝑡 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
194	193	adantl 482	. . . . . . . 8 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) ∧ 𝑘 = 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
195		simplr 774	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
196	187, 194, 195	rspcedvd 3562	. . . . . . 7 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))))
197	196	3mix1d 1343	. . . . . 6 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
198	197	ex 413	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (𝑡 ∈ (0[,]1) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
199		1red 11136	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 ∈ ℝ)
200		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
201		0red 11138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 ∈ ℝ)
202	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 1)
203		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 < 𝑡)
204	201, 199, 200, 202, 203	lttrd 11298	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 𝑡)
205	204	gt0ne0d 11705	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ≠ 0)
206	199, 200, 205	redivcld 11974	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ∈ ℝ)
207	200, 204	recgt0d 12081	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < (1 / 𝑡))
208		recgt1i 12044	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1))
209	206	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ∈ ℝ)
210		1red 11136	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → 1 ∈ ℝ)
211		simprr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) < 1)
212	209, 210, 211	ltled 11285	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ≤ 1)
213	208, 212	mpdan 693	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ≤ 1)
214	206, 207, 213	3jca 1134	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → ((1 / 𝑡) ∈ ℝ ∧ 0 < (1 / 𝑡) ∧ (1 / 𝑡) ≤ 1))
215		1re 11135	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
216	6, 215	pm3.2i 471	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ^* ∧ 1 ∈ ℝ)
217		elioc2 13353	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ) → ((1 / 𝑡) ∈ (0(,]1) ↔ ((1 / 𝑡) ∈ ℝ ∧ 0 < (1 / 𝑡) ∧ (1 / 𝑡) ≤ 1)))
218	216, 217	mp1i 13	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → ((1 / 𝑡) ∈ (0(,]1) ↔ ((1 / 𝑡) ∈ ℝ ∧ 0 < (1 / 𝑡) ∧ (1 / 𝑡) ≤ 1)))
219	214, 218	mpbird 258	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ∈ (0(,]1))
220	219	ad4ant23 759	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / 𝑡) ∈ (0(,]1))
221		oveq2 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (1 / 𝑡) → (1 − 𝑚) = (1 − (1 / 𝑡)))
222	221	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → ((1 − 𝑚) · (𝑥‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
223		oveq1 7363	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → (𝑚 · (𝑝‘𝑖)) = ((1 / 𝑡) · (𝑝‘𝑖)))
224	222, 223	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ (𝑚 = (1 / 𝑡) → (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))
225	224	eqeq2d 2750	. . . . . . . . . . . 12 ⊢ (𝑚 = (1 / 𝑡) → ((𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
226	225	ralbidv 3162	. . . . . . . . . . 11 ⊢ (𝑚 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
227	226	adantl 482	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑚 = (1 / 𝑡)) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
228		simplr 774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
229	228	recnd 11164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ∈ ℂ)
230	229	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
231	204	ex 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → (1 < 𝑡 → 0 < 𝑡))
232		gt0ne0 11606	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → 𝑡 ≠ 0)
233	232	ex 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → (0 < 𝑡 → 𝑡 ≠ 0))
234	231, 233	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ → (1 < 𝑡 → 𝑡 ≠ 0))
235	234	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (1 < 𝑡 → 𝑡 ≠ 0))
236	235	imp 407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ≠ 0)
237	236	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
238	230, 237	reccld 11915	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ∈ ℂ)
239		1cnd 11130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ)
240	230, 237	recne0d 11916	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ≠ 0)
241	238, 239, 238, 240	divsubdird 11961	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) = (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))))
242	238, 240	dividd 11920	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) / (1 / 𝑡)) = 1)
243	230, 237	recrecd 11919	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) = 𝑡)
244	242, 243	oveq12d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))) = (1 − 𝑡))
245	241, 244	eqtr2d 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (((1 / 𝑡) − 1) / (1 / 𝑡)))
246	245	oveq1d 7371	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
247	229, 236	recrecd 11919	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → (1 / (1 / 𝑡)) = 𝑡)
248	247	eqcomd 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 = (1 / (1 / 𝑡)))
249	248	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = (1 / (1 / 𝑡)))
250	249	oveq1d 7371	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
251	246, 250	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
252	251	eqeq2d 2750	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
253	252	biimpd 230	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
254		eqcom 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖))
255	139	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑦:(1...𝑁)⟶ℝ)
256	255	ffvelcdmda 7025	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
257	256	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
258	239, 238	subcld 11496	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / 𝑡)) ∈ ℂ)
259	124	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑥:(1...𝑁)⟶ℝ)
260	259	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
261	260	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
262	258, 261	mulcld 11156	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ)
263	146	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑝:(1...𝑁)⟶ℝ)
264	263	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
265	264	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
266	238, 265	mulcld 11156	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) · (𝑝‘𝑖)) ∈ ℂ)
267	257, 262, 266	subaddd 11514	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖)))
268	254, 267	bitr4id 291	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖))))
269		eqcom 2746	. . . . . . . . . . . . . . 15 ⊢ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))))
270	257, 262	subcld 11496	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) ∈ ℂ)
271	270, 238, 265, 240	divmuld 11944	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))))
272	269, 271	bitr4id 291	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖)))
273		eqcom 2746	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)))
274	257, 262, 238, 240	divsubdird 11961	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
275	257, 238, 240	divcld 11922	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) ∈ ℂ)
276	262, 238, 240	divcld 11922	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) ∈ ℂ)
277	275, 276	negsubd 11502	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
278	262, 238, 240	divnegd 11935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
279	258, 261	mulneg1d 11594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = -((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
280	279	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -((1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)))
281	280	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
282	239, 238	negsubdi2d 11512	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 / 𝑡)) = ((1 / 𝑡) − 1))
283	282	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (((1 / 𝑡) − 1) · (𝑥‘𝑖)))
284	283	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)))
285	238, 239	subcld 11496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) − 1) ∈ ℂ)
286	285, 261, 238, 240	div23d 11959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
287	284, 286	eqtrd 2774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
288	278, 281, 287	3eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
289	288	oveq2d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
290	257, 238, 240	divrec2d 11926	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
291	290	oveq1d 7371	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
292	238, 240	reccld 11915	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) ∈ ℂ)
293	292, 257	mulcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / (1 / 𝑡)) · (𝑦‘𝑖)) ∈ ℂ)
294	285, 238, 240	divcld 11922	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) ∈ ℂ)
295	294, 261	mulcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ)
296	293, 295	addcomd 11339	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
297	289, 291, 296	3eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
298	274, 277, 297	3eqtr2d 2780	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
299	298	eqeq2d 2750	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
300	273, 299	bitrid 284	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
301	268, 272, 300	3bitrd 306	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
302	253, 301	sylibrd 260	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
303	302	ralimdva 3151	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
304	303	imp 407	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))
305	220, 227, 304	rspcedvd 3562	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))
306	305	3mix3d 1345	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
307	306	exp31 420	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (1 < 𝑡 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))))
308	307	com23 86	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (1 < 𝑡 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))))
309	308	imp 407	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 < 𝑡 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
310	186, 198, 309	3jaod 1437	. . . 4 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ((𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
311	310	ex 413	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ((𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))))
312	5, 311	mpid 44	. 2 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
313	312	rexlimdva 3140	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → (∃𝑡 ∈ ℝ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∨ w3o 1091 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 ∖ cdif 3880 {csn 4555 class class class wbr 5072 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356 ↑_m cmap 8763 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 ℝ^*cxr 11169 < clt 11170 ≤ cle 11171 − cmin 11368 -cneg 11369 / cdiv 11798 ℕcn 12165 ℝ⁺crp 12933 (,]cioc 13290 [,)cico 13291 [,]cicc 13292 ...cfz 13452

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-po 5526 df-so 5527 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-1st 7931 df-2nd 7932 df-er 8633 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-rp 12934 df-ioc 13294 df-ico 13295 df-icc 13296

This theorem is referenced by: eenglngeehlnm 49230

W3C validator