Theorem axcontlem2 26745

Description: Lemma for axcont 26756. The idea here is to set up a mapping 𝐹 that will allow us to transfer dedekind 10797 to two sets of points. Here, we set up 𝐹 and show its domain and range. (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 4798	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
2	1	breq2d 5071	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3		breq1 5062	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
4	2, 3	orbi12d 915	. . . . . . . 8 ⊢ (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5		axcontlem2.1	. . . . . . . 8 ⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
6	4, 5	elrab2 3683	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7		simpll3 1210	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8		simpll2 1209	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9		simpr 487	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10		brbtwn 26679	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
11	7, 8, 9, 10	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
12	11	biimpa 479	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))
13		simp-4r 782	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑍 ≠ 𝑈)
14		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15		1m0e1 11752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 0) = 1
16	14, 15	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 0 → (1 − 𝑠) = 1)
17	16	oveq1d 7165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → ((1 − 𝑠) · (𝑍‘𝑖)) = (1 · (𝑍‘𝑖)))
18		oveq1 7157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → (𝑠 · (𝑥‘𝑖)) = (0 · (𝑥‘𝑖)))
19	17, 18	oveq12d 7168	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 0 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
20	19	eqeq2d 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 0 → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
21	20	ralbidv 3197	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
22	21	biimpac 481	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
23		eqcom 2828	. . . . . . . . . . . . . . . . 17 ⊢ (𝑍 = 𝑈 ↔ 𝑈 = 𝑍)
24	7	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
25	8	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26		eqeefv 26683	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
27	24, 25, 26	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
28	8	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29		fveecn 26682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
30	28, 29	sylancom 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
31		fveecn 26682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
32	31	ad4ant24 752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
33		mulid2 10634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → (1 · (𝑍‘𝑖)) = (𝑍‘𝑖))
34		mul02 10812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 · (𝑥‘𝑖)) = 0)
35	33, 34	oveqan12d 7169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = ((𝑍‘𝑖) + 0))
36		addid1 10814	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
37	36	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
38	35, 37	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = (𝑍‘𝑖))
39	38	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
40	30, 32, 39	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
41	40	ralbidva 3196	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
42	27, 41	bitr4d 284	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
43	23, 42	syl5bb 285	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
44	22, 43	syl5ibr 248	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
45	44	expdimp 455	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
46	45	necon3d 3037	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑍 ≠ 𝑈 → 𝑠 ≠ 0))
47	13, 46	mpd 15	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑠 ≠ 0)
48		elicc01 12848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1))
49	48	simp1bi 1141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
50		rereccl 11352	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
51	49, 50	sylan 582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
52	49	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
53	48	simp2bi 1142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
54	53	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
55		simpr 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
56	52, 54, 55	ne0gt0d 10771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
57		1re 10635	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
58		0le1 11157	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 1
59		divge0 11503	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
60	57, 58, 59	mpanl12 700	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
61	52, 56, 60	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
62		elrege0 12836	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
63	51, 61, 62	sylanbrc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
64	63	adantll 712	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
65	49	ad3antlr 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
66	65	recnd 10663	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
67		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
68	31	ad5ant25 760	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
69	8	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
70	69, 29	sylancom 590	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
71		ax-1cn 10589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℂ
72		reccl 11299	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
73		subcl 10879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
74	71, 72, 73	sylancr 589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
75	74	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
76		subcl 10879	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
77	71, 76	mpan 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
78	77	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
79	72, 78	mulcld 10655	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
80	79	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
81		simprr 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
82	75, 80, 81	adddird 10660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))))
83		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
84		subdi 11067	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
85	71, 84	mp3an2 1445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
86	72, 83, 85	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
87	86	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
88	72	mulid1d 10652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
89		recid2 11307	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
90	88, 89	oveq12d 7168	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
91	90	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
92		addsubass 10890	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
93	71, 92	mp3an3 1446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
94	74, 72, 93	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
95	74, 72	addcld 10654	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
96		npcan 10889	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
97	71, 72, 96	sylancr 589	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
98	95, 97	subeq0bd 11060	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
99	91, 94, 98	3eqtr2d 2862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
100	87, 99	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
101	100	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
102	101	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
103	72	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
104	77	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
105	103, 104, 81	mulassd 10658	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))))
106	105	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))))
107	82, 102, 106	3eqtr3rd 2865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = (0 · (𝑍‘𝑖)))
108		mul02 10812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍‘𝑖) ∈ ℂ → (0 · (𝑍‘𝑖)) = 0)
109	108	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
110	107, 109	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = 0)
111		simpll 765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
112		simprl 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) ∈ ℂ)
113	103, 111, 112	mulassd 10658	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))
114	89	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (1 · (𝑥‘𝑖)))
115		mulid2 10634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥‘𝑖) ∈ ℂ → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
116	115	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
117	114, 116	sylan9eq 2876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (𝑥‘𝑖))
118	113, 117	eqtr3d 2858	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) = (𝑥‘𝑖))
119	110, 118	oveq12d 7168	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (0 + (𝑥‘𝑖)))
120	75, 81	mulcld 10655	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍‘𝑖)) ∈ ℂ)
121		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
122		mulcl 10615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
123	78, 121, 122	syl2an 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
124	103, 123	mulcld 10655	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) ∈ ℂ)
125		mulcl 10615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
126	125	ad2ant2r 745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
127	103, 126	mulcld 10655	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) ∈ ℂ)
128	120, 124, 127	addassd 10657	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
129	103, 123, 126	adddid 10659	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))))
130	129	oveq2d 7166	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
131	128, 130	eqtr4d 2859	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
132		addid2 10817	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
133	132	ad2antrl 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
134	119, 131, 133	3eqtr3rd 2865	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
135	66, 67, 68, 70, 134	syl22anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
136	135	ralrimiva 3182	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
137		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
138	137	oveq1d 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − (1 / 𝑠)) · (𝑍‘𝑖)))
139		oveq1 7157	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
140	138, 139	oveq12d 7168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
141	140	eqeq2d 2832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (1 / 𝑠) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
142	141	ralbidv 3197	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
143	142	rspcev 3623	. . . . . . . . . . . . . . 15 ⊢ (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
144	64, 136, 143	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
145		oveq2 7158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (𝑡 · (𝑈‘𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
146	145	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
147	146	eqeq2d 2832	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
148	147	ralimi 3160	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
149		ralbi 3167	. . . . . . . . . . . . . . . 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 3297	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
152	144, 151	syl5ibrcom 249	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
153	152	impancom 454	. . . . . . . . . . . 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 3288	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
156	12, 155	syldan 593	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
157		3simpa 1144	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
158		elicc01 12848	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
159		elrege0 12836	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
160	157, 158, 159	3imtr4i 294	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
161	160	ssriv 3971	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ (0[,)+∞)
162		brbtwn 26679	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
163	9, 8, 7, 162	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
164	163	biimpa 479	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
165		ssrexv 4034	. . . . . . . . . 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 954	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
168	167	anasss 469	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
169	6, 168	sylan2b 595	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
170		r19.26 3170	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
171		eqtr2 2842	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
172	171	ralimi 3160	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
173	170, 172	sylbir 237	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
174		elrege0 12836	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
175	174	simplbi 500	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
176	175	recnd 10663	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
177		elrege0 12836	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
178	177	simplbi 500	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
179	178	recnd 10663	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
180	176, 179	anim12i 614	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
181		simplr 767	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
182		simpl2 1188	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑍 ∈ (𝔼‘𝑁))
183	182	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
184	183, 29	sylancom 590	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
185		simpl3 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑈 ∈ (𝔼‘𝑁))
186	185	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
187		fveecn 26682	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
188	186, 187	sylancom 590	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
189		subcl 10879	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
190	71, 189	mpan 688	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
191	190	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
192		simpl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
193		mulcl 10615	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑡) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
194	191, 192, 193	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
195		mulcl 10615	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
196	195	ad2ant2rl 747	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
197	77	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
198	197, 192, 122	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
199		mulcl 10615	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
200	199	ad2ant2l 744	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
201	194, 196, 198, 200	addsubeq4d 11042	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
202		nnncan1 10916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
203	71, 202	mp3an1 1444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
204	203	ancoms 461	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
205	204	oveq1d 7165	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
206	205	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
207	77	ad2antlr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
208	190	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
209		simprl 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
210	207, 208, 209	subdird 11091	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
211	206, 210	eqtr3d 2858	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
212		simpll 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
213		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
214		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
215	212, 213, 214	subdird 11091	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑈‘𝑖)) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖))))
216	211, 215	eqeq12d 2837	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
217		subcl 10879	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡 − 𝑠) ∈ ℂ)
218	217	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 − 𝑠) ∈ ℂ)
219		mulcan1g 11287	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
220	218, 209, 214, 219	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
221	201, 216, 220	3bitr2d 309	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
222	181, 184, 188, 221	syl12anc 834	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
223	222	ralbidva 3196	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
224		r19.32v 3340	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
225		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ≠ 𝑈)
226	225	neneqd 3021	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
227		simpll2 1209	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
228		simpll3 1210	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
229		eqeefv 26683	. . . . . . . . . . . . . . . 16 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
230	227, 228, 229	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
231	226, 230	mtbid 326	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))
232		orel2 887	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
233	231, 232	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
234		subeq0 10906	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
235	234	adantl 484	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
236	233, 235	sylibd 241	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
237	224, 236	syl5bi 244	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
238	223, 237	sylbid 242	. . . . . . . . . 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 3191	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
242	241	adantr 483	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
243		oveq2 7158	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
244	243	oveq1d 7165	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑖)))
245		oveq1 7157	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → (𝑡 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑖)))
246	244, 245	oveq12d 7168	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
247	246	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
248	247	ralbidv 3197	. . . . . . 7 ⊢ (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
249	248	reu4 3722	. . . . . 6 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠)))
250	169, 242, 249	sylanbrc 585	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
251		df-reu 3145	. . . . 5 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
252	250, 251	sylib 220	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
253	252	ralrimiva 3182	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
254		axcontlem2.2	. . . 4 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
255	254	fnopabg 6480	. . 3 ⊢ (∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ 𝐹 Fn 𝐷)
256	253, 255	sylib 220	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹 Fn 𝐷)
257	175	ad2antlr 725	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
258	182	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
259		fveere 26681	. . . . . . . . . . 11 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
260	258, 259	sylancom 590	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
261	185	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
262		fveere 26681	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
263	261, 262	sylancom 590	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
264		resubcl 10944	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
265	57, 264	mpan 688	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
266		remulcl 10616	. . . . . . . . . . . . 13 ⊢ (((1 − 𝑡) ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
267	265, 266	sylan 582	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
268	267	3adant3 1128	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
269		remulcl 10616	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
270	269	3adant2 1127	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
271	268, 270	readdcld 10664	. . . . . . . . . 10 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
272	257, 260, 263, 271	syl3anc 1367	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
273	272	ralrimiva 3182	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
274		simpll1 1208	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
275		mptelee 26675	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
276	274, 275	syl 17	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
277	273, 276	mpbird 259	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
278		letric 10734	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
279	57, 175, 278	sylancr 589	. . . . . . . . 9 ⊢ (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
280	279	adantl 484	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
281		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
282	175	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
283		0red 10638	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
284		1red 10636	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
285		0lt1 11156	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
286	285	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
287	283, 284, 282, 286, 281	ltletrd 10794	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
288		divelunit 12874	. . . . . . . . . . . . . . . 16 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
289	57, 58, 288	mpanl12 700	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
290	282, 287, 289	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
291	281, 290	mpbird 259	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
292	291	adantll 712	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
293	175	ad3antlr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
294	293	recnd 10663	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
295	287	gt0ne0d 11198	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
296	295	adantll 712	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
297	296	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
298	182	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
299	298, 29	sylancom 590	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
300	185	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
301	300, 187	sylancom 590	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
302		reccl 11299	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
303	302	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
304	190	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
305	304, 192, 193	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
306	195	ad2ant2rl 747	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
307	303, 305, 306	adddid 10659	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))))
308	307	oveq2d 7166	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
309		subcl 10879	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
310	71, 302, 309	sylancr 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
311		mulcl 10615	. . . . . . . . . . . . . . . . 17 ⊢ (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
312	310, 192, 311	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
313	303, 305	mulcld 10655	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) ∈ ℂ)
314		recid2 11307	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
315	314	oveq1d 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
316	315	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
317		simpll 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
318		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
319	303, 317, 318	mulassd 10658	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))
320		mulid2 10634	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) ∈ ℂ → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
321	320	ad2antll 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
322	316, 319, 321	3eqtr3d 2864	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) = (𝑈‘𝑖))
323	322, 318	eqeltrd 2913	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) ∈ ℂ)
324	312, 313, 323	addassd 10657	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
325	310	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
326	302, 304	mulcld 10655	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
327	326	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
328		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
329	325, 327, 328	adddird 10660	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))))
330		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
331		subdi 11067	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
332	71, 331	mp3an2 1445	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
333	302, 330, 332	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
334	302	mulid1d 10652	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
335	334, 314	oveq12d 7168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
336	333, 335	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
337	336	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
338		npncan2 10907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
339	71, 302, 338	sylancr 589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
340	337, 339	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
341	340	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
342	341	oveq1d 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
343	108	ad2antrl 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
344	342, 343	eqtrd 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = 0)
345	190	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
346	303, 345, 328	mulassd 10658	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))))
347	346	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))))
348	329, 344, 347	3eqtr3rd 2865	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) = 0)
349	348, 322	oveq12d 7168	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (0 + (𝑈‘𝑖)))
350		addid2 10817	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) ∈ ℂ → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
351	350	ad2antll 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
352	349, 351	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (𝑈‘𝑖))
353	308, 324, 352	3eqtr2rd 2863	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
354	294, 297, 299, 301, 353	syl22anc 836	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
355	354	ralrimiva 3182	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
356		oveq2 7158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
357	356	oveq1d 7165	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑍‘𝑖)))
358		oveq1 7157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))
359	357, 358	oveq12d 7168	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
360	359	eqeq2d 2832	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (1 / 𝑡) → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
361	360	ralbidv 3197	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
362		fveq2 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑍‘𝑘) = (𝑍‘𝑖))
363	362	oveq2d 7166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍‘𝑘)) = ((1 − 𝑡) · (𝑍‘𝑖)))
364		fveq2 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑈‘𝑘) = (𝑈‘𝑖))
365	364	oveq2d 7166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝑈‘𝑘)) = (𝑡 · (𝑈‘𝑖)))
366	363, 365	oveq12d 7168	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
367		eqid 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))
368		ovex 7183	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∈ V
369	366, 367, 368	fvmpt 6763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
370	369	oveq2d 7166	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
371	370	oveq2d 7166	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
372	371	eqeq2d 2832	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))))
373	372	ralbiia 3164	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
374	361, 373	syl6bb 289	. . . . . . . . . . . . 13 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))))
375	374	rspcev 3623	. . . . . . . . . . . 12 ⊢ (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
376	292, 355, 375	syl2anc 586	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
377	185	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 ∈ (𝔼‘𝑁))
378	182	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑍 ∈ (𝔼‘𝑁))
379	277	adantr 483	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
380		brbtwn 26679	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
381	377, 378, 379, 380	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
382	376, 381	mpbird 259	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
383	382	ex 415	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
384		simpll 765	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
385		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
386		simpr 487	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
387	384, 385, 386	3jca 1124	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
388	174	anbi1i 625	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
389		elicc01 12848	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
390	387, 388, 389	3imtr4i 294	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
391	390	adantll 712	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
392	369	rgen 3148	. . . . . . . . . . . 12 ⊢ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))
393		oveq2 7158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
394	393	oveq1d 7165	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − 𝑡) · (𝑍‘𝑖)))
395		oveq1 7157	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → (𝑠 · (𝑈‘𝑖)) = (𝑡 · (𝑈‘𝑖)))
396	394, 395	oveq12d 7168	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
397	396	eqeq2d 2832	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
398	397	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
399	398	rspcev 3623	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
400	391, 392, 399	sylancl 588	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
401	277	adantr 483	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
402	182	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
403	185	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
404		brbtwn 26679	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
405	401, 402, 403, 404	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
406	400, 405	mpbird 259	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
407	406	ex 415	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
408	383, 407	orim12d 961	. . . . . . . 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 4798	. . . . . . . . . 10 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
411	410	breq2d 5071	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
412		breq1 5062	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
413	411, 412	orbi12d 915	. . . . . . . 8 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
414	413, 5	elrab2 3683	. . . . . . 7 ⊢ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
415	277, 409, 414	sylanbrc 585	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷)
416		fveq1 6664	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))
417	416	eqeq1d 2823	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
418	417	ralbidv 3197	. . . . . . 7 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
419	418	rspcev 3623	. . . . . 6 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
420	415, 392, 419	sylancl 588	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
421	6	simplbi 500	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ (𝔼‘𝑁))
422	5	ssrab3 4057	. . . . . . . . . 10 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
423	422	sseli 3963	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ (𝔼‘𝑁))
424	421, 423	anim12i 614	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
425		r19.26 3170	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
426		eqtr3 2843	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → (𝑥‘𝑖) = (𝑦‘𝑖))
427	426	ralimi 3160	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
428	425, 427	sylbir 237	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
429		eqeefv 26683	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
430	429	adantl 484	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
431	428, 430	syl5ibr 248	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
432	424, 431	sylan2 594	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
433	432	ralrimivva 3191	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
434	433	adantr 483	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
435		df-reu 3145	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
436		fveq1 6664	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥‘𝑖) = (𝑦‘𝑖))
437	436	eqeq1d 2823	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
438	437	ralbidv 3197	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
439	438	reu4 3722	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
440	435, 439	bitr3i 279	. . . . 5 ⊢ (∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
441	420, 434, 440	sylanbrc 585	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
442	441	ralrimiva 3182	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
443		an12 643	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
444	443	opabbii 5126	. . . . . . 7 ⊢ {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
445	254, 444	eqtri 2844	. . . . . 6 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
446	445	cnveqi 5740	. . . . 5 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
447		cnvopab 5992	. . . . 5 ⊢ ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
448	446, 447	eqtri 2844	. . . 4 ⊢ ◡𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
449	448	fnopabg 6480	. . 3 ⊢ (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ ◡𝐹 Fn (0[,)+∞))
450	442, 449	sylib 220	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ◡𝐹 Fn (0[,)+∞))
451		dff1o4 6618	. 2 ⊢ (𝐹:𝐷–1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷 ∧ ◡𝐹 Fn (0[,)+∞)))
452	256, 450, 451	sylanbrc 585	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹:𝐷–1-1-onto→(0[,)+∞))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∃!weu 2649   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140  {crab 3142   ⊆ wss 3936  ⟨cop 4567   class class class wbr 5059  {copab 5121   ↦ cmpt 5139  ^◡ccnv 5549   Fn wfn 6345  –1-1-onto→wf1o 6349  ‘cfv 6350  (class class class)co 7150  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  +∞cpnf 10666   < clt 10669   ≤ cle 10670   − cmin 10864   / cdiv 11291  ℕcn 11632  [,)cico 12734  [,]cicc 12735  ...cfz 12886  𝔼cee 26668   Btwn cbtwn 26669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-z 11976  df-uz 12238  df-ico 12738  df-icc 12739  df-fz 12887  df-ee 26671  df-btwn 26672

This theorem is referenced by:  axcontlem5  26748  axcontlem9  26752  axcontlem10  26753