MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axcontlem2 Structured version   Visualization version   GIF version

Theorem axcontlem2 26053
Description: Lemma for axcont 26064. The idea here is to set up a mapping 𝐹 that will allow us to transfer dedekind 10479 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.
StepHypRef Expression
1 opeq2 4589 . . . . . . . . . 10 (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
21breq2d 4849 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3 breq1 4840 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
42, 3orbi12d 933 . . . . . . . 8 (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5 axcontlem2.1 . . . . . . . 8 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
64, 5elrab2 3558 . . . . . . 7 (𝑥𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7 simpll3 1266 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8 simpll2 1264 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9 simpr 473 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10 brbtwn 25987 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
117, 8, 9, 10syl3anc 1483 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
1211biimpa 464 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))
13 simp-4r 794 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑍𝑈)
14 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15 1m0e1 11407 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 0) = 1
1614, 15syl6eq 2852 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (1 − 𝑠) = 1)
1716oveq1d 6883 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → ((1 − 𝑠) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
18 oveq1 6875 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 · (𝑥𝑖)) = (0 · (𝑥𝑖)))
1917, 18oveq12d 6886 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
2019eqeq2d 2812 . . . . . . . . . . . . . . . . . 18 (𝑠 = 0 → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ (𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2120ralbidv 3170 . . . . . . . . . . . . . . . . 17 (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2221biimpac 466 . . . . . . . . . . . . . . . 16 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
23 eqcom 2809 . . . . . . . . . . . . . . . . 17 (𝑍 = 𝑈𝑈 = 𝑍)
247adantr 468 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
258adantr 468 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26 eqeefv 25991 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
2724, 25, 26syl2anc 575 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
288ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29 fveecn 25990 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3028, 29sylancom 578 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
31 simpllr 784 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
32 fveecn 25990 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
3331, 32sylancom 578 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
34 mulid2 10318 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
35 mul02 10493 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝑖) ∈ ℂ → (0 · (𝑥𝑖)) = 0)
3634, 35oveqan12d 6887 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = ((𝑍𝑖) + 0))
37 addid1 10495 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
3837adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
3936, 38eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = (𝑍𝑖))
4039eqeq2d 2812 . . . . . . . . . . . . . . . . . . . 20 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4130, 33, 40syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4241ralbidva 3169 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
4327, 42bitr4d 273 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4423, 43syl5bb 274 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4522, 44syl5ibr 237 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
4645expdimp 442 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
4746necon3d 2995 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑍𝑈𝑠 ≠ 0))
4813, 47mpd 15 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑠 ≠ 0)
49 elicc01 12504 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
5049simp1bi 1168 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
51 rereccl 11022 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5250, 51sylan 571 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5350adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
5449simp2bi 1169 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
5554adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
56 simpr 473 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
5753, 55, 56ne0gt0d 10453 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
58 1re 10319 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
59 0le1 10830 . . . . . . . . . . . . . . . . . . 19 0 ≤ 1
60 divge0 11171 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
6158, 59, 60mpanl12 685 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
6253, 57, 61syl2anc 575 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
63 elrege0 12492 . . . . . . . . . . . . . . . . 17 ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
6452, 62, 63sylanbrc 574 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6564adantll 696 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6650ad3antlr 713 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
6766recnd 10347 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
68 simplr 776 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
69 simp-4r 794 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
7069, 32sylancom 578 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
718ad3antrrr 712 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
7271, 29sylancom 578 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
73 ax-1cn 10273 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℂ
74 reccl 10971 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
75 subcl 10559 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
7673, 74, 75sylancr 577 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
7776adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
78 subcl 10559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
7973, 78mpan 673 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
8079adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
8174, 80mulcld 10339 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
8281adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
83 simprr 780 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
8477, 82, 83adddird 10344 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
85 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
86 subdi 10742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8773, 86mp3an2 1566 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8874, 85, 87syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8988oveq2d 6884 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
9074mulid1d 10336 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
91 recid2 10979 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
9290, 91oveq12d 6886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
9392oveq2d 6884 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
94 addsubass 10570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9573, 94mp3an3 1567 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9676, 74, 95syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9776, 74addcld 10338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
98 npcan 10569 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
9973, 74, 98sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
10097, 99subeq0bd 10735 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
10193, 96, 1003eqtr2d 2842 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
10289, 101eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
103102adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
104103oveq1d 6883 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
10574adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
10679ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
107105, 106, 83mulassd 10342 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
108107oveq2d 6884 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
10984, 104, 1083eqtr3rd 2845 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = (0 · (𝑍𝑖)))
110 mul02 10493 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍𝑖) ∈ ℂ → (0 · (𝑍𝑖)) = 0)
111110ad2antll 711 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
112109, 111eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = 0)
113 simpll 774 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
114 simprl 778 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) ∈ ℂ)
115105, 113, 114mulassd 10342 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))
11691oveq1d 6883 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (1 · (𝑥𝑖)))
117 mulid2 10318 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑖) ∈ ℂ → (1 · (𝑥𝑖)) = (𝑥𝑖))
118117adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (1 · (𝑥𝑖)) = (𝑥𝑖))
119116, 118sylan9eq 2856 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (𝑥𝑖))
120115, 119eqtr3d 2838 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) = (𝑥𝑖))
121112, 120oveq12d 6886 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (0 + (𝑥𝑖)))
12277, 83mulcld 10339 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
123 simpr 473 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
124 mulcl 10299 . . . . . . . . . . . . . . . . . . . . . 22 (((1 − 𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
12580, 123, 124syl2an 585 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
126105, 125mulcld 10339 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
127 mulcl 10299 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
128127ad2ant2r 744 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
129105, 128mulcld 10339 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) ∈ ℂ)
130122, 126, 129addassd 10341 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
131105, 125, 128adddid 10343 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))))
132131oveq2d 6884 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
133130, 132eqtr4d 2839 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
134 addid2 10498 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑖) ∈ ℂ → (0 + (𝑥𝑖)) = (𝑥𝑖))
135134ad2antrl 710 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 + (𝑥𝑖)) = (𝑥𝑖))
136121, 133, 1353eqtr3rd 2845 . . . . . . . . . . . . . . . . 17 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
13767, 68, 70, 72, 136syl22anc 858 . . . . . . . . . . . . . . . 16 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
138137ralrimiva 3150 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
139 oveq2 6876 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
140139oveq1d 6883 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − (1 / 𝑠)) · (𝑍𝑖)))
141 oveq1 6875 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
142140, 141oveq12d 6886 . . . . . . . . . . . . . . . . . 18 (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
143142eqeq2d 2812 . . . . . . . . . . . . . . . . 17 (𝑡 = (1 / 𝑠) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
144143ralbidv 3170 . . . . . . . . . . . . . . . 16 (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
145144rspcev 3498 . . . . . . . . . . . . . . 15 (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
14665, 138, 145syl2anc 575 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
147 oveq2 6876 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (𝑡 · (𝑈𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
148147oveq2d 6884 . . . . . . . . . . . . . . . . . 18 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
149148eqeq2d 2812 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
150149ralimi 3136 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
151 ralbi 3252 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
152150, 151syl 17 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
153152rexbidv 3236 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
154146, 153syl5ibrcom 238 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
155154impancom 441 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑠 ≠ 0 → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
15648, 155mpd 15 . . . . . . . . . . 11 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
157156r19.29an 3261 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
15812, 157syldan 581 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
159 3simpa 1171 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
160 elicc01 12504 . . . . . . . . . . . 12 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
161 elrege0 12492 . . . . . . . . . . . 12 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
162159, 160, 1613imtr4i 283 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
163162ssriv 3796 . . . . . . . . . 10 (0[,]1) ⊆ (0[,)+∞)
164 brbtwn 25987 . . . . . . . . . . . 12 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
1659, 8, 7, 164syl3anc 1483 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
166165biimpa 464 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
167 ssrexv 3858 . . . . . . . . . 10 ((0[,]1) ⊆ (0[,)+∞) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
168163, 166, 167mpsyl 68 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
169158, 168jaodan 971 . . . . . . . 8 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
170169anasss 454 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
1716, 170sylan2b 583 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
172 r19.26 3248 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
173 eqtr2 2822 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
174173ralimi 3136 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
175172, 174sylbir 226 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
176 elrege0 12492 . . . . . . . . . . . . 13 (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
177176simplbi 487 . . . . . . . . . . . 12 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
178177recnd 10347 . . . . . . . . . . 11 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
179 elrege0 12492 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
180179simplbi 487 . . . . . . . . . . . 12 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
181180recnd 10347 . . . . . . . . . . 11 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
182178, 181anim12i 602 . . . . . . . . . 10 ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
183 simplr 776 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
184 simpl2 1237 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑍 ∈ (𝔼‘𝑁))
185184ad2antrr 708 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
186185, 29sylancom 578 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
187 simpl3 1239 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑈 ∈ (𝔼‘𝑁))
188187ad2antrr 708 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
189 fveecn 25990 . . . . . . . . . . . . . 14 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
190188, 189sylancom 578 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
191 subcl 10559 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
19273, 191mpan 673 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
193192adantr 468 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
194 simpl 470 . . . . . . . . . . . . . . . 16 (((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
195 mulcl 10299 . . . . . . . . . . . . . . . 16 (((1 − 𝑡) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
196193, 194, 195syl2an 585 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
197 mulcl 10299 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
198197ad2ant2rl 746 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
19979adantl 469 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
200199, 194, 124syl2an 585 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
201 mulcl 10299 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
202201ad2ant2l 743 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
203196, 198, 200, 202addsubeq4d 10722 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
204 nnncan1 10596 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
20573, 204mp3an1 1565 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
206205ancoms 448 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
207206oveq1d 6883 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
208207adantr 468 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
20979ad2antlr 709 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
210192ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
211 simprl 778 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
212209, 210, 211subdird 10766 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
213208, 212eqtr3d 2838 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
214 simpll 774 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
215 simplr 776 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
216 simprr 780 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
217214, 215, 216subdird 10766 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑈𝑖)) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖))))
218213, 217eqeq12d 2817 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
219 subcl 10559 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡𝑠) ∈ ℂ)
220219adantr 468 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡𝑠) ∈ ℂ)
221 mulcan1g 10959 . . . . . . . . . . . . . . 15 (((𝑡𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
222220, 211, 216, 221syl3anc 1483 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
223203, 218, 2223bitr2d 298 . . . . . . . . . . . . 13 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
224183, 186, 190, 223syl12anc 856 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
225224ralbidva 3169 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
226 r19.32v 3267 . . . . . . . . . . . 12 (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
227 simplr 776 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍𝑈)
228227neneqd 2979 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
229 simpll2 1264 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
230 simpll3 1266 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
231 eqeefv 25991 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
232229, 230, 231syl2anc 575 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
233228, 232mtbid 315 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖))
234 orel2 906 . . . . . . . . . . . . . 14 (¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
235233, 234syl 17 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
236 subeq0 10586 . . . . . . . . . . . . . 14 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
237236adantl 469 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
238235, 237sylibd 230 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
239226, 238syl5bi 233 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
240225, 239sylbid 231 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
241182, 240sylan2 582 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
242175, 241syl5 34 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
243242ralrimivva 3155 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
244243adantr 468 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
245 oveq2 6876 . . . . . . . . . . 11 (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
246245oveq1d 6883 . . . . . . . . . 10 (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − 𝑠) · (𝑍𝑖)))
247 oveq1 6875 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑡 · (𝑈𝑖)) = (𝑠 · (𝑈𝑖)))
248246, 247oveq12d 6886 . . . . . . . . 9 (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
249248eqeq2d 2812 . . . . . . . 8 (𝑡 = 𝑠 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
250249ralbidv 3170 . . . . . . 7 (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
251250reu4 3592 . . . . . 6 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠)))
252171, 244, 251sylanbrc 574 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
253 df-reu 3099 . . . . 5 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
254252, 253sylib 209 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
255254ralrimiva 3150 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
256 axcontlem2.2 . . . 4 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
257256fnopabg 6222 . . 3 (∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn 𝐷)
258255, 257sylib 209 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn 𝐷)
259177ad2antlr 709 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
260184ad2antrr 708 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
261 fveere 25989 . . . . . . . . . . 11 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
262260, 261sylancom 578 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
263187ad2antrr 708 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
264 fveere 25989 . . . . . . . . . . 11 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
265263, 264sylancom 578 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
266 resubcl 10624 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
26758, 266mpan 673 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
268 remulcl 10300 . . . . . . . . . . . . 13 (((1 − 𝑡) ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
269267, 268sylan 571 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
2702693adant3 1155 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
271 remulcl 10300 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
2722713adant2 1154 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
273270, 272readdcld 10348 . . . . . . . . . 10 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
274259, 262, 265, 273syl3anc 1483 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
275274ralrimiva 3150 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
276 simpll1 1262 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
277 mptelee 25983 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
278276, 277syl 17 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
279275, 278mpbird 248 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
280 letric 10416 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡𝑡 ≤ 1))
28158, 177, 280sylancr 577 . . . . . . . . 9 (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡𝑡 ≤ 1))
282281adantl 469 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑡 ≤ 1))
283 simpr 473 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
284177adantr 468 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
285 0red 10322 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
286 1red 10320 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
287 0lt1 10829 . . . . . . . . . . . . . . . . 17 0 < 1
288287a1i 11 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
289285, 286, 284, 288, 283ltletrd 10476 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
290 divelunit 12531 . . . . . . . . . . . . . . . 16 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
29158, 59, 290mpanl12 685 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
292284, 289, 291syl2anc 575 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
293283, 292mpbird 248 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
294293adantll 696 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
295177ad3antlr 713 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
296295recnd 10347 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
297289gt0ne0d 10871 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
298297adantll 696 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
299298adantr 468 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
300184ad3antrrr 712 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
301300, 29sylancom 578 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
302187ad3antrrr 712 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
303302, 189sylancom 578 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
304 reccl 10971 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
305304adantr 468 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
306192adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
307306, 194, 195syl2an 585 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
308197ad2ant2rl 746 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
309305, 307, 308adddid 10343 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))))
310309oveq2d 6884 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
311 subcl 10559 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
31273, 304, 311sylancr 577 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
313 mulcl 10299 . . . . . . . . . . . . . . . . 17 (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
314312, 194, 313syl2an 585 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
315305, 307mulcld 10339 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
316 recid2 10979 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
317316oveq1d 6883 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
318317adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
319 simpll 774 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
320 simprr 780 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
321305, 319, 320mulassd 10342 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))
322 mulid2 10318 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) ∈ ℂ → (1 · (𝑈𝑖)) = (𝑈𝑖))
323322ad2antll 711 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (𝑈𝑖)) = (𝑈𝑖))
324318, 321, 3233eqtr3d 2844 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) = (𝑈𝑖))
325324, 320eqeltrd 2881 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) ∈ ℂ)
326314, 315, 325addassd 10341 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
327312adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
328304, 306mulcld 10339 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
329328adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
330 simprl 778 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
331327, 329, 330adddird 10344 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
332 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
333 subdi 10742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
33473, 333mp3an2 1566 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
335304, 332, 334syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
336304mulid1d 10336 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
337336, 316oveq12d 6886 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
338335, 337eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
339338oveq2d 6884 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
340 npncan2 10587 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
34173, 304, 340sylancr 577 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
342339, 341eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
343342adantr 468 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
344343oveq1d 6883 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
345110ad2antrl 710 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
346344, 345eqtrd 2836 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = 0)
347192ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
348305, 347, 330mulassd 10342 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
349348oveq2d 6884 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
350331, 346, 3493eqtr3rd 2845 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = 0)
351350, 324oveq12d 6886 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (0 + (𝑈𝑖)))
352 addid2 10498 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) ∈ ℂ → (0 + (𝑈𝑖)) = (𝑈𝑖))
353352ad2antll 711 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 + (𝑈𝑖)) = (𝑈𝑖))
354351, 353eqtrd 2836 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (𝑈𝑖))
355310, 326, 3543eqtr2rd 2843 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
356296, 299, 301, 303, 355syl22anc 858 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
357356ralrimiva 3150 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
358 oveq2 6876 . . . . . . . . . . . . . . . . . 18 (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
359358oveq1d 6883 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − (1 / 𝑡)) · (𝑍𝑖)))
360 oveq1 6875 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))
361359, 360oveq12d 6886 . . . . . . . . . . . . . . . 16 (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
362361eqeq2d 2812 . . . . . . . . . . . . . . 15 (𝑠 = (1 / 𝑡) → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
363362ralbidv 3170 . . . . . . . . . . . . . 14 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
364 fveq2 6402 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑍𝑘) = (𝑍𝑖))
365364oveq2d 6884 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍𝑘)) = ((1 − 𝑡) · (𝑍𝑖)))
366 fveq2 6402 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑈𝑘) = (𝑈𝑖))
367366oveq2d 6884 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (𝑡 · (𝑈𝑘)) = (𝑡 · (𝑈𝑖)))
368365, 367oveq12d 6886 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
369 eqid 2802 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))
370 ovex 6900 . . . . . . . . . . . . . . . . . . 19 (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∈ V
371368, 369, 370fvmpt 6497 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
372371oveq2d 6884 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
373372oveq2d 6884 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
374373eqeq2d 2812 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑁) → ((𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
375374ralbiia 3163 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
376363, 375syl6bb 278 . . . . . . . . . . . . 13 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
377376rspcev 3498 . . . . . . . . . . . 12 (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
378294, 357, 377syl2anc 575 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
379187ad2antrr 708 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 ∈ (𝔼‘𝑁))
380184ad2antrr 708 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑍 ∈ (𝔼‘𝑁))
381279adantr 468 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
382 brbtwn 25987 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
383379, 380, 381, 382syl3anc 1483 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
384378, 383mpbird 248 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
385384ex 399 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
386 simpll 774 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
387 simplr 776 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
388 simpr 473 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
389386, 387, 3883jca 1151 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
390176anbi1i 612 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
391 elicc01 12504 . . . . . . . . . . . . . 14 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
392389, 390, 3913imtr4i 283 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
393392adantll 696 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
394371rgen 3106 . . . . . . . . . . . 12 𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))
395 oveq2 6876 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
396395oveq1d 6883 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
397 oveq1 6875 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → (𝑠 · (𝑈𝑖)) = (𝑡 · (𝑈𝑖)))
398396, 397oveq12d 6886 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
399398eqeq2d 2812 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
400399ralbidv 3170 . . . . . . . . . . . . 13 (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
401400rspcev 3498 . . . . . . . . . . . 12 ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
402393, 394, 401sylancl 576 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
403279adantr 468 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
404184ad2antrr 708 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
405187ad2antrr 708 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
406 brbtwn 25987 . . . . . . . . . . . 12 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
407403, 404, 405, 406syl3anc 1483 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
408402, 407mpbird 248 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
409408ex 399 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
410385, 409orim12d 978 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((1 ≤ 𝑡𝑡 ≤ 1) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
411282, 410mpd 15 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
412 opeq2 4589 . . . . . . . . . 10 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
413412breq2d 4849 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
414 breq1 4840 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
415413, 414orbi12d 933 . . . . . . . 8 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
416415, 5elrab2 3558 . . . . . . 7 ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
417279, 411, 416sylanbrc 574 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷)
418 fveq1 6401 . . . . . . . . 9 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑥𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))
419418eqeq1d 2804 . . . . . . . 8 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
420419ralbidv 3170 . . . . . . 7 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
421420rspcev 3498 . . . . . 6 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
422417, 394, 421sylancl 576 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
4236simplbi 487 . . . . . . . . 9 (𝑥𝐷𝑥 ∈ (𝔼‘𝑁))
424 ssrab2 3878 . . . . . . . . . . 11 {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ⊆ (𝔼‘𝑁)
4255, 424eqsstri 3826 . . . . . . . . . 10 𝐷 ⊆ (𝔼‘𝑁)
426425sseli 3788 . . . . . . . . 9 (𝑦𝐷𝑦 ∈ (𝔼‘𝑁))
427423, 426anim12i 602 . . . . . . . 8 ((𝑥𝐷𝑦𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
428 r19.26 3248 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
429 eqtr3 2823 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → (𝑥𝑖) = (𝑦𝑖))
430429ralimi 3136 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
431428, 430sylbir 226 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
432 eqeefv 25991 . . . . . . . . . 10 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
433432adantl 469 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
434431, 433syl5ibr 237 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
435427, 434sylan2 582 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥𝐷𝑦𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
436435ralrimivva 3155 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
437436adantr 468 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
438 df-reu 3099 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
439 fveq1 6401 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
440439eqeq1d 2804 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
441440ralbidv 3170 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
442441reu4 3592 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
443438, 442bitr3i 268 . . . . 5 (∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
444422, 437, 443sylanbrc 574 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
445444ralrimiva 3150 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
446 an12 627 . . . . . . . 8 ((𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
447446opabbii 4904 . . . . . . 7 {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
448256, 447eqtri 2824 . . . . . 6 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
449448cnveqi 5492 . . . . 5 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
450 cnvopab 5738 . . . . 5 {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
451449, 450eqtri 2824 . . . 4 𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
452451fnopabg 6222 . . 3 (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn (0[,)+∞))
453445, 452sylib 209 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn (0[,)+∞))
454 dff1o4 6355 . 2 (𝐹:𝐷1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷𝐹 Fn (0[,)+∞)))
455258, 453, 454sylanbrc 574 1 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹:𝐷1-1-onto→(0[,)+∞))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2155  ∃!weu 2629  wne 2974  wral 3092  wrex 3093  ∃!wreu 3094  {crab 3096  wss 3763  cop 4370   class class class wbr 4837  {copab 4899  cmpt 4916  ccnv 5304   Fn wfn 6090  1-1-ontowf1o 6094  cfv 6095  (class class class)co 6868  cc 10213  cr 10214  0cc0 10215  1c1 10216   + caddc 10218   · cmul 10220  +∞cpnf 10350   < clt 10353  cle 10354  cmin 10545   / cdiv 10963  cn 11299  [,)cico 12389  [,]cicc 12390  ...cfz 12543  𝔼cee 25976   Btwn cbtwn 25977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-er 7973  df-map 8088  df-en 8187  df-dom 8188  df-sdom 8189  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-z 11638  df-uz 11899  df-ico 12393  df-icc 12394  df-fz 12544  df-ee 25979  df-btwn 25980
This theorem is referenced by:  axcontlem5  26056  axcontlem9  26060  axcontlem10  26061
  Copyright terms: Public domain W3C validator