Theorem axcontlem2 26873

Description: Lemma for axcont 26884. The idea here is to set up a mapping 𝐹 that will allow us to transfer dedekind 10855 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 4767	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
2	1	breq2d 5049	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3		breq1 5040	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
4	2, 3	orbi12d 916	. . . . . . . 8 ⊢ (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5		axcontlem2.1	. . . . . . . 8 ⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
6	4, 5	elrab2 3608	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7		simpll3 1212	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8		simpll2 1211	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9		simpr 488	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10		brbtwn 26807	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
11	7, 8, 9, 10	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
12	11	biimpa 480	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))
13		simp-4r 783	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑍 ≠ 𝑈)
14		oveq2 7165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15		1m0e1 11809	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 0) = 1
16	14, 15	eqtrdi 2810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 0 → (1 − 𝑠) = 1)
17	16	oveq1d 7172	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → ((1 − 𝑠) · (𝑍‘𝑖)) = (1 · (𝑍‘𝑖)))
18		oveq1 7164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → (𝑠 · (𝑥‘𝑖)) = (0 · (𝑥‘𝑖)))
19	17, 18	oveq12d 7175	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 0 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
20	19	eqeq2d 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 0 → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
21	20	ralbidv 3127	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
22	21	biimpac 482	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
23		eqcom 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑍 = 𝑈 ↔ 𝑈 = 𝑍)
24	7	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
25	8	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26		eqeefv 26811	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
27	24, 25, 26	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
28	8	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29		fveecn 26810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
30	28, 29	sylancom 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
31		fveecn 26810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
32	31	ad4ant24 753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
33		mulid2 10692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → (1 · (𝑍‘𝑖)) = (𝑍‘𝑖))
34		mul02 10870	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 · (𝑥‘𝑖)) = 0)
35	33, 34	oveqan12d 7176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = ((𝑍‘𝑖) + 0))
36		addid1 10872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
37	36	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
38	35, 37	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = (𝑍‘𝑖))
39	38	eqeq2d 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
40	30, 32, 39	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
41	40	ralbidva 3126	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
42	27, 41	bitr4d 285	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
43	23, 42	syl5bb 286	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
44	22, 43	syl5ibr 249	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
45	44	expdimp 456	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
46	45	necon3d 2973	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑍 ≠ 𝑈 → 𝑠 ≠ 0))
47	13, 46	mpd 15	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑠 ≠ 0)
48		elicc01 12912	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1))
49	48	simp1bi 1143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
50		rereccl 11410	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
51	49, 50	sylan 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
52	49	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
53	48	simp2bi 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
54	53	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
55		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
56	52, 54, 55	ne0gt0d 10829	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
57		1re 10693	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
58		0le1 11215	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 1
59		divge0 11561	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
60	57, 58, 59	mpanl12 701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
61	52, 56, 60	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
62		elrege0 12900	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
63	51, 61, 62	sylanbrc 586	. . . . . . . . . . . . . . . 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 10721	. . . . . . . . . . . . . . . . 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 591	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
71		ax-1cn 10647	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℂ
72		reccl 11357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
73		subcl 10937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
74	71, 72, 73	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
75	74	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
76		subcl 10937	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
77	71, 76	mpan 689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
78	77	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
79	72, 78	mulcld 10713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
80	79	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
81		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
82	75, 80, 81	adddird 10718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))))
83		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
84		subdi 11125	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
85	71, 84	mp3an2 1447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
86	72, 83, 85	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
87	86	oveq2d 7173	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
88	72	mulid1d 10710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
89		recid2 11365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
90	88, 89	oveq12d 7175	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
91	90	oveq2d 7173	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
92		addsubass 10948	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
93	71, 92	mp3an3 1448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
94	74, 72, 93	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
95	74, 72	addcld 10712	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
96		npcan 10947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
97	71, 72, 96	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
98	95, 97	subeq0bd 11118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
99	91, 94, 98	3eqtr2d 2800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
100	87, 99	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
101	100	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
102	101	oveq1d 7172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
103	72	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
104	77	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
105	103, 104, 81	mulassd 10716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))))
106	105	oveq2d 7173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))))
107	82, 102, 106	3eqtr3rd 2803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = (0 · (𝑍‘𝑖)))
108		mul02 10870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍‘𝑖) ∈ ℂ → (0 · (𝑍‘𝑖)) = 0)
109	108	ad2antll 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
110	107, 109	eqtrd 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = 0)
111		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
112		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) ∈ ℂ)
113	103, 111, 112	mulassd 10716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))
114	89	oveq1d 7172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (1 · (𝑥‘𝑖)))
115		mulid2 10692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥‘𝑖) ∈ ℂ → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
116	115	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
117	114, 116	sylan9eq 2814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (𝑥‘𝑖))
118	113, 117	eqtr3d 2796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) = (𝑥‘𝑖))
119	110, 118	oveq12d 7175	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (0 + (𝑥‘𝑖)))
120	75, 81	mulcld 10713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍‘𝑖)) ∈ ℂ)
121		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
122		mulcl 10673	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
123	78, 121, 122	syl2an 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
124	103, 123	mulcld 10713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) ∈ ℂ)
125		mulcl 10673	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
126	125	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
127	103, 126	mulcld 10713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) ∈ ℂ)
128	120, 124, 127	addassd 10715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
129	103, 123, 126	adddid 10717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))))
130	129	oveq2d 7173	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
131	128, 130	eqtr4d 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
132		addid2 10875	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
133	132	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
134	119, 131, 133	3eqtr3rd 2803	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
135	66, 67, 68, 70, 134	syl22anc 837	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
136	135	ralrimiva 3114	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
137		oveq2 7165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
138	137	oveq1d 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − (1 / 𝑠)) · (𝑍‘𝑖)))
139		oveq1 7164	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
140	138, 139	oveq12d 7175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
141	140	eqeq2d 2770	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (1 / 𝑠) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
142	141	ralbidv 3127	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
143	142	rspcev 3544	. . . . . . . . . . . . . . 15 ⊢ (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
144	64, 136, 143	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
145		oveq2 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (𝑡 · (𝑈‘𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
146	145	oveq2d 7173	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
147	146	eqeq2d 2770	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
148	147	ralimi 3093	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
149		ralbi 3100	. . . . . . . . . . . . . . . 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 3222	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
152	144, 151	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
153	152	impancom 455	. . . . . . . . . . . 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 3213	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
156	12, 155	syldan 594	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
157		3simpa 1146	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
158		elicc01 12912	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
159		elrege0 12900	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
160	157, 158, 159	3imtr4i 295	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
161	160	ssriv 3899	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ (0[,)+∞)
162		brbtwn 26807	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
163	9, 8, 7, 162	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
164	163	biimpa 480	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
165		ssrexv 3962	. . . . . . . . . 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 955	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
168	167	anasss 470	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
169	6, 168	sylan2b 596	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
170		r19.26 3102	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
171		eqtr2 2780	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
172	171	ralimi 3093	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
173	170, 172	sylbir 238	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
174		elrege0 12900	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
175	174	simplbi 501	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
176	175	recnd 10721	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
177		elrege0 12900	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
178	177	simplbi 501	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
179	178	recnd 10721	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
180	176, 179	anim12i 615	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
181		simplr 768	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
182		simpl2 1190	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑍 ∈ (𝔼‘𝑁))
183	182	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
184	183, 29	sylancom 591	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
185		simpl3 1191	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑈 ∈ (𝔼‘𝑁))
186	185	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
187		fveecn 26810	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
188	186, 187	sylancom 591	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
189		subcl 10937	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
190	71, 189	mpan 689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
191	190	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
192		simpl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
193		mulcl 10673	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑡) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
194	191, 192, 193	syl2an 598	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
195		mulcl 10673	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
196	195	ad2ant2rl 748	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
197	77	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
198	197, 192, 122	syl2an 598	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
199		mulcl 10673	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
200	199	ad2ant2l 745	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
201	194, 196, 198, 200	addsubeq4d 11100	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
202		nnncan1 10974	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
203	71, 202	mp3an1 1446	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
204	203	ancoms 462	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
205	204	oveq1d 7172	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
206	205	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
207	77	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
208	190	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
209		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
210	207, 208, 209	subdird 11149	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
211	206, 210	eqtr3d 2796	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
212		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
213		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
214		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
215	212, 213, 214	subdird 11149	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑈‘𝑖)) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖))))
216	211, 215	eqeq12d 2775	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
217		subcl 10937	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡 − 𝑠) ∈ ℂ)
218	217	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 − 𝑠) ∈ ℂ)
219		mulcan1g 11345	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
220	218, 209, 214, 219	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
221	201, 216, 220	3bitr2d 310	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
222	181, 184, 188, 221	syl12anc 835	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
223	222	ralbidva 3126	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
224		r19.32v 3260	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
225		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ≠ 𝑈)
226	225	neneqd 2957	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
227		simpll2 1211	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
228		simpll3 1212	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
229		eqeefv 26811	. . . . . . . . . . . . . . . 16 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
230	227, 228, 229	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
231	226, 230	mtbid 327	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))
232		orel2 888	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
233	231, 232	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
234		subeq0 10964	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
235	234	adantl 485	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
236	233, 235	sylibd 242	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
237	224, 236	syl5bi 245	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
238	223, 237	sylbid 243	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠))
239	180, 238	sylan2 595	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠))
240	173, 239	syl5 34	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
241	240	ralrimivva 3121	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
242	241	adantr 484	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
243		oveq2 7165	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
244	243	oveq1d 7172	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑖)))
245		oveq1 7164	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → (𝑡 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑖)))
246	244, 245	oveq12d 7175	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
247	246	eqeq2d 2770	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
248	247	ralbidv 3127	. . . . . . 7 ⊢ (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
249	248	reu4 3648	. . . . . 6 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠)))
250	169, 242, 249	sylanbrc 586	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
251		df-reu 3078	. . . . 5 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
252	250, 251	sylib 221	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
253	252	ralrimiva 3114	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
254		axcontlem2.2	. . . 4 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
255	254	fnopabg 6474	. . 3 ⊢ (∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ 𝐹 Fn 𝐷)
256	253, 255	sylib 221	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹 Fn 𝐷)
257	175	ad2antlr 726	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
258	182	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
259		fveere 26809	. . . . . . . . . . 11 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
260	258, 259	sylancom 591	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
261	185	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
262		fveere 26809	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
263	261, 262	sylancom 591	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
264		resubcl 11002	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
265	57, 264	mpan 689	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
266		remulcl 10674	. . . . . . . . . . . . 13 ⊢ (((1 − 𝑡) ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
267	265, 266	sylan 583	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
268	267	3adant3 1130	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
269		remulcl 10674	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
270	269	3adant2 1129	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
271	268, 270	readdcld 10722	. . . . . . . . . 10 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
272	257, 260, 263, 271	syl3anc 1369	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
273	272	ralrimiva 3114	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
274		simpll1 1210	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
275		mptelee 26803	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
276	274, 275	syl 17	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
277	273, 276	mpbird 260	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
278		letric 10792	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
279	57, 175, 278	sylancr 590	. . . . . . . . 9 ⊢ (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
280	279	adantl 485	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
281		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
282	175	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
283		0red 10696	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
284		1red 10694	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
285		0lt1 11214	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
286	285	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
287	283, 284, 282, 286, 281	ltletrd 10852	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
288		divelunit 12940	. . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
291	281, 290	mpbird 260	. . . . . . . . . . . . 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 10721	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
295	287	gt0ne0d 11256	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
296	295	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
297	296	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
298	182	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
299	298, 29	sylancom 591	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
300	185	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
301	300, 187	sylancom 591	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
302		reccl 11357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
303	302	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
304	190	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
305	304, 192, 193	syl2an 598	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
306	195	ad2ant2rl 748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
307	303, 305, 306	adddid 10717	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))))
308	307	oveq2d 7173	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
309		subcl 10937	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
310	71, 302, 309	sylancr 590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
311		mulcl 10673	. . . . . . . . . . . . . . . . 17 ⊢ (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
312	310, 192, 311	syl2an 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
313	303, 305	mulcld 10713	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) ∈ ℂ)
314		recid2 11365	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
315	314	oveq1d 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
316	315	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
317		simpll 766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
318		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
319	303, 317, 318	mulassd 10716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))
320		mulid2 10692	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) ∈ ℂ → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
321	320	ad2antll 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
322	316, 319, 321	3eqtr3d 2802	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) = (𝑈‘𝑖))
323	322, 318	eqeltrd 2853	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) ∈ ℂ)
324	312, 313, 323	addassd 10715	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
325	310	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
326	302, 304	mulcld 10713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
327	326	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
328		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
329	325, 327, 328	adddird 10718	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))))
330		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
331		subdi 11125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
332	71, 331	mp3an2 1447	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
333	302, 330, 332	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
334	302	mulid1d 10710	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
335	334, 314	oveq12d 7175	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
336	333, 335	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
337	336	oveq2d 7173	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
338		npncan2 10965	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
339	71, 302, 338	sylancr 590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
340	337, 339	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
341	340	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
342	341	oveq1d 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
343	108	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
344	342, 343	eqtrd 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = 0)
345	190	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
346	303, 345, 328	mulassd 10716	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))))
347	346	oveq2d 7173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))))
348	329, 344, 347	3eqtr3rd 2803	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) = 0)
349	348, 322	oveq12d 7175	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (0 + (𝑈‘𝑖)))
350		addid2 10875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) ∈ ℂ → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
351	350	ad2antll 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
352	349, 351	eqtrd 2794	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (𝑈‘𝑖))
353	308, 324, 352	3eqtr2rd 2801	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
354	294, 297, 299, 301, 353	syl22anc 837	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
355	354	ralrimiva 3114	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
356		oveq2 7165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
357	356	oveq1d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑍‘𝑖)))
358		oveq1 7164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))
359	357, 358	oveq12d 7175	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
360	359	eqeq2d 2770	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (1 / 𝑡) → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
361	360	ralbidv 3127	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
362		fveq2 6664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑍‘𝑘) = (𝑍‘𝑖))
363	362	oveq2d 7173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍‘𝑘)) = ((1 − 𝑡) · (𝑍‘𝑖)))
364		fveq2 6664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑈‘𝑘) = (𝑈‘𝑖))
365	364	oveq2d 7173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝑈‘𝑘)) = (𝑡 · (𝑈‘𝑖)))
366	363, 365	oveq12d 7175	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
367		eqid 2759	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))
368		ovex 7190	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∈ V
369	366, 367, 368	fvmpt 6765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
370	369	oveq2d 7173	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
371	370	oveq2d 7173	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
372	371	eqeq2d 2770	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))))
373	372	ralbiia 3097	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
374	361, 373	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))))
375	374	rspcev 3544	. . . . . . . . . . . 12 ⊢ (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
376	292, 355, 375	syl2anc 587	. . . . . . . . . . 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 484	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
380		brbtwn 26807	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
381	377, 378, 379, 380	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
382	376, 381	mpbird 260	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
383	382	ex 416	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
384		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
385		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
386		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
387	384, 385, 386	3jca 1126	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
388	174	anbi1i 626	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
389		elicc01 12912	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
390	387, 388, 389	3imtr4i 295	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
391	390	adantll 713	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
392	369	rgen 3081	. . . . . . . . . . . 12 ⊢ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))
393		oveq2 7165	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
394	393	oveq1d 7172	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − 𝑡) · (𝑍‘𝑖)))
395		oveq1 7164	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → (𝑠 · (𝑈‘𝑖)) = (𝑡 · (𝑈‘𝑖)))
396	394, 395	oveq12d 7175	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
397	396	eqeq2d 2770	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
398	397	ralbidv 3127	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
399	398	rspcev 3544	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
400	391, 392, 399	sylancl 589	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
401	277	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
402	182	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
403	185	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
404		brbtwn 26807	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
405	401, 402, 403, 404	syl3anc 1369	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
406	400, 405	mpbird 260	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
407	406	ex 416	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
408	383, 407	orim12d 962	. . . . . . . 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 4767	. . . . . . . . . 10 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
411	410	breq2d 5049	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
412		breq1 5040	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
413	411, 412	orbi12d 916	. . . . . . . 8 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
414	413, 5	elrab2 3608	. . . . . . 7 ⊢ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
415	277, 409, 414	sylanbrc 586	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷)
416		fveq1 6663	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))
417	416	eqeq1d 2761	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
418	417	ralbidv 3127	. . . . . . 7 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
419	418	rspcev 3544	. . . . . 6 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
420	415, 392, 419	sylancl 589	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
421	6	simplbi 501	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ (𝔼‘𝑁))
422	5	ssrab3 3989	. . . . . . . . . 10 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
423	422	sseli 3891	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ (𝔼‘𝑁))
424	421, 423	anim12i 615	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
425		r19.26 3102	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
426		eqtr3 2781	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → (𝑥‘𝑖) = (𝑦‘𝑖))
427	426	ralimi 3093	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
428	425, 427	sylbir 238	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
429		eqeefv 26811	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
430	429	adantl 485	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
431	428, 430	syl5ibr 249	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
432	424, 431	sylan2 595	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
433	432	ralrimivva 3121	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
434	433	adantr 484	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
435		df-reu 3078	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
436		fveq1 6663	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥‘𝑖) = (𝑦‘𝑖))
437	436	eqeq1d 2761	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
438	437	ralbidv 3127	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
439	438	reu4 3648	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
440	435, 439	bitr3i 280	. . . . 5 ⊢ (∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
441	420, 434, 440	sylanbrc 586	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
442	441	ralrimiva 3114	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
443		an12 644	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
444	443	opabbii 5104	. . . . . . 7 ⊢ {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
445	254, 444	eqtri 2782	. . . . . 6 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
446	445	cnveqi 5721	. . . . 5 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
447		cnvopab 5975	. . . . 5 ⊢ ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
448	446, 447	eqtri 2782	. . . 4 ⊢ ◡𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
449	448	fnopabg 6474	. . 3 ⊢ (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ ◡𝐹 Fn (0[,)+∞))
450	442, 449	sylib 221	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ◡𝐹 Fn (0[,)+∞))
451		dff1o4 6616	. 2 ⊢ (𝐹:𝐷–1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷 ∧ ◡𝐹 Fn (0[,)+∞)))
452	256, 450, 451	sylanbrc 586	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹:𝐷–1-1-onto→(0[,)+∞))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∃!weu 2588   ≠ wne 2952  ∀wral 3071  ∃wrex 3072  ∃!wreu 3073  {crab 3075   ⊆ wss 3861  ⟨cop 4532   class class class wbr 5037  {copab 5099   ↦ cmpt 5117  ^◡ccnv 5528   Fn wfn 6336  –1-1-onto→wf1o 6340  ‘cfv 6341  (class class class)co 7157  ℂcc 10587  ℝcr 10588  0cc0 10589  1c1 10590   + caddc 10592   · cmul 10594  +∞cpnf 10724   < clt 10727   ≤ cle 10728   − cmin 10922   / cdiv 11349  ℕcn 11688  [,)cico 12795  [,]cicc 12796  ...cfz 12953  𝔼cee 26796   Btwn cbtwn 26797

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1st 7700  df-2nd 7701  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-er 8306  df-map 8425  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-div 11350  df-nn 11689  df-z 12035  df-uz 12297  df-ico 12799  df-icc 12800  df-fz 12954  df-ee 26799  df-btwn 26800

This theorem is referenced by:  axcontlem5  26876  axcontlem9  26880  axcontlem10  26881