Theorem axcontlem2 28203

Description: Lemma for axcont 28214. The idea here is to set up a mapping 𝐹 that will allow to transfer dedekind 11373 to two sets of points. Here, we set up 𝐹 and show its domain and codomain. (Contributed by Scott Fenton, 17-Jun-2013.)

Hypotheses

Ref	Expression
axcontlem2.1	⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
axcontlem2.2	⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}

Assertion

Ref	Expression
axcontlem2	⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹:𝐷–1-1-onto→(0[,)+∞))

Distinct variable groups:   𝑍,𝑝,𝑥,𝑡,𝑖   𝑈,𝑝,𝑥,𝑡,𝑖   𝑁,𝑝,𝑥,𝑡,𝑖   𝑥,𝐷,𝑡

Allowed substitution hints:   𝐷(𝑖,𝑝)   𝐹(𝑥,𝑡,𝑖,𝑝)

Proof of Theorem axcontlem2

Dummy variables 𝑘 𝑦 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq2 4873	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
2	1	breq2d 5159	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3		breq1 5150	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
4	2, 3	orbi12d 918	. . . . . . . 8 ⊢ (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5		axcontlem2.1	. . . . . . . 8 ⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
6	4, 5	elrab2 3685	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7		simpll3 1215	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8		simpll2 1214	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9		simpr 486	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10		brbtwn 28137	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
11	7, 8, 9, 10	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
12	11	biimpa 478	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))
13		simp-4r 783	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑍 ≠ 𝑈)
14		oveq2 7412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15		1m0e1 12329	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 0) = 1
16	14, 15	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 0 → (1 − 𝑠) = 1)
17	16	oveq1d 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → ((1 − 𝑠) · (𝑍‘𝑖)) = (1 · (𝑍‘𝑖)))
18		oveq1 7411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → (𝑠 · (𝑥‘𝑖)) = (0 · (𝑥‘𝑖)))
19	17, 18	oveq12d 7422	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 0 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
20	19	eqeq2d 2744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 0 → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
21	20	ralbidv 3178	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
22	21	biimpac 480	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
23		eqcom 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑍 = 𝑈 ↔ 𝑈 = 𝑍)
24	7	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
25	8	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26		eqeefv 28141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
27	24, 25, 26	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
28	8	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29		fveecn 28140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
30	28, 29	sylancom 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
31		fveecn 28140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
32	31	ad4ant24 753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
33		mullid 11209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → (1 · (𝑍‘𝑖)) = (𝑍‘𝑖))
34		mul02 11388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 · (𝑥‘𝑖)) = 0)
35	33, 34	oveqan12d 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = ((𝑍‘𝑖) + 0))
36		addrid 11390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
37	36	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
38	35, 37	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = (𝑍‘𝑖))
39	38	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
40	30, 32, 39	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
41	40	ralbidva 3176	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
42	27, 41	bitr4d 282	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
43	23, 42	bitrid 283	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
44	22, 43	imbitrrid 245	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
45	44	expdimp 454	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
46	45	necon3d 2962	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑍 ≠ 𝑈 → 𝑠 ≠ 0))
47	13, 46	mpd 15	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑠 ≠ 0)
48		elicc01 13439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1))
49	48	simp1bi 1146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
50		rereccl 11928	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
51	49, 50	sylan 581	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
52	49	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
53	48	simp2bi 1147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
54	53	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
55		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
56	52, 54, 55	ne0gt0d 11347	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
57		1re 11210	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
58		0le1 11733	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 1
59		divge0 12079	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
60	57, 58, 59	mpanl12 701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
61	52, 56, 60	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
62		elrege0 13427	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
63	51, 61, 62	sylanbrc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
64	63	adantll 713	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
65	49	ad3antlr 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
66	65	recnd 11238	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
67		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
68	31	ad5ant25 761	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
69	8	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
70	69, 29	sylancom 589	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
71		ax-1cn 11164	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℂ
72		reccl 11875	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
73		subcl 11455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
74	71, 72, 73	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
75	74	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
76		subcl 11455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
77	71, 76	mpan 689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
78	77	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
79	72, 78	mulcld 11230	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
80	79	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
81		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
82	75, 80, 81	adddird 11235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))))
83		simpl 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
84		subdi 11643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
85	71, 84	mp3an2 1450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
86	72, 83, 85	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
87	86	oveq2d 7420	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
88	72	mulridd 11227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
89		recid2 11883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
90	88, 89	oveq12d 7422	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
91	90	oveq2d 7420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
92		addsubass 11466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
93	71, 92	mp3an3 1451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
94	74, 72, 93	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
95	74, 72	addcld 11229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
96		npcan 11465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
97	71, 72, 96	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
98	95, 97	subeq0bd 11636	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
99	91, 94, 98	3eqtr2d 2779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
100	87, 99	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
101	100	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
102	101	oveq1d 7419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
103	72	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
104	77	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
105	103, 104, 81	mulassd 11233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))))
106	105	oveq2d 7420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))))
107	82, 102, 106	3eqtr3rd 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = (0 · (𝑍‘𝑖)))
108		mul02 11388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍‘𝑖) ∈ ℂ → (0 · (𝑍‘𝑖)) = 0)
109	108	ad2antll 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
110	107, 109	eqtrd 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = 0)
111		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
112		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) ∈ ℂ)
113	103, 111, 112	mulassd 11233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))
114	89	oveq1d 7419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (1 · (𝑥‘𝑖)))
115		mullid 11209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥‘𝑖) ∈ ℂ → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
116	115	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
117	114, 116	sylan9eq 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (𝑥‘𝑖))
118	113, 117	eqtr3d 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) = (𝑥‘𝑖))
119	110, 118	oveq12d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (0 + (𝑥‘𝑖)))
120	75, 81	mulcld 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍‘𝑖)) ∈ ℂ)
121		simpr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
122		mulcl 11190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
123	78, 121, 122	syl2an 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
124	103, 123	mulcld 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) ∈ ℂ)
125		mulcl 11190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
126	125	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
127	103, 126	mulcld 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) ∈ ℂ)
128	120, 124, 127	addassd 11232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
129	103, 123, 126	adddid 11234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))))
130	129	oveq2d 7420	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
131	128, 130	eqtr4d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
132		addlid 11393	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
133	132	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
134	119, 131, 133	3eqtr3rd 2782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
135	66, 67, 68, 70, 134	syl22anc 838	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
136	135	ralrimiva 3147	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
137		oveq2 7412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
138	137	oveq1d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − (1 / 𝑠)) · (𝑍‘𝑖)))
139		oveq1 7411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
140	138, 139	oveq12d 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
141	140	eqeq2d 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (1 / 𝑠) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
142	141	ralbidv 3178	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
143	142	rspcev 3612	. . . . . . . . . . . . . . 15 ⊢ (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
144	64, 136, 143	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
145		oveq2 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (𝑡 · (𝑈‘𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
146	145	oveq2d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
147	146	eqeq2d 2744	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
148	147	ralimi 3084	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
149		ralbi 3104	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
150	148, 149	syl 17	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
151	150	rexbidv 3179	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
152	144, 151	syl5ibrcom 246	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
153	152	impancom 453	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑠 ≠ 0 → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
154	47, 153	mpd 15	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
155	154	r19.29an 3159	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
156	12, 155	syldan 592	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
157		3simpa 1149	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
158		elicc01 13439	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
159		elrege0 13427	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
160	157, 158, 159	3imtr4i 292	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
161	160	ssriv 3985	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ (0[,)+∞)
162		brbtwn 28137	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
163	9, 8, 7, 162	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
164	163	biimpa 478	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
165		ssrexv 4050	. . . . . . . . . 10 ⊢ ((0[,]1) ⊆ (0[,)+∞) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
166	161, 164, 165	mpsyl 68	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
167	156, 166	jaodan 957	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
168	167	anasss 468	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
169	6, 168	sylan2b 595	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
170		r19.26 3112	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
171		eqtr2 2757	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
172	171	ralimi 3084	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
173	170, 172	sylbir 234	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
174		elrege0 13427	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
175	174	simplbi 499	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
176	175	recnd 11238	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
177		elrege0 13427	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
178	177	simplbi 499	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
179	178	recnd 11238	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
180	176, 179	anim12i 614	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
181		simplr 768	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
182		simpl2 1193	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑍 ∈ (𝔼‘𝑁))
183	182	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
184	183, 29	sylancom 589	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
185		simpl3 1194	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑈 ∈ (𝔼‘𝑁))
186	185	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
187		fveecn 28140	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
188	186, 187	sylancom 589	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
189		subcl 11455	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
190	71, 189	mpan 689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
191	190	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
192		simpl 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
193		mulcl 11190	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑡) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
194	191, 192, 193	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
195		mulcl 11190	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
196	195	ad2ant2rl 748	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
197	77	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
198	197, 192, 122	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
199		mulcl 11190	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
200	199	ad2ant2l 745	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
201	194, 196, 198, 200	addsubeq4d 11618	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
202		nnncan1 11492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
203	71, 202	mp3an1 1449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
204	203	ancoms 460	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
205	204	oveq1d 7419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
206	205	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
207	77	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
208	190	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
209		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
210	207, 208, 209	subdird 11667	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
211	206, 210	eqtr3d 2775	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
212		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
213		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
214		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
215	212, 213, 214	subdird 11667	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑈‘𝑖)) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖))))
216	211, 215	eqeq12d 2749	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
217		subcl 11455	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡 − 𝑠) ∈ ℂ)
218	217	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 − 𝑠) ∈ ℂ)
219		mulcan1g 11863	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
220	218, 209, 214, 219	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
221	201, 216, 220	3bitr2d 307	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
222	181, 184, 188, 221	syl12anc 836	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
223	222	ralbidva 3176	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
224		r19.32v 3192	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
225		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ≠ 𝑈)
226	225	neneqd 2946	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
227		simpll2 1214	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
228		simpll3 1215	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
229		eqeefv 28141	. . . . . . . . . . . . . . . 16 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
230	227, 228, 229	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
231	226, 230	mtbid 324	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))
232		orel2 890	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
233	231, 232	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
234		subeq0 11482	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
235	234	adantl 483	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
236	233, 235	sylibd 238	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
237	224, 236	biimtrid 241	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
238	223, 237	sylbid 239	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠))
239	180, 238	sylan2 594	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠))
240	173, 239	syl5 34	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
241	240	ralrimivva 3201	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
242	241	adantr 482	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
243		oveq2 7412	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
244	243	oveq1d 7419	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑖)))
245		oveq1 7411	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → (𝑡 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑖)))
246	244, 245	oveq12d 7422	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
247	246	eqeq2d 2744	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
248	247	ralbidv 3178	. . . . . . 7 ⊢ (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
249	248	reu4 3726	. . . . . 6 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠)))
250	169, 242, 249	sylanbrc 584	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
251		df-reu 3378	. . . . 5 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
252	250, 251	sylib 217	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
253	252	ralrimiva 3147	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
254		axcontlem2.2	. . . 4 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
255	254	fnopabg 6684	. . 3 ⊢ (∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ 𝐹 Fn 𝐷)
256	253, 255	sylib 217	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹 Fn 𝐷)
257	175	ad2antlr 726	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
258	182	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
259		fveere 28139	. . . . . . . . . . 11 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
260	258, 259	sylancom 589	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
261	185	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
262		fveere 28139	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
263	261, 262	sylancom 589	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
264		resubcl 11520	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
265	57, 264	mpan 689	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
266		remulcl 11191	. . . . . . . . . . . . 13 ⊢ (((1 − 𝑡) ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
267	265, 266	sylan 581	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
268	267	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
269		remulcl 11191	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
270	269	3adant2 1132	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
271	268, 270	readdcld 11239	. . . . . . . . . 10 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
272	257, 260, 263, 271	syl3anc 1372	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
273	272	ralrimiva 3147	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
274		simpll1 1213	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
275		mptelee 28133	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
276	274, 275	syl 17	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
277	273, 276	mpbird 257	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
278		letric 11310	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
279	57, 175, 278	sylancr 588	. . . . . . . . 9 ⊢ (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
280	279	adantl 483	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
281		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
282	175	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
283		0red 11213	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
284		1red 11211	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
285		0lt1 11732	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
286	285	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
287	283, 284, 282, 286, 281	ltletrd 11370	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
288		divelunit 13467	. . . . . . . . . . . . . . . 16 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
289	57, 58, 288	mpanl12 701	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
290	282, 287, 289	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
291	281, 290	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
292	291	adantll 713	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
293	175	ad3antlr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
294	293	recnd 11238	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
295	287	gt0ne0d 11774	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
296	295	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
297	296	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
298	182	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
299	298, 29	sylancom 589	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
300	185	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
301	300, 187	sylancom 589	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
302		reccl 11875	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
303	302	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
304	190	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
305	304, 192, 193	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
306	195	ad2ant2rl 748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
307	303, 305, 306	adddid 11234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))))
308	307	oveq2d 7420	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
309		subcl 11455	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
310	71, 302, 309	sylancr 588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
311		mulcl 11190	. . . . . . . . . . . . . . . . 17 ⊢ (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
312	310, 192, 311	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
313	303, 305	mulcld 11230	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) ∈ ℂ)
314		recid2 11883	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
315	314	oveq1d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
316	315	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
317		simpll 766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
318		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
319	303, 317, 318	mulassd 11233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))
320		mullid 11209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) ∈ ℂ → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
321	320	ad2antll 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
322	316, 319, 321	3eqtr3d 2781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) = (𝑈‘𝑖))
323	322, 318	eqeltrd 2834	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) ∈ ℂ)
324	312, 313, 323	addassd 11232	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
325	310	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
326	302, 304	mulcld 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
327	326	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
328		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
329	325, 327, 328	adddird 11235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))))
330		simpl 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
331		subdi 11643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
332	71, 331	mp3an2 1450	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
333	302, 330, 332	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
334	302	mulridd 11227	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
335	334, 314	oveq12d 7422	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
336	333, 335	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
337	336	oveq2d 7420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
338		npncan2 11483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
339	71, 302, 338	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
340	337, 339	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
341	340	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
342	341	oveq1d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
343	108	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
344	342, 343	eqtrd 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = 0)
345	190	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
346	303, 345, 328	mulassd 11233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))))
347	346	oveq2d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))))
348	329, 344, 347	3eqtr3rd 2782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) = 0)
349	348, 322	oveq12d 7422	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (0 + (𝑈‘𝑖)))
350		addlid 11393	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) ∈ ℂ → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
351	350	ad2antll 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
352	349, 351	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (𝑈‘𝑖))
353	308, 324, 352	3eqtr2rd 2780	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
354	294, 297, 299, 301, 353	syl22anc 838	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
355	354	ralrimiva 3147	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
356		oveq2 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
357	356	oveq1d 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑍‘𝑖)))
358		oveq1 7411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))
359	357, 358	oveq12d 7422	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
360	359	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (1 / 𝑡) → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
361	360	ralbidv 3178	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
362		fveq2 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑍‘𝑘) = (𝑍‘𝑖))
363	362	oveq2d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍‘𝑘)) = ((1 − 𝑡) · (𝑍‘𝑖)))
364		fveq2 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑈‘𝑘) = (𝑈‘𝑖))
365	364	oveq2d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝑈‘𝑘)) = (𝑡 · (𝑈‘𝑖)))
366	363, 365	oveq12d 7422	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
367		eqid 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))
368		ovex 7437	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∈ V
369	366, 367, 368	fvmpt 6994	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
370	369	oveq2d 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
371	370	oveq2d 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
372	371	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))))
373	372	ralbiia 3092	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
374	361, 373	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))))
375	374	rspcev 3612	. . . . . . . . . . . 12 ⊢ (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
376	292, 355, 375	syl2anc 585	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
377	185	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 ∈ (𝔼‘𝑁))
378	182	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑍 ∈ (𝔼‘𝑁))
379	277	adantr 482	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
380		brbtwn 28137	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
381	377, 378, 379, 380	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
382	376, 381	mpbird 257	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
383	382	ex 414	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
384		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
385		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
386		simpr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
387	384, 385, 386	3jca 1129	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
388	174	anbi1i 625	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
389		elicc01 13439	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
390	387, 388, 389	3imtr4i 292	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
391	390	adantll 713	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
392	369	rgen 3064	. . . . . . . . . . . 12 ⊢ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))
393		oveq2 7412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
394	393	oveq1d 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − 𝑡) · (𝑍‘𝑖)))
395		oveq1 7411	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → (𝑠 · (𝑈‘𝑖)) = (𝑡 · (𝑈‘𝑖)))
396	394, 395	oveq12d 7422	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
397	396	eqeq2d 2744	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
398	397	ralbidv 3178	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
399	398	rspcev 3612	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
400	391, 392, 399	sylancl 587	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
401	277	adantr 482	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
402	182	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
403	185	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
404		brbtwn 28137	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
405	401, 402, 403, 404	syl3anc 1372	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
406	400, 405	mpbird 257	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
407	406	ex 414	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
408	383, 407	orim12d 964	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((1 ≤ 𝑡 ∨ 𝑡 ≤ 1) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
409	280, 408	mpd 15	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
410		opeq2 4873	. . . . . . . . . 10 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
411	410	breq2d 5159	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
412		breq1 5150	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
413	411, 412	orbi12d 918	. . . . . . . 8 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
414	413, 5	elrab2 3685	. . . . . . 7 ⊢ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
415	277, 409, 414	sylanbrc 584	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷)
416		fveq1 6887	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))
417	416	eqeq1d 2735	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
418	417	ralbidv 3178	. . . . . . 7 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
419	418	rspcev 3612	. . . . . 6 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
420	415, 392, 419	sylancl 587	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
421	6	simplbi 499	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ (𝔼‘𝑁))
422	5	ssrab3 4079	. . . . . . . . . 10 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
423	422	sseli 3977	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ (𝔼‘𝑁))
424	421, 423	anim12i 614	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
425		r19.26 3112	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
426		eqtr3 2759	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → (𝑥‘𝑖) = (𝑦‘𝑖))
427	426	ralimi 3084	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
428	425, 427	sylbir 234	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
429		eqeefv 28141	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
430	429	adantl 483	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
431	428, 430	imbitrrid 245	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
432	424, 431	sylan2 594	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
433	432	ralrimivva 3201	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
434	433	adantr 482	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
435		df-reu 3378	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
436		fveq1 6887	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥‘𝑖) = (𝑦‘𝑖))
437	436	eqeq1d 2735	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
438	437	ralbidv 3178	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
439	438	reu4 3726	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
440	435, 439	bitr3i 277	. . . . 5 ⊢ (∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
441	420, 434, 440	sylanbrc 584	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
442	441	ralrimiva 3147	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
443		an12 644	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
444	443	opabbii 5214	. . . . . . 7 ⊢ {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
445	254, 444	eqtri 2761	. . . . . 6 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
446	445	cnveqi 5872	. . . . 5 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
447		cnvopab 6135	. . . . 5 ⊢ ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
448	446, 447	eqtri 2761	. . . 4 ⊢ ◡𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
449	448	fnopabg 6684	. . 3 ⊢ (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ ◡𝐹 Fn (0[,)+∞))
450	442, 449	sylib 217	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ◡𝐹 Fn (0[,)+∞))
451		dff1o4 6838	. 2 ⊢ (𝐹:𝐷–1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷 ∧ ◡𝐹 Fn (0[,)+∞)))
452	256, 450, 451	sylanbrc 584	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹:𝐷–1-1-onto→(0[,)+∞))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ∃!weu 2563   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  ∃!wreu 3375  {crab 3433   ⊆ wss 3947  ⟨cop 4633   class class class wbr 5147  {copab 5209   ↦ cmpt 5230  ^◡ccnv 5674   Fn wfn 6535  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7404  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111  +∞cpnf 11241   < clt 11244   ≤ cle 11245   − cmin 11440   / cdiv 11867  ℕcn 12208  [,)cico 13322  [,]cicc 13323  ...cfz 13480  𝔼cee 28126   Btwn cbtwn 28127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-z 12555  df-uz 12819  df-ico 13326  df-icc 13327  df-fz 13481  df-ee 28129  df-btwn 28130

This theorem is referenced by:  axcontlem5  28206  axcontlem9  28210  axcontlem10  28211