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

Theorem axcontlem2 25645
Description: Lemma for axcont 25656. The idea here is to set up a mapping 𝐹 that will allow us to transfer dedekind 10079 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 4341 . . . . . . . . . 10 (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
21breq2d 4595 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3 breq1 4586 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
42, 3orbi12d 742 . . . . . . . 8 (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5 axcontlem2.1 . . . . . . . 8 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
64, 5elrab2 3333 . . . . . . 7 (𝑥𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7 simpll3 1095 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8 simpll2 1094 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9 simpr 476 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10 brbtwn 25579 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
117, 8, 9, 10syl3anc 1318 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
1211biimpa 500 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))
13 simp-4r 803 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑍𝑈)
14 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15 1m0e1 11008 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 0) = 1
1614, 15syl6eq 2660 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (1 − 𝑠) = 1)
1716oveq1d 6564 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → ((1 − 𝑠) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
18 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 · (𝑥𝑖)) = (0 · (𝑥𝑖)))
1917, 18oveq12d 6567 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
2019eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑠 = 0 → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ (𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2120ralbidv 2969 . . . . . . . . . . . . . . . . 17 (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2221biimpac 502 . . . . . . . . . . . . . . . 16 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
23 eqcom 2617 . . . . . . . . . . . . . . . . 17 (𝑍 = 𝑈𝑈 = 𝑍)
247adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
258adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26 eqeefv 25583 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
2724, 25, 26syl2anc 691 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
288ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29 fveecn 25582 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3028, 29sylancom 698 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
31 simpllr 795 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
32 fveecn 25582 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
3331, 32sylancom 698 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
34 mulid2 9917 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
35 mul02 10093 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝑖) ∈ ℂ → (0 · (𝑥𝑖)) = 0)
3634, 35oveqan12d 6568 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = ((𝑍𝑖) + 0))
37 addid1 10095 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
3837adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
3936, 38eqtrd 2644 . . . . . . . . . . . . . . . . . . . . 21 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = (𝑍𝑖))
4039eqeq2d 2620 . . . . . . . . . . . . . . . . . . . 20 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4130, 33, 40syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4241ralbidva 2968 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
4327, 42bitr4d 270 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4423, 43syl5bb 271 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4522, 44syl5ibr 235 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
4645expdimp 452 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
4746necon3d 2803 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑍𝑈𝑠 ≠ 0))
4813, 47mpd 15 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑠 ≠ 0)
49 0re 9919 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℝ
50 1re 9918 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ
5149, 50elicc2i 12110 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
5251simp1bi 1069 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
53 rereccl 10622 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5452, 53sylan 487 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5552adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
5651simp2bi 1070 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
5756adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
58 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
5955, 57, 58ne0gt0d 10053 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
60 0le1 10430 . . . . . . . . . . . . . . . . . . 19 0 ≤ 1
61 divge0 10771 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
6250, 60, 61mpanl12 714 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
6355, 59, 62syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
64 elrege0 12149 . . . . . . . . . . . . . . . . 17 ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
6554, 63, 64sylanbrc 695 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6665adantll 746 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6752ad3antlr 763 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
6867recnd 9947 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
69 simplr 788 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
70 simp-4r 803 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
7170, 32sylancom 698 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
728ad3antrrr 762 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
7372, 29sylancom 698 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
74 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℂ
75 reccl 10571 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
76 subcl 10159 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
7774, 75, 76sylancr 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
7877adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
79 subcl 10159 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
8074, 79mpan 702 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
8180adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
8275, 81mulcld 9939 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
8382adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
84 simprr 792 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
8578, 83, 84adddird 9944 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
86 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
87 subdi 10342 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8874, 87mp3an2 1404 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8975, 86, 88syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
9089oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
9175mulid1d 9936 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
92 recid2 10579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
9391, 92oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
9493oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
95 addsubass 10170 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9674, 95mp3an3 1405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9777, 75, 96syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9877, 75addcld 9938 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
99 npcan 10169 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
10074, 75, 99sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
10198, 100subeq0bd 10335 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
10294, 97, 1013eqtr2d 2650 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
10390, 102eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
104103adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
105104oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
10675adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
10780ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
108106, 107, 84mulassd 9942 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
109108oveq2d 6565 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
11085, 105, 1093eqtr3rd 2653 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = (0 · (𝑍𝑖)))
111 mul02 10093 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍𝑖) ∈ ℂ → (0 · (𝑍𝑖)) = 0)
112111ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
113110, 112eqtrd 2644 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = 0)
114 simpll 786 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
115 simprl 790 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) ∈ ℂ)
116106, 114, 115mulassd 9942 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))
11792oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (1 · (𝑥𝑖)))
118 mulid2 9917 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑖) ∈ ℂ → (1 · (𝑥𝑖)) = (𝑥𝑖))
119118adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (1 · (𝑥𝑖)) = (𝑥𝑖))
120117, 119sylan9eq 2664 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (𝑥𝑖))
121116, 120eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) = (𝑥𝑖))
122113, 121oveq12d 6567 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (0 + (𝑥𝑖)))
12378, 84mulcld 9939 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
124 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
125 mulcl 9899 . . . . . . . . . . . . . . . . . . . . . 22 (((1 − 𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
12681, 124, 125syl2an 493 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
127106, 126mulcld 9939 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
128 mulcl 9899 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
129128ad2ant2r 779 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
130106, 129mulcld 9939 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) ∈ ℂ)
131123, 127, 130addassd 9941 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
132106, 126, 129adddid 9943 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))))
133132oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
134131, 133eqtr4d 2647 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
135 addid2 10098 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑖) ∈ ℂ → (0 + (𝑥𝑖)) = (𝑥𝑖))
136135ad2antrl 760 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 + (𝑥𝑖)) = (𝑥𝑖))
137122, 134, 1363eqtr3rd 2653 . . . . . . . . . . . . . . . . 17 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
13868, 69, 71, 73, 137syl22anc 1319 . . . . . . . . . . . . . . . 16 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
139138ralrimiva 2949 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
140 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
141140oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − (1 / 𝑠)) · (𝑍𝑖)))
142 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
143141, 142oveq12d 6567 . . . . . . . . . . . . . . . . . 18 (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
144143eqeq2d 2620 . . . . . . . . . . . . . . . . 17 (𝑡 = (1 / 𝑠) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
145144ralbidv 2969 . . . . . . . . . . . . . . . 16 (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
146145rspcev 3282 . . . . . . . . . . . . . . 15 (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
14766, 139, 146syl2anc 691 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
148 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (𝑡 · (𝑈𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
149148oveq2d 6565 . . . . . . . . . . . . . . . . . 18 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
150149eqeq2d 2620 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
151150ralimi 2936 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
152 ralbi 3050 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
153151, 152syl 17 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
154153rexbidv 3034 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
155147, 154syl5ibrcom 236 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
156155impancom 455 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑠 ≠ 0 → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
15748, 156mpd 15 . . . . . . . . . . 11 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
158157r19.29an 3059 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
15912, 158syldan 486 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
160 3simpa 1051 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
16149, 50elicc2i 12110 . . . . . . . . . . . 12 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
162 elrege0 12149 . . . . . . . . . . . 12 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
163160, 161, 1623imtr4i 280 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
164163ssriv 3572 . . . . . . . . . 10 (0[,]1) ⊆ (0[,)+∞)
165 brbtwn 25579 . . . . . . . . . . . 12 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
1669, 8, 7, 165syl3anc 1318 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
167166biimpa 500 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
168 ssrexv 3630 . . . . . . . . . 10 ((0[,]1) ⊆ (0[,)+∞) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
169164, 167, 168mpsyl 66 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
170159, 169jaodan 822 . . . . . . . 8 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
171170anasss 677 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
1726, 171sylan2b 491 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
173 r19.26 3046 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
174 eqtr2 2630 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
175174ralimi 2936 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
176173, 175sylbir 224 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
177 elrege0 12149 . . . . . . . . . . . . 13 (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
178177simplbi 475 . . . . . . . . . . . 12 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
179178recnd 9947 . . . . . . . . . . 11 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
180 elrege0 12149 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
181180simplbi 475 . . . . . . . . . . . 12 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
182181recnd 9947 . . . . . . . . . . 11 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
183179, 182anim12i 588 . . . . . . . . . 10 ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
184 simplr 788 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
185 simpl2 1058 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑍 ∈ (𝔼‘𝑁))
186185ad2antrr 758 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
187186, 29sylancom 698 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
188 simpl3 1059 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑈 ∈ (𝔼‘𝑁))
189188ad2antrr 758 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
190 fveecn 25582 . . . . . . . . . . . . . 14 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
191189, 190sylancom 698 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
192 subcl 10159 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
19374, 192mpan 702 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
194193adantr 480 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
195 simpl 472 . . . . . . . . . . . . . . . 16 (((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
196 mulcl 9899 . . . . . . . . . . . . . . . 16 (((1 − 𝑡) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
197194, 195, 196syl2an 493 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
198 mulcl 9899 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
199198ad2ant2rl 781 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
20080adantl 481 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
201200, 195, 125syl2an 493 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
202 mulcl 9899 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
203202ad2ant2l 778 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
204197, 199, 201, 203addsubeq4d 10322 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
205 nnncan1 10196 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
20674, 205mp3an1 1403 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
207206ancoms 468 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
208207oveq1d 6564 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
209208adantr 480 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
21080ad2antlr 759 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
211193ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
212 simprl 790 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
213210, 211, 212subdird 10366 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
214209, 213eqtr3d 2646 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
215 simpll 786 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
216 simplr 788 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
217 simprr 792 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
218215, 216, 217subdird 10366 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑈𝑖)) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖))))
219214, 218eqeq12d 2625 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
220 subcl 10159 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡𝑠) ∈ ℂ)
221220adantr 480 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡𝑠) ∈ ℂ)
222 mulcan1g 10559 . . . . . . . . . . . . . . 15 (((𝑡𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
223221, 212, 217, 222syl3anc 1318 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
224204, 219, 2233bitr2d 295 . . . . . . . . . . . . 13 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
225184, 187, 191, 224syl12anc 1316 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
226225ralbidva 2968 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
227 r19.32v 3064 . . . . . . . . . . . 12 (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
228 simplr 788 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍𝑈)
229228neneqd 2787 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
230 simpll2 1094 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
231 simpll3 1095 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
232 eqeefv 25583 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
233230, 231, 232syl2anc 691 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
234229, 233mtbid 313 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖))
235 orel2 397 . . . . . . . . . . . . . 14 (¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
236234, 235syl 17 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
237 subeq0 10186 . . . . . . . . . . . . . 14 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
238237adantl 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
239236, 238sylibd 228 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
240227, 239syl5bi 231 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
241226, 240sylbid 229 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
242183, 241sylan2 490 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
243176, 242syl5 33 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
244243ralrimivva 2954 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
245244adantr 480 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
246 oveq2 6557 . . . . . . . . . . 11 (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
247246oveq1d 6564 . . . . . . . . . 10 (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − 𝑠) · (𝑍𝑖)))
248 oveq1 6556 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑡 · (𝑈𝑖)) = (𝑠 · (𝑈𝑖)))
249247, 248oveq12d 6567 . . . . . . . . 9 (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
250249eqeq2d 2620 . . . . . . . 8 (𝑡 = 𝑠 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
251250ralbidv 2969 . . . . . . 7 (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
252251reu4 3367 . . . . . 6 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠)))
253172, 245, 252sylanbrc 695 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
254 df-reu 2903 . . . . 5 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
255253, 254sylib 207 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
256255ralrimiva 2949 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
257 axcontlem2.2 . . . 4 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
258257fnopabg 5930 . . 3 (∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn 𝐷)
259256, 258sylib 207 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn 𝐷)
260178ad2antlr 759 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
261185ad2antrr 758 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
262 fveere 25581 . . . . . . . . . . 11 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
263261, 262sylancom 698 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
264188ad2antrr 758 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
265 fveere 25581 . . . . . . . . . . 11 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
266264, 265sylancom 698 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
267 resubcl 10224 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
26850, 267mpan 702 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
269 remulcl 9900 . . . . . . . . . . . . 13 (((1 − 𝑡) ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
270268, 269sylan 487 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
2712703adant3 1074 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
272 remulcl 9900 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
2732723adant2 1073 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
274271, 273readdcld 9948 . . . . . . . . . 10 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
275260, 263, 266, 274syl3anc 1318 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
276275ralrimiva 2949 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
277 simpll1 1093 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
278 mptelee 25575 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
279277, 278syl 17 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
280276, 279mpbird 246 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
281 letric 10016 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡𝑡 ≤ 1))
28250, 178, 281sylancr 694 . . . . . . . . 9 (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡𝑡 ≤ 1))
283282adantl 481 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑡 ≤ 1))
284 simpr 476 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
285178adantr 480 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
286 0red 9920 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
287 1red 9934 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
288 0lt1 10429 . . . . . . . . . . . . . . . . 17 0 < 1
289288a1i 11 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
290286, 287, 285, 289, 284ltletrd 10076 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
291 divelunit 12185 . . . . . . . . . . . . . . . 16 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
29250, 60, 291mpanl12 714 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
293285, 290, 292syl2anc 691 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
294284, 293mpbird 246 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
295294adantll 746 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
296178ad3antlr 763 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
297296recnd 9947 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
298290gt0ne0d 10471 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
299298adantll 746 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
300299adantr 480 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
301185ad3antrrr 762 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
302301, 29sylancom 698 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
303188ad3antrrr 762 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
304303, 190sylancom 698 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
305 reccl 10571 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
306305adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
307193adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
308307, 195, 196syl2an 493 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
309198ad2ant2rl 781 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
310306, 308, 309adddid 9943 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))))
311310oveq2d 6565 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
312 subcl 10159 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
31374, 305, 312sylancr 694 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
314 mulcl 9899 . . . . . . . . . . . . . . . . 17 (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
315313, 195, 314syl2an 493 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
316306, 308mulcld 9939 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
317 recid2 10579 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
318317oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
319318adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
320 simpll 786 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
321 simprr 792 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
322306, 320, 321mulassd 9942 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))
323 mulid2 9917 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) ∈ ℂ → (1 · (𝑈𝑖)) = (𝑈𝑖))
324323ad2antll 761 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (𝑈𝑖)) = (𝑈𝑖))
325319, 322, 3243eqtr3d 2652 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) = (𝑈𝑖))
326325, 321eqeltrd 2688 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) ∈ ℂ)
327315, 316, 326addassd 9941 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
328313adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
329305, 307mulcld 9939 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
330329adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
331 simprl 790 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
332328, 330, 331adddird 9944 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
333 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
334 subdi 10342 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
33574, 334mp3an2 1404 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
336305, 333, 335syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
337305mulid1d 9936 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
338337, 317oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
339336, 338eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
340339oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
341 npncan2 10187 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
34274, 305, 341sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
343340, 342eqtrd 2644 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
344343adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
345344oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
346111ad2antrl 760 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
347345, 346eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = 0)
348193ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
349306, 348, 331mulassd 9942 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
350349oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
351332, 347, 3503eqtr3rd 2653 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = 0)
352351, 325oveq12d 6567 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (0 + (𝑈𝑖)))
353 addid2 10098 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) ∈ ℂ → (0 + (𝑈𝑖)) = (𝑈𝑖))
354353ad2antll 761 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 + (𝑈𝑖)) = (𝑈𝑖))
355352, 354eqtrd 2644 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (𝑈𝑖))
356311, 327, 3553eqtr2rd 2651 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
357297, 300, 302, 304, 356syl22anc 1319 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
358357ralrimiva 2949 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
359 oveq2 6557 . . . . . . . . . . . . . . . . . 18 (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
360359oveq1d 6564 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − (1 / 𝑡)) · (𝑍𝑖)))
361 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))
362360, 361oveq12d 6567 . . . . . . . . . . . . . . . 16 (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
363362eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑠 = (1 / 𝑡) → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
364363ralbidv 2969 . . . . . . . . . . . . . 14 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
365 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑍𝑘) = (𝑍𝑖))
366365oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍𝑘)) = ((1 − 𝑡) · (𝑍𝑖)))
367 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑈𝑘) = (𝑈𝑖))
368367oveq2d 6565 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (𝑡 · (𝑈𝑘)) = (𝑡 · (𝑈𝑖)))
369366, 368oveq12d 6567 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
370 eqid 2610 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))
371 ovex 6577 . . . . . . . . . . . . . . . . . . 19 (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∈ V
372369, 370, 371fvmpt 6191 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
373372oveq2d 6565 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
374373oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
375374eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑁) → ((𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
376375ralbiia 2962 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
377364, 376syl6bb 275 . . . . . . . . . . . . 13 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
378377rspcev 3282 . . . . . . . . . . . 12 (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
379295, 358, 378syl2anc 691 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
380188ad2antrr 758 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 ∈ (𝔼‘𝑁))
381185ad2antrr 758 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑍 ∈ (𝔼‘𝑁))
382280adantr 480 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
383 brbtwn 25579 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
384380, 381, 382, 383syl3anc 1318 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
385379, 384mpbird 246 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
386385ex 449 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
387 simpll 786 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
388 simplr 788 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
389 simpr 476 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
390387, 388, 3893jca 1235 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
391177anbi1i 727 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
39249, 50elicc2i 12110 . . . . . . . . . . . . . 14 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
393390, 391, 3923imtr4i 280 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
394393adantll 746 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
395372rgen 2906 . . . . . . . . . . . 12 𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))
396 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
397396oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
398 oveq1 6556 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → (𝑠 · (𝑈𝑖)) = (𝑡 · (𝑈𝑖)))
399397, 398oveq12d 6567 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
400399eqeq2d 2620 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
401400ralbidv 2969 . . . . . . . . . . . . 13 (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
402401rspcev 3282 . . . . . . . . . . . 12 ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
403394, 395, 402sylancl 693 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
404280adantr 480 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
405185ad2antrr 758 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
406188ad2antrr 758 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
407 brbtwn 25579 . . . . . . . . . . . 12 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
408404, 405, 406, 407syl3anc 1318 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
409403, 408mpbird 246 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
410409ex 449 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
411386, 410orim12d 879 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((1 ≤ 𝑡𝑡 ≤ 1) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
412283, 411mpd 15 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
413 opeq2 4341 . . . . . . . . . 10 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
414413breq2d 4595 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
415 breq1 4586 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
416414, 415orbi12d 742 . . . . . . . 8 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
417416, 5elrab2 3333 . . . . . . 7 ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
418280, 412, 417sylanbrc 695 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷)
419 fveq1 6102 . . . . . . . . 9 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑥𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))
420419eqeq1d 2612 . . . . . . . 8 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
421420ralbidv 2969 . . . . . . 7 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
422421rspcev 3282 . . . . . 6 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
423418, 395, 422sylancl 693 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
4246simplbi 475 . . . . . . . . 9 (𝑥𝐷𝑥 ∈ (𝔼‘𝑁))
425 ssrab2 3650 . . . . . . . . . . 11 {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ⊆ (𝔼‘𝑁)
4265, 425eqsstri 3598 . . . . . . . . . 10 𝐷 ⊆ (𝔼‘𝑁)
427426sseli 3564 . . . . . . . . 9 (𝑦𝐷𝑦 ∈ (𝔼‘𝑁))
428424, 427anim12i 588 . . . . . . . 8 ((𝑥𝐷𝑦𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
429 r19.26 3046 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
430 eqtr3 2631 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → (𝑥𝑖) = (𝑦𝑖))
431430ralimi 2936 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
432429, 431sylbir 224 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
433 eqeefv 25583 . . . . . . . . . 10 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
434433adantl 481 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
435432, 434syl5ibr 235 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
436428, 435sylan2 490 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥𝐷𝑦𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
437436ralrimivva 2954 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
438437adantr 480 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
439 df-reu 2903 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
440 fveq1 6102 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
441440eqeq1d 2612 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
442441ralbidv 2969 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
443442reu4 3367 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
444439, 443bitr3i 265 . . . . 5 (∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
445423, 438, 444sylanbrc 695 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
446445ralrimiva 2949 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
447 an12 834 . . . . . . . 8 ((𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
448447opabbii 4649 . . . . . . 7 {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
449257, 448eqtri 2632 . . . . . 6 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
450449cnveqi 5219 . . . . 5 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
451 cnvopab 5452 . . . . 5 {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
452450, 451eqtri 2632 . . . 4 𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
453452fnopabg 5930 . . 3 (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn (0[,)+∞))
454446, 453sylib 207 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn (0[,)+∞))
455 dff1o4 6058 . 2 (𝐹:𝐷1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷𝐹 Fn (0[,)+∞)))
456259, 454, 455sylanbrc 695 1 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹:𝐷1-1-onto→(0[,)+∞))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383  w3a 1031   = wceq 1475  wcel 1977  ∃!weu 2458  wne 2780  wral 2896  wrex 2897  ∃!wreu 2898  {crab 2900  wss 3540  cop 4131   class class class wbr 4583  {copab 4642  cmpt 4643  ccnv 5037   Fn wfn 5799  1-1-ontowf1o 5803  cfv 5804  (class class class)co 6549  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950   < clt 9953  cle 9954  cmin 10145   / cdiv 10563  cn 10897  [,)cico 12048  [,]cicc 12049  ...cfz 12197  𝔼cee 25568   Btwn cbtwn 25569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-z 11255  df-uz 11564  df-ico 12052  df-icc 12053  df-fz 12198  df-ee 25571  df-btwn 25572
This theorem is referenced by:  axcontlem5  25648  axcontlem9  25652  axcontlem10  25653
  Copyright terms: Public domain W3C validator