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 45152

Description: Lemma 2 for eenglngeehlnm 45153. (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 10633	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
2		1red 10631	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
3		simpr 488	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
4		reorelicc 45124	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
5	1, 2, 3, 4	syl3anc 1368	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
6		0xr 10677	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
7	6	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ∈ ℝ^*)
8		1xr 10689	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ^*
9	8	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈ ℝ^*)
10		simpl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈ ℝ)
11	10	recnd 10658	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈ ℂ)
12		0red 10633	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℝ)
13		1red 10631	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℝ)
14		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 0)
15		0lt1 11151	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
16	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < 1)
17	10, 12, 13, 14, 16	lttrd 10790	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 1)
18	10, 17	ltned 10765	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ 1)
19		1subrec1sub 45119	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 1) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
20	11, 18, 19	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
21	10, 13	resubcld 11057	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℝ)
22		1cnd 10625	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℂ)
23	11, 22, 18	subne0d 10995	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 0)
24	10, 21, 23	redivcld 11457	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ)
25	24	rexrd 10680	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ^*)
26	20, 25	eqeltrd 2890	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ∈ ℝ^*)
27	26	ad4ant23 752	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈ ℝ^*)
28	10	renegcld 11056	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -𝑡 ∈ ℝ)
29	10, 13	sublt0d 11255	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) < 0 ↔ 𝑡 < 1))
30	17, 29	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) < 0)
31	21, 30	negelrpd 12411	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -(𝑡 − 1) ∈ ℝ⁺)
32	10, 12, 14	ltled 10777	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≤ 0)
33	10	le0neg1d 11200	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 ≤ 0 ↔ 0 ≤ -𝑡))
34	32, 33	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ -𝑡)
35	28, 31, 34	divge0d 12459	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (-𝑡 / -(𝑡 − 1)))
36	21	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℂ)
37	11, 36, 23	div2negd 11420	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (-𝑡 / -(𝑡 − 1)) = (𝑡 / (𝑡 − 1)))
38	20, 37	eqtr4d 2836	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (-𝑡 / -(𝑡 − 1)))
39	35, 38	breqtrrd 5058	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (1 − (1 / (1 − 𝑡))))
40	39	ad4ant23 752	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ≤ (1 − (1 / (1 − 𝑡))))
41		1red 10631	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈ ℝ)
42	13, 10	resubcld 11057	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ)
43	10, 13	posdifd 11216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 < 1 ↔ 0 < (1 − 𝑡)))
44	17, 43	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < (1 − 𝑡))
45	42, 44	elrpd 12416	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ⁺)
46	45	ad4ant23 752	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − 𝑡) ∈ ℝ⁺)
47	46	rpreccld 12429	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / (1 − 𝑡)) ∈ ℝ⁺)
48	41, 47	ltsubrpd 12451	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) < 1)
49	7, 9, 27, 40, 48	elicod 12775	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈ (0[,)1))
50		oveq2 7143	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (1 − 𝑙) = (1 − (1 − (1 / (1 − 𝑡)))))
51	50	oveq1d 7150	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → ((1 − 𝑙) · (𝑝‘𝑖)) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)))
52		oveq1 7142	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (𝑙 · (𝑦‘𝑖)) = ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))
53	51, 52	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
54	53	eqeq2d 2809	. . . . . . . . . . . 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 485	. . . . . . . . . 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 10986	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℂ)
58	10, 17	gtned 10764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 𝑡)
59	22, 11, 58	subne0d 10995	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ≠ 0)
60	57, 59	reccld 11398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 / (1 − 𝑡)) ∈ ℂ)
61	22, 60	nncand 10991	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) = (1 / (1 − 𝑡)))
62	61, 60	eqeltrd 2890	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ∈ ℂ)
63	22, 60	subcld 10986	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
64	16	gt0ne0d 11193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 0)
65	36, 11	subeq0ad 10996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ (𝑡 − 1) = 𝑡))
66	11, 22, 11	sub32d 11018	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) − 𝑡) = ((𝑡 − 𝑡) − 1))
67	66	eqeq1d 2800	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ ((𝑡 − 𝑡) − 1) = 0))
68	11	subidd 10974	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 𝑡) = 0)
69	68	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 𝑡) − 1) = (0 − 1))
70	69	eqeq1d 2800	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 𝑡) − 1) = 0 ↔ (0 − 1) = 0))
71		0cnd 10623	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℂ)
72	71, 22, 71	subaddd 11004	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) = 0 ↔ (1 + 0) = 0))
73	22	addid1d 10829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 + 0) = 1)
74	73	eqeq1d 2800	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 + 0) = 0 ↔ 1 = 0))
75	72, 74	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) = 0 ↔ 1 = 0))
76	67, 70, 75	3bitrd 308	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ 1 = 0))
77	65, 76	bitr3d 284	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) = 𝑡 ↔ 1 = 0))
78	77	necon3bid 3031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) ≠ 𝑡 ↔ 1 ≠ 0))
79	64, 78	mpbird 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 𝑡)
80	20	eqeq2d 2809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ 1 = (𝑡 / (𝑡 − 1))))
81		eqcom 2805	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 = (𝑡 / (𝑡 − 1)) ↔ (𝑡 / (𝑡 − 1)) = 1)
82	11, 36, 22, 23	divmuld 11427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) = 1 ↔ ((𝑡 − 1) · 1) = 𝑡))
83	81, 82	syl5bb 286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (𝑡 / (𝑡 − 1)) ↔ ((𝑡 − 1) · 1) = 𝑡))
84	36	mulid1d 10647	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) · 1) = (𝑡 − 1))
85	84	eqeq1d 2800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) · 1) = 𝑡 ↔ (𝑡 − 1) = 𝑡))
86	80, 83, 85	3bitrd 308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) = 𝑡))
87	86	necon3bid 3031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 ≠ (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) ≠ 𝑡))
88	79, 87	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ (1 − (1 / (1 − 𝑡))))
89	22, 63, 88	subne0d 10995	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ≠ 0)
90	61	oveq1d 7150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = ((1 / (1 − 𝑡)) · (1 − 𝑡)))
91	57, 59	recid2d 11401	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 / (1 − 𝑡)) · (1 − 𝑡)) = 1)
92	90, 91	eqtrd 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = 1)
93	62, 57, 89, 92	mvllmuld 11461	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) = (1 / (1 − (1 − (1 / (1 − 𝑡))))))
94	93	ad4ant23 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (1 / (1 − (1 − (1 / (1 − 𝑡))))))
95	94	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
96	20	oveq1d 7150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) − 1) = ((𝑡 / (𝑡 − 1)) − 1))
97	20, 96	oveq12d 7153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) = ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)))
98		subdivcomb2 11325	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((𝑡 − 1) ∈ ℂ ∧ (𝑡 − 1) ≠ 0)) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
99	11, 22, 36, 23, 98	syl112anc 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
100	84	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = (𝑡 − (𝑡 − 1)))
101	11, 22	nncand 10991	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − (𝑡 − 1)) = 1)
102	100, 101	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = 1)
103	102	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = (1 / (𝑡 − 1)))
104	99, 103	eqtr3d 2835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) = (1 / (𝑡 − 1)))
105	104	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = ((1 / (𝑡 − 1)) · 𝑡))
106	11, 36, 23	divrec2d 11409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) = ((1 / (𝑡 − 1)) · 𝑡))
107	105, 106	eqtr4d 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1)))
108	20, 63	eqeltrrd 2891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℂ)
109	108, 22	subcld 10986	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ∈ ℂ)
110	79	necomd 3042	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ (𝑡 − 1))
111	11, 36, 23, 110	divne1d 11416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ≠ 1)
112	108, 22, 111	subne0d 10995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ≠ 0)
113	108, 109, 11, 112	divmuld 11427	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡 ↔ (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1))))
114	107, 113	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡)
115	97, 114	eqtr2d 2834	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 = ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)))
116	115	ad4ant23 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)))
117	116	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))
118	95, 117	oveq12d 7153	. . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . 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 232	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
121		eqcom 2805	. . . . . . . . . . . . . . 15 ⊢ ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = (𝑥‘𝑖))
122		elmapi 8411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ↑_m (1...𝑁)) → 𝑥:(1...𝑁)⟶ℝ)
123	122	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) → 𝑥:(1...𝑁)⟶ℝ)
124	123	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑥:(1...𝑁)⟶ℝ)
125	124	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑥:(1...𝑁)⟶ℝ)
126	125	ffvelrnda 6828	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
127	126	recnd 10658	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
128		1cnd 10625	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ)
129	11	ad4ant23 752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
130	128, 129	subcld 10986	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
131	58	ad4ant23 752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ≠ 𝑡)
132	128, 129, 131	subne0d 10995	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ≠ 0)
133	130, 132	reccld 11398	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 − 𝑡)) ∈ ℂ)
134	128, 133	subcld 10986	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
135		eldifi 4054	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥}) → 𝑦 ∈ (ℝ ↑_m (1...𝑁)))
136		elmapi 8411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ℝ ↑_m (1...𝑁)) → 𝑦:(1...𝑁)⟶ℝ)
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥}) → 𝑦:(1...𝑁)⟶ℝ)
138	137	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) → 𝑦:(1...𝑁)⟶ℝ)
139	138	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑦:(1...𝑁)⟶ℝ)
140	139	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑦:(1...𝑁)⟶ℝ)
141	140	ffvelrnda 6828	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
142	141	recnd 10658	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
143	134, 142	mulcld 10650	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) ∈ ℂ)
144	62	ad4ant23 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1 − 𝑡)))) ∈ ℂ)
145		elmapi 8411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ (ℝ ↑_m (1...𝑁)) → 𝑝:(1...𝑁)⟶ℝ)
146	145	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) → 𝑝:(1...𝑁)⟶ℝ)
147	146	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑝:(1...𝑁)⟶ℝ)
148	147	ffvelrnda 6828	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
149	148	recnd 10658	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
150	144, 149	mulcld 10650	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ∈ ℂ)
151	127, 143, 150	subadd2d 11005	. . . . . . . . . . . . . . 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 293	. . . . . . . . . . . . . 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 2805	. . . . . . . . . . . . . . 15 ⊢ (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ↔ ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
154	127, 143	subcld 10986	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ∈ ℂ)
155	89	ad4ant23 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1 − 𝑡)))) ≠ 0)
156	154, 144, 149, 155	divmuld 11427	. . . . . . . . . . . . . . . 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 2805	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))))
158	127, 143, 144, 155	divsubdird 11444	. . . . . . . . . . . . . . . . . . 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 11405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
160	143, 144, 155	divcld 11405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
161	159, 160	negsubd 10992	. . . . . . . . . . . . . . . . . . 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 11409	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
163	143, 144, 155	divneg2d 11419	. . . . . . . . . . . . . . . . . . . . 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 11002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 − (1 / (1 − 𝑡)))) = ((1 − (1 / (1 − 𝑡))) − 1))
165	164	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . 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 10986	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ∈ ℂ)
167	88	necomd 3042	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ≠ 1)
168	63, 22, 167	subne0d 10995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) − 1) ≠ 0)
169	168	ad4ant23 752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ≠ 0)
170	134, 142, 166, 169	div23d 11442	. . . . . . . . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . . . . . . 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 7153	. . . . . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . . . 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	syl5bb 286	. . . . . . . . . . . . . . . 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 284	. . . . . . . . . . . . . . 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	syl5bb 286	. . . . . . . . . . . . . 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 282	. . . . . . . . . . . . 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 262	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
180	179	ralimdva 3144	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
181	180	imp 410	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
182	49, 56, 181	rspcedvd 3574	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))
183	182	3mix2d 1334	. . . . . . . 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 423	. . . . . . 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 410	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (𝑡 < 0 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
187		simpr 488	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
188		oveq2 7143	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑡 → (1 − 𝑘) = (1 − 𝑡))
189	188	oveq1d 7150	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → ((1 − 𝑘) · (𝑥‘𝑖)) = ((1 − 𝑡) · (𝑥‘𝑖)))
190		oveq1 7142	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → (𝑘 · (𝑦‘𝑖)) = (𝑡 · (𝑦‘𝑖)))
191	189, 190	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑡 → (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
192	191	eqeq2d 2809	. . . . . . . . . 10 ⊢ (𝑘 = 𝑡 → ((𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
193	192	ralbidv 3162	. . . . . . . . 9 ⊢ (𝑘 = 𝑡 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
194	193	adantl 485	. . . . . . . 8 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) ∧ 𝑘 = 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
195		simplr 768	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
196	187, 194, 195	rspcedvd 3574	. . . . . . 7 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))))
197	196	3mix1d 1333	. . . . . 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 416	. . . . 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 10631	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 ∈ ℝ)
200		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
201		0red 10633	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 ∈ ℝ)
202	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 1)
203		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 < 𝑡)
204	201, 199, 200, 202, 203	lttrd 10790	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 𝑡)
205	204	gt0ne0d 11193	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ≠ 0)
206	199, 200, 205	redivcld 11457	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ∈ ℝ)
207	200, 204	recgt0d 11563	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < (1 / 𝑡))
208		recgt1i 11526	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1))
209	206	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ∈ ℝ)
210		1red 10631	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → 1 ∈ ℝ)
211		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) < 1)
212	209, 210, 211	ltled 10777	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ≤ 1)
213	208, 212	mpdan 686	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ≤ 1)
214	206, 207, 213	3jca 1125	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → ((1 / 𝑡) ∈ ℝ ∧ 0 < (1 / 𝑡) ∧ (1 / 𝑡) ≤ 1))
215		1re 10630	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
216	6, 215	pm3.2i 474	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ^* ∧ 1 ∈ ℝ)
217		elioc2 12788	. . . . . . . . . . . . 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 260	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ∈ (0(,]1))
220	219	ad4ant23 752	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / 𝑡) ∈ (0(,]1))
221		oveq2 7143	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (1 / 𝑡) → (1 − 𝑚) = (1 − (1 / 𝑡)))
222	221	oveq1d 7150	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → ((1 − 𝑚) · (𝑥‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
223		oveq1 7142	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → (𝑚 · (𝑝‘𝑖)) = ((1 / 𝑡) · (𝑝‘𝑖)))
224	222, 223	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ (𝑚 = (1 / 𝑡) → (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))
225	224	eqeq2d 2809	. . . . . . . . . . . 12 ⊢ (𝑚 = (1 / 𝑡) → ((𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
226	225	ralbidv 3162	. . . . . . . . . . 11 ⊢ (𝑚 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
227	226	adantl 485	. . . . . . . . . 10 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑚 = (1 / 𝑡)) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
228		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
229	228	recnd 10658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ∈ ℂ)
230	229	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
231	204	ex 416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → (1 < 𝑡 → 0 < 𝑡))
232		gt0ne0 11094	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → 𝑡 ≠ 0)
233	232	ex 416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℝ → (0 < 𝑡 → 𝑡 ≠ 0))
234	231, 233	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ ℝ → (1 < 𝑡 → 𝑡 ≠ 0))
235	234	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (1 < 𝑡 → 𝑡 ≠ 0))
236	235	imp 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ≠ 0)
237	236	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
238	230, 237	reccld 11398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ∈ ℂ)
239		1cnd 10625	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ)
240	230, 237	recne0d 11399	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ≠ 0)
241	238, 239, 238, 240	divsubdird 11444	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) = (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))))
242	238, 240	dividd 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) / (1 / 𝑡)) = 1)
243	230, 237	recrecd 11402	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) = 𝑡)
244	242, 243	oveq12d 7153	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))) = (1 − 𝑡))
245	241, 244	eqtr2d 2834	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (((1 / 𝑡) − 1) / (1 / 𝑡)))
246	245	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
247	229, 236	recrecd 11402	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → (1 / (1 / 𝑡)) = 𝑡)
248	247	eqcomd 2804	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 = (1 / (1 / 𝑡)))
249	248	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = (1 / (1 / 𝑡)))
250	249	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
251	246, 250	oveq12d 7153	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
252	251	eqeq2d 2809	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
253	252	biimpd 232	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
254		eqcom 2805	. . . . . . . . . . . . . . 15 ⊢ ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖))
255	139	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑦:(1...𝑁)⟶ℝ)
256	255	ffvelrnda 6828	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
257	256	recnd 10658	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
258	239, 238	subcld 10986	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / 𝑡)) ∈ ℂ)
259	124	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑥:(1...𝑁)⟶ℝ)
260	259	ffvelrnda 6828	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
261	260	recnd 10658	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
262	258, 261	mulcld 10650	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ)
263	146	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑝:(1...𝑁)⟶ℝ)
264	263	ffvelrnda 6828	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
265	264	recnd 10658	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
266	238, 265	mulcld 10650	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) · (𝑝‘𝑖)) ∈ ℂ)
267	257, 262, 266	subaddd 11004	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖)))
268	254, 267	bitr4id 293	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖))))
269		eqcom 2805	. . . . . . . . . . . . . . 15 ⊢ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))))
270	257, 262	subcld 10986	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) ∈ ℂ)
271	270, 238, 265, 240	divmuld 11427	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))))
272	269, 271	bitr4id 293	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖)))
273		eqcom 2805	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)))
274	257, 262, 238, 240	divsubdird 11444	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
275	257, 238, 240	divcld 11405	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) ∈ ℂ)
276	262, 238, 240	divcld 11405	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) ∈ ℂ)
277	275, 276	negsubd 10992	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
278	262, 238, 240	divnegd 11418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
279	258, 261	mulneg1d 11082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = -((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
280	279	eqcomd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -((1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)))
281	280	oveq1d 7150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
282	239, 238	negsubdi2d 11002	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 / 𝑡)) = ((1 / 𝑡) − 1))
283	282	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (((1 / 𝑡) − 1) · (𝑥‘𝑖)))
284	283	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)))
285	238, 239	subcld 10986	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) − 1) ∈ ℂ)
286	285, 261, 238, 240	div23d 11442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
287	284, 286	eqtrd 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
288	278, 281, 287	3eqtrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
289	288	oveq2d 7151	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
290	257, 238, 240	divrec2d 11409	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
291	290	oveq1d 7150	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
292	238, 240	reccld 11398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) ∈ ℂ)
293	292, 257	mulcld 10650	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / (1 / 𝑡)) · (𝑦‘𝑖)) ∈ ℂ)
294	285, 238, 240	divcld 11405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) ∈ ℂ)
295	294, 261	mulcld 10650	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ)
296	293, 295	addcomd 10831	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
297	289, 291, 296	3eqtrd 2837	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
298	274, 277, 297	3eqtr2d 2839	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
299	298	eqeq2d 2809	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
300	273, 299	syl5bb 286	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
301	268, 272, 300	3bitrd 308	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
302	253, 301	sylibrd 262	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
303	302	ralimdva 3144	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
304	303	imp 410	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))
305	220, 227, 304	rspcedvd 3574	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑_m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑_m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑_m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))
306	305	3mix3d 1335	. . . . . . . 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 423	. . . . . . 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 410	. . . . 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 1425	. . . 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 416	. . 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 3243	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 209 ∧ wa 399 ∨ w3o 1083 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 ∖ cdif 3878 {csn 4525 class class class wbr 5030 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ↑_m cmap 8389 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 · cmul 10531 ℝ^*cxr 10663 < clt 10664 ≤ cle 10665 − cmin 10859 -cneg 10860 / cdiv 11286 ℕcn 11625 ℝ⁺crp 12377 (,]cioc 12727 [,)cico 12728 [,]cicc 12729 ...cfz 12885

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-1st 7671 df-2nd 7672 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-rp 12378 df-ioc 12731 df-ico 12732 df-icc 12733

This theorem is referenced by: eenglngeehlnm 45153

W3C validator