Theorem eenglngeehlnmlem2 47734

Description: Lemma 2 for eenglngeehlnm 47735. (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 11239	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
2		1red 11237	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
3		simpr 484	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
4		reorelicc 47706	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
5	1, 2, 3, 4	syl3anc 1369	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡))
6		0xr 11283	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ*
7	6	a1i 11	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ∈ ℝ*)
8		1xr 11295	. . . . . . . . . . . 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 11264	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈ ℂ)
12		0red 11239	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℝ)
13		1red 11237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℝ)
14		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 0)
15		0lt1 11758	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
16	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < 1)
17	10, 12, 13, 14, 16	lttrd 11397	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 1)
18	10, 17	ltned 11372	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ 1)
19		1subrec1sub 47701	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 1) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
20	11, 18, 19	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (𝑡 / (𝑡 − 1)))
21	10, 13	resubcld 11664	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℝ)
22		1cnd 11231	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈ ℂ)
23	11, 22, 18	subne0d 11602	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 0)
24	10, 21, 23	redivcld 12064	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ)
25	24	rexrd 11286	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ*)
26	20, 25	eqeltrd 2828	. . . . . . . . . . . 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 11663	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -𝑡 ∈ ℝ)
29	10, 13	sublt0d 11862	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) < 0 ↔ 𝑡 < 1))
30	17, 29	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) < 0)
31	21, 30	negelrpd 13032	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -(𝑡 − 1) ∈ ℝ+)
32	10, 12, 14	ltled 11384	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≤ 0)
33	10	le0neg1d 11807	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 ≤ 0 ↔ 0 ≤ -𝑡))
34	32, 33	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ -𝑡)
35	28, 31, 34	divge0d 13080	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (-𝑡 / -(𝑡 − 1)))
36	21	recnd 11264	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈ ℂ)
37	11, 36, 23	div2negd 12027	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (-𝑡 / -(𝑡 − 1)) = (𝑡 / (𝑡 − 1)))
38	20, 37	eqtr4d 2770	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) = (-𝑡 / -(𝑡 − 1)))
39	35, 38	breqtrrd 5170	. . . . . . . . . . . 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 11237	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈ ℝ)
42	13, 10	resubcld 11664	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ)
43	10, 13	posdifd 11823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 < 1 ↔ 0 < (1 − 𝑡)))
44	17, 43	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < (1 − 𝑡))
45	42, 44	elrpd 13037	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℝ+)
46	45	ad4ant23 752	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − 𝑡) ∈ ℝ+)
47	46	rpreccld 13050	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / (1 − 𝑡)) ∈ ℝ+)
48	41, 47	ltsubrpd 13072	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) < 1)
49	7, 9, 27, 40, 48	elicod 13398	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈ (0[,)1))
50		oveq2 7422	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (1 − 𝑙) = (1 − (1 − (1 / (1 − 𝑡)))))
51	50	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → ((1 − 𝑙) · (𝑝‘𝑖)) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)))
52		oveq1 7421	. . . . . . . . . . . . . 14 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (𝑙 · (𝑦‘𝑖)) = ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))
53	51, 52	oveq12d 7432	. . . . . . . . . . . . 13 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
54	53	eqeq2d 2738	. . . . . . . . . . . 12 ⊢ (𝑙 = (1 − (1 / (1 − 𝑡))) → ((𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))))
55	54	ralbidv 3172	. . . . . . . . . . 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 11593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈ ℂ)
58	10, 17	gtned 11371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 𝑡)
59	22, 11, 58	subne0d 11602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ≠ 0)
60	57, 59	reccld 12005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 / (1 − 𝑡)) ∈ ℂ)
61	22, 60	nncand 11598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) = (1 / (1 − 𝑡)))
62	61, 60	eqeltrd 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ∈ ℂ)
63	22, 60	subcld 11593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
64	16	gt0ne0d 11800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 0)
65	36, 11	subeq0ad 11603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ (𝑡 − 1) = 𝑡))
66	11, 22, 11	sub32d 11625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) − 𝑡) = ((𝑡 − 𝑡) − 1))
67	66	eqeq1d 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ ((𝑡 − 𝑡) − 1) = 0))
68	11	subidd 11581	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 𝑡) = 0)
69	68	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 𝑡) − 1) = (0 − 1))
70	69	eqeq1d 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 𝑡) − 1) = 0 ↔ (0 − 1) = 0))
71		0cnd 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈ ℂ)
72	71, 22, 71	subaddd 11611	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) = 0 ↔ (1 + 0) = 0))
73	22	addridd 11436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 + 0) = 1)
74	73	eqeq1d 2729	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2980	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) ≠ 𝑡 ↔ 1 ≠ 0))
79	64, 78	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 𝑡)
80	20	eqeq2d 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ 1 = (𝑡 / (𝑡 − 1))))
81		eqcom 2734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 = (𝑡 / (𝑡 − 1)) ↔ (𝑡 / (𝑡 − 1)) = 1)
82	11, 36, 22, 23	divmuld 12034	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) = 1 ↔ ((𝑡 − 1) · 1) = 𝑡))
83	81, 82	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (𝑡 / (𝑡 − 1)) ↔ ((𝑡 − 1) · 1) = 𝑡))
84	36	mulridd 11253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) · 1) = (𝑡 − 1))
85	84	eqeq1d 2729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) · 1) = 𝑡 ↔ (𝑡 − 1) = 𝑡))
86	80, 83, 85	3bitrd 305	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) = 𝑡))
87	86	necon3bid 2980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 ≠ (1 − (1 / (1 − 𝑡))) ↔ (𝑡 − 1) ≠ 𝑡))
88	79, 87	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ (1 − (1 / (1 − 𝑡))))
89	22, 63, 88	subne0d 11602	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 − (1 / (1 − 𝑡)))) ≠ 0)
90	61	oveq1d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = ((1 / (1 − 𝑡)) · (1 − 𝑡)))
91	57, 59	recid2d 12008	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 / (1 − 𝑡)) · (1 − 𝑡)) = 1)
92	90, 91	eqtrd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 − (1 / (1 − 𝑡)))) · (1 − 𝑡)) = 1)
93	62, 57, 89, 92	mvllmuld 12068	. . . . . . . . . . . . . . . . . 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 7429	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
96	20	oveq1d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) − 1) = ((𝑡 / (𝑡 − 1)) − 1))
97	20, 96	oveq12d 7432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) = ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)))
98		subdivcomb2 11932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((𝑡 − 1) ∈ ℂ ∧ (𝑡 − 1) ≠ 0)) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
99	11, 22, 36, 23, 98	syl112anc 1372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1))
100	84	oveq2d 7430	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = (𝑡 − (𝑡 − 1)))
101	11, 22	nncand 11598	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − (𝑡 − 1)) = 1)
102	100, 101	eqtrd 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = 1)
103	102	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = (1 / (𝑡 − 1)))
104	99, 103	eqtr3d 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) = (1 / (𝑡 − 1)))
105	104	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = ((1 / (𝑡 − 1)) · 𝑡))
106	11, 36, 23	divrec2d 12016	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) = ((1 / (𝑡 − 1)) · 𝑡))
107	105, 106	eqtr4d 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1)))
108	20, 63	eqeltrrd 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℂ)
109	108, 22	subcld 11593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ∈ ℂ)
110	79	necomd 2991	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ (𝑡 − 1))
111	11, 36, 23, 110	divne1d 12023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ≠ 1)
112	108, 22, 111	subne0d 11602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ≠ 0)
113	108, 109, 11, 112	divmuld 12034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡 ↔ (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1))))
114	107, 113	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡)
115	97, 114	eqtr2d 2768	. . . . . . . . . . . . . . . . . 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 7429	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))
118	95, 117	oveq12d 7432	. . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . 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 228	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖)))))
121		eqcom 2734	. . . . . . . . . . . . . . 15 ⊢ ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = (𝑥‘𝑖))
122		elmapi 8859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℝ ↑m (1...𝑁)) → 𝑥:(1...𝑁)⟶ℝ)
123	122	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) → 𝑥:(1...𝑁)⟶ℝ)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) → 𝑥:(1...𝑁)⟶ℝ)
125	124	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑥:(1...𝑁)⟶ℝ)
126	125	ffvelcdmda 7088	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
127	126	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
128		1cnd 11231	. . . . . . . . . . . . . . . . . 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 11593	. . . . . . . . . . . . . . . . . . 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 11602	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ≠ 0)
133	130, 132	reccld 12005	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 − 𝑡)) ∈ ℂ)
134	128, 133	subcld 11593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / (1 − 𝑡))) ∈ ℂ)
135		eldifi 4122	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥}) → 𝑦 ∈ (ℝ ↑m (1...𝑁)))
136		elmapi 8859	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ℝ ↑m (1...𝑁)) → 𝑦:(1...𝑁)⟶ℝ)
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥}) → 𝑦:(1...𝑁)⟶ℝ)
138	137	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) → 𝑦:(1...𝑁)⟶ℝ)
139	138	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) → 𝑦:(1...𝑁)⟶ℝ)
140	139	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑦:(1...𝑁)⟶ℝ)
141	140	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
142	141	recnd 11264	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
143	134, 142	mulcld 11256	. . . . . . . . . . . . . . . 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 8859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ (ℝ ↑m (1...𝑁)) → 𝑝:(1...𝑁)⟶ℝ)
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) → 𝑝:(1...𝑁)⟶ℝ)
147	146	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑝:(1...𝑁)⟶ℝ)
148	147	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
149	148	recnd 11264	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
150	144, 149	mulcld 11256	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ∈ ℂ)
151	127, 143, 150	subadd2d 11612	. . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . 15 ⊢ (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) ↔ ((1 − (1 − (1 / (1 − 𝑡)))) · (𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))
154	127, 143	subcld 11593	. . . . . . . . . . . . . . . . 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 12034	. . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 − 𝑡))))))
158	127, 143, 144, 155	divsubdird 12051	. . . . . . . . . . . . . . . . . . 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 12012	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
160	143, 144, 155	divcld 12012	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 − 𝑡))))) ∈ ℂ)
161	159, 160	negsubd 11599	. . . . . . . . . . . . . . . . . . 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 12016	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 − 𝑡))))) = ((1 / (1 − (1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)))
163	143, 144, 155	divneg2d 12026	. . . . . . . . . . . . . . . . . . . . 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 11609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 − (1 / (1 − 𝑡)))) = ((1 − (1 / (1 − 𝑡))) − 1))
165	164	oveq2d 7430	. . . . . . . . . . . . . . . . . . . . 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 11593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ∈ ℂ)
167	88	necomd 2991	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 / (1 − 𝑡))) ≠ 1)
168	63, 22, 167	subne0d 11602	. . . . . . . . . . . . . . . . . . . . . . 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 12049	. . . . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . . . . 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 7432	. . . . . . . . . . . . . . . . . . 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 2773	. . . . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . . . . 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 3162	. . . . . . . . . . 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 3609	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))
183	182	3mix2d 1335	. . . . . . . 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 7422	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑡 → (1 − 𝑘) = (1 − 𝑡))
189	188	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → ((1 − 𝑘) · (𝑥‘𝑖)) = ((1 − 𝑡) · (𝑥‘𝑖)))
190		oveq1 7421	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑡 → (𝑘 · (𝑦‘𝑖)) = (𝑡 · (𝑦‘𝑖)))
191	189, 190	oveq12d 7432	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑡 → (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
192	191	eqeq2d 2738	. . . . . . . . . 10 ⊢ (𝑘 = 𝑡 → ((𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))))
193	192	ralbidv 3172	. . . . . . . . 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 768	. . . . . . . 8 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))
196	187, 194, 195	rspcedvd 3609	. . . . . . 7 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))))
197	196	3mix1d 1334	. . . . . 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 11237	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 ∈ ℝ)
200		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
201		0red 11239	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 ∈ ℝ)
202	15	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 1)
203		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 1 < 𝑡)
204	201, 199, 200, 202, 203	lttrd 11397	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < 𝑡)
205	204	gt0ne0d 11800	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 𝑡 ≠ 0)
206	199, 200, 205	redivcld 12064	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ∈ ℝ)
207	200, 204	recgt0d 12170	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → 0 < (1 / 𝑡))
208		recgt1i 12133	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1))
209	206	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ∈ ℝ)
210		1red 11237	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → 1 ∈ ℝ)
211		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) < 1)
212	209, 210, 211	ltled 11384	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 1 < 𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ≤ 1)
213	208, 212	mpdan 686	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → (1 / 𝑡) ≤ 1)
214	206, 207, 213	3jca 1126	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ 1 < 𝑡) → ((1 / 𝑡) ∈ ℝ ∧ 0 < (1 / 𝑡) ∧ (1 / 𝑡) ≤ 1))
215		1re 11236	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
216	6, 215	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ* ∧ 1 ∈ ℝ)
217		elioc2 13411	. . . . . . . . . . . . 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 752	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / 𝑡) ∈ (0(,]1))
221		oveq2 7422	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (1 / 𝑡) → (1 − 𝑚) = (1 − (1 / 𝑡)))
222	221	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → ((1 − 𝑚) · (𝑥‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
223		oveq1 7421	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (1 / 𝑡) → (𝑚 · (𝑝‘𝑖)) = ((1 / 𝑡) · (𝑝‘𝑖)))
224	222, 223	oveq12d 7432	. . . . . . . . . . . . 13 ⊢ (𝑚 = (1 / 𝑡) → (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))
225	224	eqeq2d 2738	. . . . . . . . . . . 12 ⊢ (𝑚 = (1 / 𝑡) → ((𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))))
226	225	ralbidv 3172	. . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑡 ∈ ℝ)
229	228	recnd 11264	. . . . . . . . . . . . . . . . . . . . 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 11701	. . . . . . . . . . . . . . . . . . . . . . . . 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 12005	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ∈ ℂ)
239		1cnd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ)
240	230, 237	recne0d 12006	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ≠ 0)
241	238, 239, 238, 240	divsubdird 12051	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) = (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))))
242	238, 240	dividd 12010	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) / (1 / 𝑡)) = 1)
243	230, 237	recrecd 12009	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) = 𝑡)
244	242, 243	oveq12d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))) = (1 − 𝑡))
245	241, 244	eqtr2d 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (((1 / 𝑡) − 1) / (1 / 𝑡)))
246	245	oveq1d 7429	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
247	229, 236	recrecd 12009	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → (1 / (1 / 𝑡)) = 𝑡)
248	247	eqcomd 2733	. . . . . . . . . . . . . . . . . 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 7429	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
251	246, 250	oveq12d 7432	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
252	251	eqeq2d 2738	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
253	252	biimpd 228	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))))
254		eqcom 2734	. . . . . . . . . . . . . . 15 ⊢ ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖))
255	139	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) → 𝑦:(1...𝑁)⟶ℝ)
256	255	ffvelcdmda 7088	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
257	256	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
258	239, 238	subcld 11593	. . . . . . . . . . . . . . . . 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	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
261	260	recnd 11264	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
262	258, 261	mulcld 11256	. . . . . . . . . . . . . . . 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	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
265	264	recnd 11264	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
266	238, 265	mulcld 11256	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) · (𝑝‘𝑖)) ∈ ℂ)
267	257, 262, 266	subaddd 11611	. . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . 15 ⊢ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))))
270	257, 262	subcld 11593	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) ∈ ℂ)
271	270, 238, 265, 240	divmuld 12034	. . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)))
274	257, 262, 238, 240	divsubdird 12051	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
275	257, 238, 240	divcld 12012	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) ∈ ℂ)
276	262, 238, 240	divcld 12012	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) ∈ ℂ)
277	275, 276	negsubd 11599	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))))
278	262, 238, 240	divnegd 12025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
279	258, 261	mulneg1d 11689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = -((1 − (1 / 𝑡)) · (𝑥‘𝑖)))
280	279	eqcomd 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -((1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)))
281	280	oveq1d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))
282	239, 238	negsubdi2d 11609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 / 𝑡)) = ((1 / 𝑡) − 1))
283	282	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (((1 / 𝑡) − 1) · (𝑥‘𝑖)))
284	283	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)))
285	238, 239	subcld 11593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) − 1) ∈ ℂ)
286	285, 261, 238, 240	div23d 12049	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
287	284, 286	eqtrd 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
288	278, 281, 287	3eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))
289	288	oveq2d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
290	257, 238, 240	divrec2d 12016	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))
291	290	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))))
292	238, 240	reccld 12005	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) ∈ ℂ)
293	292, 257	mulcld 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / (1 / 𝑡)) · (𝑦‘𝑖)) ∈ ℂ)
294	285, 238, 240	divcld 12012	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) ∈ ℂ)
295	294, 261	mulcld 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ)
296	293, 295	addcomd 11438	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
297	289, 291, 296	3eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
298	274, 277, 297	3eqtr2d 2773	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))
299	298	eqeq2d 2738	. . . . . . . . . . . . . . 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 3162	. . . . . . . . . . 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 3609	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 < 𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))
306	305	3mix3d 1336	. . . . . . . 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 1426	. . . 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 3150	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m (1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m (1...𝑁))) → (∃𝑡 ∈ ℝ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ w3o 1084   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   ≠ wne 2935  ∀wral 3056  ∃wrex 3065   ∖ cdif 3941  {csn 4624   class class class wbr 5142  ⟶wf 6538  ‘cfv 6542  (class class class)co 7414   ↑_m cmap 8836  ℂcc 11128  ℝcr 11129  0cc0 11130  1c1 11131   + caddc 11133   · cmul 11135  ℝ^*cxr 11269   < clt 11270   ≤ cle 11271   − cmin 11466  -cneg 11467   / cdiv 11893  ℕcn 12234  ℝ⁺crp 12998  (,]cioc 13349  [,)cico 13350  [,]cicc 13351  ...cfz 13508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-po 5584  df-so 5585  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-er 8718  df-map 8838  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-rp 12999  df-ioc 13353  df-ico 13354  df-icc 13355

This theorem is referenced by:  eenglngeehlnm  47735