Theorem axcontlem2 28998

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem axcontlem2

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

Step	Hyp	Ref	Expression
1		opeq2 4898	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
2	1	breq2d 5178	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3		breq1 5169	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
4	2, 3	orbi12d 917	. . . . . . . 8 ⊢ (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5		axcontlem2.1	. . . . . . . 8 ⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
6	4, 5	elrab2 3711	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7		simpll3 1214	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8		simpll2 1213	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10		brbtwn 28932	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
11	7, 8, 9, 10	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
12	11	biimpa 476	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))
13		simp-4r 783	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑍 ≠ 𝑈)
14		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15		1m0e1 12414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 0) = 1
16	14, 15	eqtrdi 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 0 → (1 − 𝑠) = 1)
17	16	oveq1d 7463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → ((1 − 𝑠) · (𝑍‘𝑖)) = (1 · (𝑍‘𝑖)))
18		oveq1 7455	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 0 → (𝑠 · (𝑥‘𝑖)) = (0 · (𝑥‘𝑖)))
19	17, 18	oveq12d 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 0 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
20	19	eqeq2d 2751	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 0 → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
21	20	ralbidv 3184	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
22	21	biimpac 478	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))
23		eqcom 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑍 = 𝑈 ↔ 𝑈 = 𝑍)
24	7	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
25	8	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26		eqeefv 28936	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
27	24, 25, 26	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
28	8	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29		fveecn 28935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
30	28, 29	sylancom 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
31		fveecn 28935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
32	31	ad4ant24 753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
33		mullid 11289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → (1 · (𝑍‘𝑖)) = (𝑍‘𝑖))
34		mul02 11468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 · (𝑥‘𝑖)) = 0)
35	33, 34	oveqan12d 7467	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = ((𝑍‘𝑖) + 0))
36		addrid 11470	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍‘𝑖) ∈ ℂ → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
37	36	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
38	35, 37	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = (𝑍‘𝑖))
39	38	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
40	30, 32, 39	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖)))
41	40	ralbidva 3182	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖)))
42	27, 41	bitr4d 282	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
43	23, 42	bitrid 283	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))))
44	22, 43	imbitrrid 246	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
45	44	expdimp 452	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
46	45	necon3d 2967	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑍 ≠ 𝑈 → 𝑠 ≠ 0))
47	13, 46	mpd 15	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑠 ≠ 0)
48		elicc01 13526	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1))
49	48	simp1bi 1145	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
50		rereccl 12012	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
51	49, 50	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
52	49	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
53	48	simp2bi 1146	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
54	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
55		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
56	52, 54, 55	ne0gt0d 11427	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
57		1re 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
58		0le1 11813	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 1
59		divge0 12164	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
60	57, 58, 59	mpanl12 701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
61	52, 56, 60	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
62		elrege0 13514	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
63	51, 61, 62	sylanbrc 582	. . . . . . . . . . . . . . . 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 11318	. . . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
71		ax-1cn 11242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℂ
72		reccl 11956	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
73		subcl 11535	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
74	71, 72, 73	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
75	74	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
76		subcl 11535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
77	71, 76	mpan 689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
78	77	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
79	72, 78	mulcld 11310	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
81		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
82	75, 80, 81	adddird 11315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))))
83		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
84		subdi 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
85	71, 84	mp3an2 1449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
86	72, 83, 85	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
87	86	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
88	72	mulridd 11307	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
89		recid2 11964	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
90	88, 89	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
91	90	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
92		addsubass 11546	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
93	71, 92	mp3an3 1450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
94	74, 72, 93	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
95	74, 72	addcld 11309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
96		npcan 11545	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
97	71, 72, 96	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
98	95, 97	subeq0bd 11716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
99	91, 94, 98	3eqtr2d 2786	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
100	87, 99	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
102	101	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
103	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
104	77	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
105	103, 104, 81	mulassd 11313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))))
106	105	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))))
107	82, 102, 106	3eqtr3rd 2789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = (0 · (𝑍‘𝑖)))
108		mul02 11468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑍‘𝑖) ∈ ℂ → (0 · (𝑍‘𝑖)) = 0)
109	108	ad2antll 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
110	107, 109	eqtrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = 0)
111		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
112		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) ∈ ℂ)
113	103, 111, 112	mulassd 11313	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))
114	89	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (1 · (𝑥‘𝑖)))
115		mullid 11289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥‘𝑖) ∈ ℂ → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
116	115	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
117	114, 116	sylan9eq 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (𝑥‘𝑖))
118	113, 117	eqtr3d 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) = (𝑥‘𝑖))
119	110, 118	oveq12d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (0 + (𝑥‘𝑖)))
120	75, 81	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍‘𝑖)) ∈ ℂ)
121		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
122		mulcl 11268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
123	78, 121, 122	syl2an 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
124	103, 123	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) ∈ ℂ)
125		mulcl 11268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
126	125	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ)
127	103, 126	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) ∈ ℂ)
128	120, 124, 127	addassd 11312	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
129	103, 123, 126	adddid 11314	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))))
130	129	oveq2d 7464	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))))
131	128, 130	eqtr4d 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
132		addlid 11473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥‘𝑖) ∈ ℂ → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
133	132	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖))
134	119, 131, 133	3eqtr3rd 2789	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
135	66, 67, 68, 70, 134	syl22anc 838	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
136	135	ralrimiva 3152	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
137		oveq2 7456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
138	137	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − (1 / 𝑠)) · (𝑍‘𝑖)))
139		oveq1 7455	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
140	138, 139	oveq12d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
141	140	eqeq2d 2751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (1 / 𝑠) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
142	141	ralbidv 3184	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
143	142	rspcev 3635	. . . . . . . . . . . . . . 15 ⊢ (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
144	64, 136, 143	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
145		oveq2 7456	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (𝑡 · (𝑈‘𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))
146	145	oveq2d 7464	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))
147	146	eqeq2d 2751	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
148	147	ralimi 3089	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
149		ralbi 3109	. . . . . . . . . . . . . . . 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 3185	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))))
152	144, 151	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
153	152	impancom 451	. . . . . . . . . . . 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 3164	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
156	12, 155	syldan 590	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
157		3simpa 1148	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
158		elicc01 13526	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1))
159		elrege0 13514	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
160	157, 158, 159	3imtr4i 292	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
161	160	ssriv 4012	. . . . . . . . . 10 ⊢ (0[,]1) ⊆ (0[,)+∞)
162		brbtwn 28932	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
163	9, 8, 7, 162	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
164	163	biimpa 476	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
165		ssrexv 4078	. . . . . . . . . 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 958	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
168	167	anasss 466	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
169	6, 168	sylan2b 593	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
170		r19.26 3117	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
171		eqtr2 2764	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
172	171	ralimi 3089	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
173	170, 172	sylbir 235	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
174		elrege0 13514	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
175	174	simplbi 497	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
176	175	recnd 11318	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
177		elrege0 13514	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
178	177	simplbi 497	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
179	178	recnd 11318	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
180	176, 179	anim12i 612	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
181		simplr 768	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
182		simpl2 1192	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑍 ∈ (𝔼‘𝑁))
183	182	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
184	183, 29	sylancom 587	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
185		simpl3 1193	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑈 ∈ (𝔼‘𝑁))
186	185	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
187		fveecn 28935	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
188	186, 187	sylancom 587	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
189		subcl 11535	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
190	71, 189	mpan 689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
191	190	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
192		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ)
193		mulcl 11268	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑡) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
194	191, 192, 193	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
195		mulcl 11268	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
196	195	ad2ant2rl 748	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
197	77	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
198	197, 192, 122	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
199		mulcl 11268	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
200	199	ad2ant2l 745	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ)
201	194, 196, 198, 200	addsubeq4d 11698	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
202		nnncan1 11572	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
203	71, 202	mp3an1 1448	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
204	203	ancoms 458	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠))
205	204	oveq1d 7463	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
206	205	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖)))
207	77	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
208	190	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
209		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
210	207, 208, 209	subdird 11747	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
211	206, 210	eqtr3d 2782	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))))
212		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
213		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
214		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
215	212, 213, 214	subdird 11747	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑈‘𝑖)) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖))))
216	211, 215	eqeq12d 2756	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))))
217		subcl 11535	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡 − 𝑠) ∈ ℂ)
218	217	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 − 𝑠) ∈ ℂ)
219		mulcan1g 11943	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
220	218, 209, 214, 219	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
221	201, 216, 220	3bitr2d 307	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
222	181, 184, 188, 221	syl12anc 836	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
223	222	ralbidva 3182	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
224		r19.32v 3198	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
225		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ≠ 𝑈)
226	225	neneqd 2951	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
227		simpll2 1213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
228		simpll3 1214	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
229		eqeefv 28936	. . . . . . . . . . . . . . . 16 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
230	227, 228, 229	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
231	226, 230	mtbid 324	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))
232		orel2 889	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
233	231, 232	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0))
234		subeq0 11562	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
235	234	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠))
236	233, 235	sylibd 239	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
237	224, 236	biimtrid 242	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠))
238	223, 237	sylbid 240	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠))
239	180, 238	sylan2 592	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠))
240	173, 239	syl5 34	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
241	240	ralrimivva 3208	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
242	241	adantr 480	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))
243		oveq2 7456	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
244	243	oveq1d 7463	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑖)))
245		oveq1 7455	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → (𝑡 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑖)))
246	244, 245	oveq12d 7466	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
247	246	eqeq2d 2751	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
248	247	ralbidv 3184	. . . . . . 7 ⊢ (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
249	248	reu4 3753	. . . . . 6 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠)))
250	169, 242, 249	sylanbrc 582	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
251		df-reu 3389	. . . . 5 ⊢ (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
252	250, 251	sylib 218	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
253	252	ralrimiva 3152	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
254		axcontlem2.2	. . . 4 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
255	254	fnopabg 6717	. . 3 ⊢ (∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ 𝐹 Fn 𝐷)
256	253, 255	sylib 218	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹 Fn 𝐷)
257	175	ad2antlr 726	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
258	182	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
259		fveere 28934	. . . . . . . . . . 11 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
260	258, 259	sylancom 587	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ)
261	185	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
262		fveere 28934	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
263	261, 262	sylancom 587	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ)
264		resubcl 11600	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
265	57, 264	mpan 689	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
266		remulcl 11269	. . . . . . . . . . . . 13 ⊢ (((1 − 𝑡) ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
267	265, 266	sylan 579	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
268	267	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ)
269		remulcl 11269	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
270	269	3adant2 1131	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ)
271	268, 270	readdcld 11319	. . . . . . . . . 10 ⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
272	257, 260, 263, 271	syl3anc 1371	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
273	272	ralrimiva 3152	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)
274		simpll1 1212	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
275		mptelee 28928	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
276	274, 275	syl 17	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ))
277	273, 276	mpbird 257	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
278		letric 11390	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
279	57, 175, 278	sylancr 586	. . . . . . . . 9 ⊢ (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
280	279	adantl 481	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1))
281		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
282	175	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
283		0red 11293	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
284		1red 11291	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
285		0lt1 11812	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 1
286	285	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
287	283, 284, 282, 286, 281	ltletrd 11450	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
288		divelunit 13554	. . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
291	281, 290	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
292	291	adantll 713	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
293	175	ad3antlr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
294	293	recnd 11318	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
295	287	gt0ne0d 11854	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
296	295	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
297	296	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
298	182	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
299	298, 29	sylancom 587	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
300	185	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
301	300, 187	sylancom 587	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
302		reccl 11956	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
303	302	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
304	190	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
305	304, 192, 193	syl2an 595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
306	195	ad2ant2rl 748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ)
307	303, 305, 306	adddid 11314	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))))
308	307	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
309		subcl 11535	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
310	71, 302, 309	sylancr 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
311		mulcl 11268	. . . . . . . . . . . . . . . . 17 ⊢ (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
312	310, 192, 311	syl2an 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
313	303, 305	mulcld 11310	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) ∈ ℂ)
314		recid2 11964	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
315	314	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
316	315	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖)))
317		simpll 766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
318		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
319	303, 317, 318	mulassd 11313	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))
320		mullid 11289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈‘𝑖) ∈ ℂ → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
321	320	ad2antll 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖))
322	316, 319, 321	3eqtr3d 2788	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) = (𝑈‘𝑖))
323	322, 318	eqeltrd 2844	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) ∈ ℂ)
324	312, 313, 323	addassd 11312	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))))
325	310	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
326	302, 304	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
327	326	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
328		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
329	325, 327, 328	adddird 11315	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))))
330		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
331		subdi 11723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
332	71, 331	mp3an2 1449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
333	302, 330, 332	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
334	302	mulridd 11307	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
335	334, 314	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
336	333, 335	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
337	336	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
338		npncan2 11563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
339	71, 302, 338	sylancr 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
340	337, 339	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
341	340	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
342	341	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖)))
343	108	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0)
344	342, 343	eqtrd 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = 0)
345	190	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
346	303, 345, 328	mulassd 11313	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))))
347	346	oveq2d 7464	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))))
348	329, 344, 347	3eqtr3rd 2789	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) = 0)
349	348, 322	oveq12d 7466	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (0 + (𝑈‘𝑖)))
350		addlid 11473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝑖) ∈ ℂ → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
351	350	ad2antll 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖))
352	349, 351	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (𝑈‘𝑖))
353	308, 324, 352	3eqtr2rd 2787	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
354	294, 297, 299, 301, 353	syl22anc 838	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
355	354	ralrimiva 3152	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
356		oveq2 7456	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
357	356	oveq1d 7463	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑍‘𝑖)))
358		oveq1 7455	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))
359	357, 358	oveq12d 7466	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
360	359	eqeq2d 2751	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (1 / 𝑡) → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
361	360	ralbidv 3184	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
362		fveq2 6920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑍‘𝑘) = (𝑍‘𝑖))
363	362	oveq2d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍‘𝑘)) = ((1 − 𝑡) · (𝑍‘𝑖)))
364		fveq2 6920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝑈‘𝑘) = (𝑈‘𝑖))
365	364	oveq2d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝑈‘𝑘)) = (𝑡 · (𝑈‘𝑖)))
366	363, 365	oveq12d 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
367		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))
368		ovex 7481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∈ V
369	366, 367, 368	fvmpt 7029	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
370	369	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
371	370	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
372	371	eqeq2d 2751	. . . . . . . . . . . . . . 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 287	. . . . . . . . . . . . 13 ⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))))
375	374	rspcev 3635	. . . . . . . . . . . 12 ⊢ (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))
376	292, 355, 375	syl2anc 583	. . . . . . . . . . 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 480	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
380		brbtwn 28932	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
381	377, 378, 379, 380	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))))
382	376, 381	mpbird 257	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
383	382	ex 412	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
384		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
385		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
386		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
387	384, 385, 386	3jca 1128	. . . . . . . . . . . . . 14 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
388	174	anbi1i 623	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
389		elicc01 13526	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
390	387, 388, 389	3imtr4i 292	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
391	390	adantll 713	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
392	369	rgen 3069	. . . . . . . . . . . 12 ⊢ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))
393		oveq2 7456	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
394	393	oveq1d 7463	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − 𝑡) · (𝑍‘𝑖)))
395		oveq1 7455	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑡 → (𝑠 · (𝑈‘𝑖)) = (𝑡 · (𝑈‘𝑖)))
396	394, 395	oveq12d 7466	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
397	396	eqeq2d 2751	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
398	397	ralbidv 3184	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
399	398	rspcev 3635	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
400	391, 392, 399	sylancl 585	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))
401	277	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁))
402	182	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
403	185	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
404		brbtwn 28932	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
405	401, 402, 403, 404	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))))
406	400, 405	mpbird 257	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
407	406	ex 412	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
408	383, 407	orim12d 965	. . . . . . . 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 4898	. . . . . . . . . 10 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩)
411	410	breq2d 5178	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩))
412		breq1 5169	. . . . . . . . 9 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
413	411, 412	orbi12d 917	. . . . . . . 8 ⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
414	413, 5	elrab2 3711	. . . . . . 7 ⊢ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
415	277, 409, 414	sylanbrc 582	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷)
416		fveq1 6919	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))
417	416	eqeq1d 2742	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
418	417	ralbidv 3184	. . . . . . 7 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
419	418	rspcev 3635	. . . . . 6 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
420	415, 392, 419	sylancl 585	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))
421	6	simplbi 497	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ (𝔼‘𝑁))
422	5	ssrab3 4105	. . . . . . . . . 10 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
423	422	sseli 4004	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ (𝔼‘𝑁))
424	421, 423	anim12i 612	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
425		r19.26 3117	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
426		eqtr3 2766	. . . . . . . . . . 11 ⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → (𝑥‘𝑖) = (𝑦‘𝑖))
427	426	ralimi 3089	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
428	425, 427	sylbir 235	. . . . . . . . 9 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
429		eqeefv 28936	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
430	429	adantl 481	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
431	428, 430	imbitrrid 246	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
432	424, 431	sylan2 592	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
433	432	ralrimivva 3208	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
434	433	adantr 480	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))
435		df-reu 3389	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
436		fveq1 6919	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥‘𝑖) = (𝑦‘𝑖))
437	436	eqeq1d 2742	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
438	437	ralbidv 3184	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
439	438	reu4 3753	. . . . . 6 ⊢ (∃!𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
440	435, 439	bitr3i 277	. . . . 5 ⊢ (∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)))
441	420, 434, 440	sylanbrc 582	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
442	441	ralrimiva 3152	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))
443		an12 644	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))
444	443	opabbii 5233	. . . . . . 7 ⊢ {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
445	254, 444	eqtri 2768	. . . . . 6 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
446	445	cnveqi 5899	. . . . 5 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
447		cnvopab 6169	. . . . 5 ⊢ ◡{⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
448	446, 447	eqtri 2768	. . . 4 ⊢ ◡𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
449	448	fnopabg 6717	. . 3 ⊢ (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ ◡𝐹 Fn (0[,)+∞))
450	442, 449	sylib 218	. 2 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ◡𝐹 Fn (0[,)+∞))
451		dff1o4 6870	. 2 ⊢ (𝐹:𝐷–1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷 ∧ ◡𝐹 Fn (0[,)+∞)))
452	256, 450, 451	sylanbrc 582	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹:𝐷–1-1-onto→(0[,)+∞))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∃!weu 2571   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  ∃!wreu 3386  {crab 3443   ⊆ wss 3976  ⟨cop 4654   class class class wbr 5166  {copab 5228   ↦ cmpt 5249  ^◡ccnv 5699   Fn wfn 6568  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189  +∞cpnf 11321   < clt 11324   ≤ cle 11325   − cmin 11520   / cdiv 11947  ℕcn 12293  [,)cico 13409  [,]cicc 13410  ...cfz 13567  𝔼cee 28921   Btwn cbtwn 28922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-z 12640  df-uz 12904  df-ico 13413  df-icc 13414  df-fz 13568  df-ee 28924  df-btwn 28925

This theorem is referenced by:  axcontlem5  29001  axcontlem9  29005  axcontlem10  29006