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 48659

Description: Lemma 2 for eenglngeehlnm 48660. (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 11264	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
2		1red 11262	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
3		simpr 484	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
4		reorelicc 48631	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
5	1, 2, 3, 4	syl3anc 1373	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
6		0xr 11308	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
7	6	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ∈ ℝ^*)
8		1xr 11320	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ^*
9	8	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈ ℝ^*)
10		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈ ℝ)
11	10	recnd 11289	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈ ℂ)
12		0red 11264	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℝ)
13		1red 11262	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℝ)
14		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 0)
15		0lt1 11785	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
16	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < 1)
17	10, 12, 13, 14, 16	lttrd 11422	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 1)
18	10, 17	ltned 11397	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ 1)
19		1subrec1sub 48626	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 1) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
20	11, 18, 19	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
21	10, 13	resubcld 11691	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℝ)
22		1cnd 11256	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℂ)
23	11, 22, 18	subne0d 11629	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 0)
24	10, 21, 23	redivcld 12095	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ)
25	24	rexrd 11311	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ^*)
26	20, 25	eqeltrd 2841	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ∈ ℝ^*)
27	26	ad4ant23 753	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈ ℝ^*)
28	10	renegcld 11690	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -𝑡 ∈ ℝ)
29	10, 13	sublt0d 11889	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) < 0 ↔ 𝑡 < 1))
30	17, 29	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) < 0)
31	21, 30	negelrpd 13069	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -(𝑡 − 1) ∈ ℝ⁺)
32	10, 12, 14	ltled 11409	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≤ 0)
33	10	le0neg1d 11834	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 ≤ 0 ↔ 0 ≤ -𝑡))
34	32, 33	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ -𝑡)
35	28, 31, 34	divge0d 13117	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (-𝑡 / -(𝑡 − 1)))
36	21	recnd 11289	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℂ)
37	11, 36, 23	div2negd 12058	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (-𝑡 / -(𝑡 − 1)) = (𝑡 / (𝑡 − 1)))
38	20, 37	eqtr4d 2780	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (-𝑡 / -(𝑡 − 1)))
39	35, 38	breqtrrd 5171	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (1 − (1 / (1 − 𝑡))))
40	39	ad4ant23 753	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ≤ (1 − (1 / (1 − 𝑡))))
41		1red 11262	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈ ℝ)
42	13, 10	resubcld 11691	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ)
43	10, 13	posdifd 11850	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 < 1 ↔ 0 < (1 − 𝑡)))
44	17, 43	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < (1 − 𝑡))
45	42, 44	elrpd 13074	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ⁺)
46	45	ad4ant23 753	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − 𝑡) ∈ ℝ⁺)
47	46	rpreccld 13087	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / (1 − 𝑡)) ∈ ℝ⁺)
48	41, 47	ltsubrpd 13109	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) < 1)
49	7, 9, 27, 40, 48	elicod 13437	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈ (0[,)1))
50		oveq2 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (1 − 𝑙) = (1 − (1 − (1 / (1 − 𝑡)))))
51	50	oveq1d 7446	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → ((1 − 𝑙) · (𝑝‘𝑖)) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)))
52		oveq1 7438	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (𝑙 · (𝑦‘𝑖)) = ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))
53	51, 52	oveq12d 7449	. . . . . . . . . . . . 13 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
54	53	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → ((𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
55	54	ralbidv 3178	. . . . . . . . . . 11 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
56	55	adantl 481	. . . . . . . . . 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 11620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℂ)
58	10, 17	gtned 11396	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 𝑡)
59	22, 11, 58	subne0d 11629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ≠ 0)
60	57, 59	reccld 12036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 / (1 − 𝑡)) ∈ ℂ)
61	22, 60	nncand 11625	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) = (1 / (1 − 𝑡)))
62	61, 60	eqeltrd 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ∈ ℂ)
63	22, 60	subcld 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
64	16	gt0ne0d 11827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 0)
65	36, 11	subeq0ad 11630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ (𝑡 − 1) = 𝑡))
66	11, 22, 11	sub32d 11652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) − 𝑡) = ((𝑡 − 𝑡) − 1))
67	66	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ ((𝑡 − 𝑡) − 1) = 0))
68	11	subidd 11608	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 𝑡) = 0)
69	68	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 𝑡) − 1) = (0 − 1))
70	69	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 𝑡) − 1) = 0 ↔ (0 − 1) = 0))
71		0cnd 11254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℂ)
72	71, 22, 71	subaddd 11638	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) = 0 ↔ (1 + 0) = 0))
73	22	addridd 11461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 + 0) = 1)
74	73	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 + 0) = 0 ↔ 1 = 0))
75	72, 74	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) = 0 ↔ 1 = 0))
76	67, 70, 75	3bitrd 305	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ 1 = 0))
77	65, 76	bitr3d 281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) = 𝑡 ↔ 1 = 0))
78	77	necon3bid 2985	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) ≠ 𝑡 ↔ 1 ≠ 0))
79	64, 78	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 𝑡)
80	20	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ 1 = (𝑡 / (𝑡 − 1))))
81		eqcom 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 = (𝑡 / (𝑡 − 1)) ↔ (𝑡 / (𝑡 − 1)) = 1)
82	11, 36, 22, 23	divmuld 12065	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) = 1 ↔ ((𝑡 − 1) · 1) = 𝑡))
83	81, 82	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (𝑡 / (𝑡 − 1)) ↔ ((𝑡 − 1) · 1) = 𝑡))
84	36	mulridd 11278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) · 1) = (𝑡 − 1))
85	84	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) · 1) = 𝑡 ↔ (𝑡 − 1) = 𝑡))
86	80, 83, 85	3bitrd 305	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) = 𝑡))
87	86	necon3bid 2985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 ≠ (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) ≠ 𝑡))
88	79, 87	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ (1 − (1 / (1 − 𝑡))))
89	22, 63, 88	subne0d 11629	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ≠ 0)
90	61	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = ((1 / (1 − 𝑡)) · (1 − 𝑡)))
91	57, 59	recid2d 12039	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 / (1 − 𝑡)) · (1 − 𝑡)) = 1)
92	90, 91	eqtrd 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = 1)
93	62, 57, 89, 92	mvllmuld 12099	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) = (1 / (1 − (1 − (1 / (1 − 𝑡))))))
94	93	ad4ant23 753	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (1 / (1 − (1 − (1 / (1 − 𝑡))))))
95	94	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
96	20	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) − 1) = ((𝑡 / (𝑡 − 1)) − 1))
97	20, 96	oveq12d 7449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) = ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)))
98		subdivcomb2 11963	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((𝑡 − 1) ∈ ℂ ∧ (𝑡 − 1) ≠ 0)) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
99	11, 22, 36, 23, 98	syl112anc 1376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
100	84	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = (𝑡 − (𝑡 − 1)))
101	11, 22	nncand 11625	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − (𝑡 − 1)) = 1)
102	100, 101	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = 1)
103	102	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = (1 / (𝑡 − 1)))
104	99, 103	eqtr3d 2779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) = (1 / (𝑡 − 1)))
105	104	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = ((1 / (𝑡 − 1)) · 𝑡))
106	11, 36, 23	divrec2d 12047	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) = ((1 / (𝑡 − 1)) · 𝑡))
107	105, 106	eqtr4d 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1)))
108	20, 63	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℂ)
109	108, 22	subcld 11620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ∈ ℂ)
110	79	necomd 2996	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ (𝑡 − 1))
111	11, 36, 23, 110	divne1d 12054	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ≠ 1)
112	108, 22, 111	subne0d 11629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ≠ 0)
113	108, 109, 11, 112	divmuld 12065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡 ↔ (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1))))
114	107, 113	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡)
115	97, 114	eqtr2d 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 = ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)))
116	115	ad4ant23 753	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)))
117	116	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))
118	95, 117	oveq12d 7449	. . . . . . . . . . . . . . 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 2748	. . . . . . . . . . . . . 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 229	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
121		eqcom 2744	. . . . . . . . . . . . . . 15 ⊢ ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = (𝑥‘𝑖))
122		elmapi 8889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶ℝ)
123	122	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) → 𝑥:(1...𝑁)⟶ℝ)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑥:(1...𝑁)⟶ℝ)
125	124	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑥:(1...𝑁)⟶ℝ)
126	125	ffvelcdmda 7104	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
127	126	recnd 11289	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
128		1cnd 11256	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ)
129	11	ad4ant23 753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
130	128, 129	subcld 11620	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
131	58	ad4ant23 753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ≠ 𝑡)
132	128, 129, 131	subne0d 11629	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ≠ 0)
133	130, 132	reccld 12036	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 − 𝑡)) ∈ ℂ)
134	128, 133	subcld 11620	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
135		eldifi 4131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥}) → 𝑦 ∈ (ℝ ↑_m (1...𝑁)))
136		elmapi 8889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ℝ ↑_m (1...𝑁)) → 𝑦:(1...𝑁)⟶ℝ)
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥}) → 𝑦:(1...𝑁)⟶ℝ)
138	137	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) → 𝑦:(1...𝑁)⟶ℝ)
139	138	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑦:(1...𝑁)⟶ℝ)
140	139	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑦:(1...𝑁)⟶ℝ)
141	140	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
142	141	recnd 11289	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
143	134, 142	mulcld 11281	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) ∈ ℂ)
144	62	ad4ant23 753	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1 − 𝑡)))) ∈ ℂ)
145		elmapi 8889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ (ℝ ↑_m (1...𝑁)) → 𝑝:(1...𝑁)⟶ℝ)
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑝:(1...𝑁)⟶ℝ)
147	146	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑝:(1...𝑁)⟶ℝ)
148	147	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
149	148	recnd 11289	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
150	144, 149	mulcld 11281	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ∈ ℂ)
151	127, 143, 150	subadd2d 11639	. . . . . . . . . . . . . . 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 290	. . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . 15 ⊢ (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ↔ ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
154	127, 143	subcld 11620	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ∈ ℂ)
155	89	ad4ant23 753	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1 − 𝑡)))) ≠ 0)
156	154, 144, 149, 155	divmuld 12065	. . . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))))
158	127, 143, 144, 155	divsubdird 12082	. . . . . . . . . . . . . . . . . . 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 12043	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
160	143, 144, 155	divcld 12043	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
161	159, 160	negsubd 11626	. . . . . . . . . . . . . . . . . . 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 12047	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
163	143, 144, 155	divneg2d 12057	. . . . . . . . . . . . . . . . . . . . 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 11636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 − (1 / (1 − 𝑡)))) = ((1 − (1 / (1 − 𝑡))) − 1))
165	164	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . 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 11620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ∈ ℂ)
167	88	necomd 2996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ≠ 1)
168	63, 22, 167	subne0d 11629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) − 1) ≠ 0)
169	168	ad4ant23 753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ≠ 0)
170	134, 142, 166, 169	div23d 12080	. . . . . . . . . . . . . . . . . . . . 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 2781	. . . . . . . . . . . . . . . . . . . 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 7449	. . . . . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . . . . 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 2748	. . . . . . . . . . . . . . . . 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 283	. . . . . . . . . . . . . . . 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 281	. . . . . . . . . . . . . . 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 283	. . . . . . . . . . . . . 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 279	. . . . . . . . . . . . 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 259	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
180	179	ralimdva 3167	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
181	180	imp 406	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
182	49, 56, 181	rspcedvd 3624	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))
183	182	3mix2d 1338	. . . . . . . 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 419	. . . . . . 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 406	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (𝑡 < 0 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
187		simpr 484	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
188		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑡 → (1 − 𝑘) = (1 − 𝑡))
189	188	oveq1d 7446	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → ((1 − 𝑘) · (𝑥‘𝑖)) = ((1 − 𝑡) · (𝑥‘𝑖)))
190		oveq1 7438	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → (𝑘 · (𝑦‘𝑖)) = (𝑡 · (𝑦‘𝑖)))
191	189, 190	oveq12d 7449	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑡 → (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
192	191	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑘 = 𝑡 → ((𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
193	192	ralbidv 3178	. . . . . . . . 9 ⊢ (𝑘 = 𝑡 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
194	193	adantl 481	. . . . . . . 8 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) ∧ 𝑘 = 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
195		simplr 769	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
196	187, 194, 195	rspcedvd 3624	. . . . . . 7 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))))
197	196	3mix1d 1337	. . . . . 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 412	. . . . 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 11262	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 ∈ ℝ)
200		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
201		0red 11264	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 ∈ ℝ)
202	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 1)
203		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 < 𝑡)
204	201, 199, 200, 202, 203	lttrd 11422	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 𝑡)
205	204	gt0ne0d 11827	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ≠ 0)
206	199, 200, 205	redivcld 12095	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ∈ ℝ)
207	200, 204	recgt0d 12202	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < (1 / 𝑡))
208		recgt1i 12165	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1))
209	206	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ∈ ℝ)
210		1red 11262	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → 1 ∈ ℝ)
211		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) < 1)
212	209, 210, 211	ltled 11409	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ≤ 1)
213	208, 212	mpdan 687	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ≤ 1)
214	206, 207, 213	3jca 1129	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → ((1 / 𝑡) ∈ ℝ ∧ 0 < (1 / 𝑡) ∧ (1 / 𝑡) ≤ 1))
215		1re 11261	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
216	6, 215	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ^* ∧ 1 ∈ ℝ)
217		elioc2 13450	. . . . . . . . . . . . 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 257	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ∈ (0(,]1))
220	219	ad4ant23 753	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / 𝑡) ∈ (0(,]1))
221		oveq2 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (1 / 𝑡) → (1 − 𝑚) = (1 − (1 / 𝑡)))
222	221	oveq1d 7446	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → ((1 − 𝑚) · (𝑥‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
223		oveq1 7438	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → (𝑚 · (𝑝‘𝑖)) = ((1 / 𝑡) · (𝑝‘𝑖)))
224	222, 223	oveq12d 7449	. . . . . . . . . . . . 13 ⊢ (𝑚 = (1 / 𝑡) → (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))
225	224	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑚 = (1 / 𝑡) → ((𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
226	225	ralbidv 3178	. . . . . . . . . . 11 ⊢ (𝑚 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
227	226	adantl 481	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑚 = (1 / 𝑡)) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
228		simplr 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
229	228	recnd 11289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ∈ ℂ)
230	229	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
231	204	ex 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → (1 < 𝑡 → 0 < 𝑡))
232		gt0ne0 11728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → 𝑡 ≠ 0)
233	232	ex 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → (0 < 𝑡 → 𝑡 ≠ 0))
234	231, 233	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ → (1 < 𝑡 → 𝑡 ≠ 0))
235	234	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (1 < 𝑡 → 𝑡 ≠ 0))
236	235	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ≠ 0)
237	236	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
238	230, 237	reccld 12036	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ∈ ℂ)
239		1cnd 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ)
240	230, 237	recne0d 12037	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ≠ 0)
241	238, 239, 238, 240	divsubdird 12082	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) = (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))))
242	238, 240	dividd 12041	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) / (1 / 𝑡)) = 1)
243	230, 237	recrecd 12040	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) = 𝑡)
244	242, 243	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))) = (1 − 𝑡))
245	241, 244	eqtr2d 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (((1 / 𝑡) − 1) / (1 / 𝑡)))
246	245	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
247	229, 236	recrecd 12040	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → (1 / (1 / 𝑡)) = 𝑡)
248	247	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 = (1 / (1 / 𝑡)))
249	248	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = (1 / (1 / 𝑡)))
250	249	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
251	246, 250	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
252	251	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
253	252	biimpd 229	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
254		eqcom 2744	. . . . . . . . . . . . . . 15 ⊢ ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖))
255	139	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑦:(1...𝑁)⟶ℝ)
256	255	ffvelcdmda 7104	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
257	256	recnd 11289	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
258	239, 238	subcld 11620	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / 𝑡)) ∈ ℂ)
259	124	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑥:(1...𝑁)⟶ℝ)
260	259	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
261	260	recnd 11289	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
262	258, 261	mulcld 11281	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ)
263	146	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑝:(1...𝑁)⟶ℝ)
264	263	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
265	264	recnd 11289	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
266	238, 265	mulcld 11281	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) · (𝑝‘𝑖)) ∈ ℂ)
267	257, 262, 266	subaddd 11638	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖)))
268	254, 267	bitr4id 290	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖))))
269		eqcom 2744	. . . . . . . . . . . . . . 15 ⊢ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))))
270	257, 262	subcld 11620	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) ∈ ℂ)
271	270, 238, 265, 240	divmuld 12065	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))))
272	269, 271	bitr4id 290	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖)))
273		eqcom 2744	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)))
274	257, 262, 238, 240	divsubdird 12082	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
275	257, 238, 240	divcld 12043	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) ∈ ℂ)
276	262, 238, 240	divcld 12043	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) ∈ ℂ)
277	275, 276	negsubd 11626	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
278	262, 238, 240	divnegd 12056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
279	258, 261	mulneg1d 11716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = -((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
280	279	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -((1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)))
281	280	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
282	239, 238	negsubdi2d 11636	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 / 𝑡)) = ((1 / 𝑡) − 1))
283	282	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (((1 / 𝑡) − 1) · (𝑥‘𝑖)))
284	283	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)))
285	238, 239	subcld 11620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) − 1) ∈ ℂ)
286	285, 261, 238, 240	div23d 12080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
287	284, 286	eqtrd 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
288	278, 281, 287	3eqtrd 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
289	288	oveq2d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
290	257, 238, 240	divrec2d 12047	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
291	290	oveq1d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
292	238, 240	reccld 12036	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) ∈ ℂ)
293	292, 257	mulcld 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / (1 / 𝑡)) · (𝑦‘𝑖)) ∈ ℂ)
294	285, 238, 240	divcld 12043	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) ∈ ℂ)
295	294, 261	mulcld 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ)
296	293, 295	addcomd 11463	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
297	289, 291, 296	3eqtrd 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
298	274, 277, 297	3eqtr2d 2783	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
299	298	eqeq2d 2748	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
300	273, 299	bitrid 283	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
301	268, 272, 300	3bitrd 305	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
302	253, 301	sylibrd 259	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
303	302	ralimdva 3167	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
304	303	imp 406	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))
305	220, 227, 304	rspcedvd 3624	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))
306	305	3mix3d 1339	. . . . . . . 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 419	. . . . . . 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 406	. . . . 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 1431	. . . 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 412	. . 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 3155	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 206 ∧ wa 395 ∨ w3o 1086 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∖ cdif 3948 {csn 4626 class class class wbr 5143 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ↑_m cmap 8866 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 -cneg 11493 / cdiv 11920 ℕcn 12266 ℝ⁺crp 13034 (,]cioc 13388 [,)cico 13389 [,]cicc 13390 ...cfz 13547

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-po 5592 df-so 5593 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-1st 8014 df-2nd 8015 df-er 8745 df-map 8868 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-rp 13035 df-ioc 13392 df-ico 13393 df-icc 13394

This theorem is referenced by: eenglngeehlnm 48660

W3C validator