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

Theorem axcontlem2 25890
 Description: Lemma for axcont 25901. The idea here is to set up a mapping 𝐹 that will allow us to transfer dedekind 10238 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 4434 . . . . . . . . . 10 (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
21breq2d 4697 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3 breq1 4688 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
42, 3orbi12d 746 . . . . . . . 8 (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5 axcontlem2.1 . . . . . . . 8 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
64, 5elrab2 3399 . . . . . . 7 (𝑥𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7 simpll3 1122 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8 simpll2 1121 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9 simpr 476 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10 brbtwn 25824 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
117, 8, 9, 10syl3anc 1366 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
1211biimpa 500 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))
13 simp-4r 824 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑍𝑈)
14 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15 1m0e1 11169 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 0) = 1
1614, 15syl6eq 2701 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (1 − 𝑠) = 1)
1716oveq1d 6705 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → ((1 − 𝑠) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
18 oveq1 6697 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 · (𝑥𝑖)) = (0 · (𝑥𝑖)))
1917, 18oveq12d 6708 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
2019eqeq2d 2661 . . . . . . . . . . . . . . . . . 18 (𝑠 = 0 → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ (𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2120ralbidv 3015 . . . . . . . . . . . . . . . . 17 (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2221biimpac 502 . . . . . . . . . . . . . . . 16 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
23 eqcom 2658 . . . . . . . . . . . . . . . . 17 (𝑍 = 𝑈𝑈 = 𝑍)
247adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
258adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26 eqeefv 25828 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
2724, 25, 26syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
288ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29 fveecn 25827 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3028, 29sylancom 702 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
31 simpllr 815 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
32 fveecn 25827 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
3331, 32sylancom 702 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
34 mulid2 10076 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
35 mul02 10252 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝑖) ∈ ℂ → (0 · (𝑥𝑖)) = 0)
3634, 35oveqan12d 6709 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = ((𝑍𝑖) + 0))
37 addid1 10254 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
3837adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
3936, 38eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = (𝑍𝑖))
4039eqeq2d 2661 . . . . . . . . . . . . . . . . . . . 20 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4130, 33, 40syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4241ralbidva 3014 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
4327, 42bitr4d 271 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4423, 43syl5bb 272 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4522, 44syl5ibr 236 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
4645expdimp 452 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
4746necon3d 2844 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑍𝑈𝑠 ≠ 0))
4813, 47mpd 15 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑠 ≠ 0)
49 0re 10078 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℝ
50 1re 10077 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ
5149, 50elicc2i 12277 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
5251simp1bi 1096 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
53 rereccl 10781 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5452, 53sylan 487 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5552adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
5651simp2bi 1097 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
5756adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
58 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
5955, 57, 58ne0gt0d 10212 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
60 0le1 10589 . . . . . . . . . . . . . . . . . . 19 0 ≤ 1
61 divge0 10930 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
6250, 60, 61mpanl12 718 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
6355, 59, 62syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
64 elrege0 12316 . . . . . . . . . . . . . . . . 17 ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
6554, 63, 64sylanbrc 699 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6665adantll 750 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6752ad3antlr 767 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
6867recnd 10106 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
69 simplr 807 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
70 simp-4r 824 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
7170, 32sylancom 702 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
728ad3antrrr 766 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
7372, 29sylancom 702 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
74 ax-1cn 10032 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℂ
75 reccl 10730 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
76 subcl 10318 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
7774, 75, 76sylancr 696 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
7877adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
79 subcl 10318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
8074, 79mpan 706 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
8180adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
8275, 81mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
8382adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
84 simprr 811 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
8578, 83, 84adddird 10103 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
86 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
87 subdi 10501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8874, 87mp3an2 1452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8975, 86, 88syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
9089oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
9175mulid1d 10095 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
92 recid2 10738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
9391, 92oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
9493oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
95 addsubass 10329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9674, 95mp3an3 1453 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9777, 75, 96syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9877, 75addcld 10097 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
99 npcan 10328 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
10074, 75, 99sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
10198, 100subeq0bd 10494 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
10294, 97, 1013eqtr2d 2691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
10390, 102eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
104103adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
105104oveq1d 6705 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
10675adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
10780ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
108106, 107, 84mulassd 10101 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
109108oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
11085, 105, 1093eqtr3rd 2694 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = (0 · (𝑍𝑖)))
111 mul02 10252 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍𝑖) ∈ ℂ → (0 · (𝑍𝑖)) = 0)
112111ad2antll 765 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
113110, 112eqtrd 2685 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = 0)
114 simpll 805 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
115 simprl 809 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) ∈ ℂ)
116106, 114, 115mulassd 10101 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))
11792oveq1d 6705 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (1 · (𝑥𝑖)))
118 mulid2 10076 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑖) ∈ ℂ → (1 · (𝑥𝑖)) = (𝑥𝑖))
119118adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (1 · (𝑥𝑖)) = (𝑥𝑖))
120117, 119sylan9eq 2705 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (𝑥𝑖))
121116, 120eqtr3d 2687 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) = (𝑥𝑖))
122113, 121oveq12d 6708 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (0 + (𝑥𝑖)))
12378, 84mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
124 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
125 mulcl 10058 . . . . . . . . . . . . . . . . . . . . . 22 (((1 − 𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
12681, 124, 125syl2an 493 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
127106, 126mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
128 mulcl 10058 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
129128ad2ant2r 798 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
130106, 129mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) ∈ ℂ)
131123, 127, 130addassd 10100 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
132106, 126, 129adddid 10102 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))))
133132oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
134131, 133eqtr4d 2688 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
135 addid2 10257 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑖) ∈ ℂ → (0 + (𝑥𝑖)) = (𝑥𝑖))
136135ad2antrl 764 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 + (𝑥𝑖)) = (𝑥𝑖))
137122, 134, 1363eqtr3rd 2694 . . . . . . . . . . . . . . . . 17 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
13868, 69, 71, 73, 137syl22anc 1367 . . . . . . . . . . . . . . . 16 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
139138ralrimiva 2995 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
140 oveq2 6698 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
141140oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − (1 / 𝑠)) · (𝑍𝑖)))
142 oveq1 6697 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
143141, 142oveq12d 6708 . . . . . . . . . . . . . . . . . 18 (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
144143eqeq2d 2661 . . . . . . . . . . . . . . . . 17 (𝑡 = (1 / 𝑠) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
145144ralbidv 3015 . . . . . . . . . . . . . . . 16 (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
146145rspcev 3340 . . . . . . . . . . . . . . 15 (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
14766, 139, 146syl2anc 694 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
148 oveq2 6698 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (𝑡 · (𝑈𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
149148oveq2d 6706 . . . . . . . . . . . . . . . . . 18 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
150149eqeq2d 2661 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
151150ralimi 2981 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
152 ralbi 3097 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
153151, 152syl 17 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
154153rexbidv 3081 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
155147, 154syl5ibrcom 237 . . . . . . . . . . . . 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 3106 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
15912, 158syldan 486 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
160 3simpa 1078 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
16149, 50elicc2i 12277 . . . . . . . . . . . 12 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
162 elrege0 12316 . . . . . . . . . . . 12 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
163160, 161, 1623imtr4i 281 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
164163ssriv 3640 . . . . . . . . . 10 (0[,]1) ⊆ (0[,)+∞)
165 brbtwn 25824 . . . . . . . . . . . 12 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
1669, 8, 7, 165syl3anc 1366 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
167166biimpa 500 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
168 ssrexv 3700 . . . . . . . . . 10 ((0[,]1) ⊆ (0[,)+∞) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
169164, 167, 168mpsyl 68 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
170159, 169jaodan 843 . . . . . . . 8 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
171170anasss 680 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
1726, 171sylan2b 491 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
173 r19.26 3093 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
174 eqtr2 2671 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
175174ralimi 2981 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
176173, 175sylbir 225 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
177 elrege0 12316 . . . . . . . . . . . . 13 (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
178177simplbi 475 . . . . . . . . . . . 12 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
179178recnd 10106 . . . . . . . . . . 11 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
180 elrege0 12316 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
181180simplbi 475 . . . . . . . . . . . 12 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
182181recnd 10106 . . . . . . . . . . 11 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
183179, 182anim12i 589 . . . . . . . . . 10 ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
184 simplr 807 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
185 simpl2 1085 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑍 ∈ (𝔼‘𝑁))
186185ad2antrr 762 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
187186, 29sylancom 702 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
188 simpl3 1086 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑈 ∈ (𝔼‘𝑁))
189188ad2antrr 762 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
190 fveecn 25827 . . . . . . . . . . . . . 14 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
191189, 190sylancom 702 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
192 subcl 10318 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
19374, 192mpan 706 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
194193adantr 480 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
195 simpl 472 . . . . . . . . . . . . . . . 16 (((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
196 mulcl 10058 . . . . . . . . . . . . . . . 16 (((1 − 𝑡) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
197194, 195, 196syl2an 493 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
198 mulcl 10058 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
199198ad2ant2rl 800 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
20080adantl 481 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
201200, 195, 125syl2an 493 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
202 mulcl 10058 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
203202ad2ant2l 797 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
204197, 199, 201, 203addsubeq4d 10481 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
205 nnncan1 10355 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
20674, 205mp3an1 1451 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
207206ancoms 468 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
208207oveq1d 6705 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
209208adantr 480 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
21080ad2antlr 763 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
211193ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
212 simprl 809 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
213210, 211, 212subdird 10525 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
214209, 213eqtr3d 2687 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
215 simpll 805 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
216 simplr 807 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
217 simprr 811 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
218215, 216, 217subdird 10525 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑈𝑖)) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖))))
219214, 218eqeq12d 2666 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
220 subcl 10318 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡𝑠) ∈ ℂ)
221220adantr 480 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡𝑠) ∈ ℂ)
222 mulcan1g 10718 . . . . . . . . . . . . . . 15 (((𝑡𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
223221, 212, 217, 222syl3anc 1366 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
224204, 219, 2233bitr2d 296 . . . . . . . . . . . . 13 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
225184, 187, 191, 224syl12anc 1364 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
226225ralbidva 3014 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
227 r19.32v 3112 . . . . . . . . . . . 12 (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
228 simplr 807 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍𝑈)
229228neneqd 2828 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
230 simpll2 1121 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
231 simpll3 1122 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
232 eqeefv 25828 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
233230, 231, 232syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
234229, 233mtbid 313 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖))
235 orel2 397 . . . . . . . . . . . . . 14 (¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
236234, 235syl 17 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
237 subeq0 10345 . . . . . . . . . . . . . 14 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
238237adantl 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
239236, 238sylibd 229 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
240227, 239syl5bi 232 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
241226, 240sylbid 230 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
242183, 241sylan2 490 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
243176, 242syl5 34 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
244243ralrimivva 3000 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
245244adantr 480 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
246 oveq2 6698 . . . . . . . . . . 11 (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
247246oveq1d 6705 . . . . . . . . . 10 (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − 𝑠) · (𝑍𝑖)))
248 oveq1 6697 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑡 · (𝑈𝑖)) = (𝑠 · (𝑈𝑖)))
249247, 248oveq12d 6708 . . . . . . . . 9 (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
250249eqeq2d 2661 . . . . . . . 8 (𝑡 = 𝑠 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
251250ralbidv 3015 . . . . . . 7 (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
252251reu4 3433 . . . . . 6 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠)))
253172, 245, 252sylanbrc 699 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
254 df-reu 2948 . . . . 5 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
255253, 254sylib 208 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
256255ralrimiva 2995 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
257 axcontlem2.2 . . . 4 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
258257fnopabg 6055 . . 3 (∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn 𝐷)
259256, 258sylib 208 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn 𝐷)
260178ad2antlr 763 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
261185ad2antrr 762 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
262 fveere 25826 . . . . . . . . . . 11 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
263261, 262sylancom 702 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
264188ad2antrr 762 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
265 fveere 25826 . . . . . . . . . . 11 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
266264, 265sylancom 702 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
267 resubcl 10383 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
26850, 267mpan 706 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
269 remulcl 10059 . . . . . . . . . . . . 13 (((1 − 𝑡) ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
270268, 269sylan 487 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
2712703adant3 1101 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
272 remulcl 10059 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
2732723adant2 1100 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
274271, 273readdcld 10107 . . . . . . . . . 10 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
275260, 263, 266, 274syl3anc 1366 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
276275ralrimiva 2995 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
277 simpll1 1120 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
278 mptelee 25820 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
279277, 278syl 17 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
280276, 279mpbird 247 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
281 letric 10175 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡𝑡 ≤ 1))
28250, 178, 281sylancr 696 . . . . . . . . 9 (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡𝑡 ≤ 1))
283282adantl 481 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑡 ≤ 1))
284 simpr 476 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
285178adantr 480 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
286 0red 10079 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
287 1red 10093 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
288 0lt1 10588 . . . . . . . . . . . . . . . . 17 0 < 1
289288a1i 11 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
290286, 287, 285, 289, 284ltletrd 10235 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
291 divelunit 12352 . . . . . . . . . . . . . . . 16 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
29250, 60, 291mpanl12 718 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
293285, 290, 292syl2anc 694 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
294284, 293mpbird 247 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
295294adantll 750 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
296178ad3antlr 767 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
297296recnd 10106 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
298290gt0ne0d 10630 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
299298adantll 750 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
300299adantr 480 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
301185ad3antrrr 766 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
302301, 29sylancom 702 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
303188ad3antrrr 766 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
304303, 190sylancom 702 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
305 reccl 10730 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
306305adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
307193adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
308307, 195, 196syl2an 493 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
309198ad2ant2rl 800 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
310306, 308, 309adddid 10102 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))))
311310oveq2d 6706 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
312 subcl 10318 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
31374, 305, 312sylancr 696 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
314 mulcl 10058 . . . . . . . . . . . . . . . . 17 (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
315313, 195, 314syl2an 493 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
316306, 308mulcld 10098 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
317 recid2 10738 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
318317oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
319318adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
320 simpll 805 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
321 simprr 811 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
322306, 320, 321mulassd 10101 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))
323 mulid2 10076 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) ∈ ℂ → (1 · (𝑈𝑖)) = (𝑈𝑖))
324323ad2antll 765 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (𝑈𝑖)) = (𝑈𝑖))
325319, 322, 3243eqtr3d 2693 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) = (𝑈𝑖))
326325, 321eqeltrd 2730 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) ∈ ℂ)
327315, 316, 326addassd 10100 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
328313adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
329305, 307mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
330329adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
331 simprl 809 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
332328, 330, 331adddird 10103 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
333 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
334 subdi 10501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
33574, 334mp3an2 1452 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
336305, 333, 335syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
337305mulid1d 10095 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
338337, 317oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
339336, 338eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
340339oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
341 npncan2 10346 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
34274, 305, 341sylancr 696 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
343340, 342eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
344343adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
345344oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
346111ad2antrl 764 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
347345, 346eqtrd 2685 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = 0)
348193ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
349306, 348, 331mulassd 10101 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
350349oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
351332, 347, 3503eqtr3rd 2694 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = 0)
352351, 325oveq12d 6708 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (0 + (𝑈𝑖)))
353 addid2 10257 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) ∈ ℂ → (0 + (𝑈𝑖)) = (𝑈𝑖))
354353ad2antll 765 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 + (𝑈𝑖)) = (𝑈𝑖))
355352, 354eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (𝑈𝑖))
356311, 327, 3553eqtr2rd 2692 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
357297, 300, 302, 304, 356syl22anc 1367 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
358357ralrimiva 2995 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
359 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
360359oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − (1 / 𝑡)) · (𝑍𝑖)))
361 oveq1 6697 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))
362360, 361oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
363362eqeq2d 2661 . . . . . . . . . . . . . . 15 (𝑠 = (1 / 𝑡) → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
364363ralbidv 3015 . . . . . . . . . . . . . 14 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
365 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑍𝑘) = (𝑍𝑖))
366365oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍𝑘)) = ((1 − 𝑡) · (𝑍𝑖)))
367 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑈𝑘) = (𝑈𝑖))
368367oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (𝑡 · (𝑈𝑘)) = (𝑡 · (𝑈𝑖)))
369366, 368oveq12d 6708 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
370 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))
371 ovex 6718 . . . . . . . . . . . . . . . . . . 19 (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∈ V
372369, 370, 371fvmpt 6321 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
373372oveq2d 6706 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
374373oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
375374eqeq2d 2661 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑁) → ((𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
376375ralbiia 3008 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
377364, 376syl6bb 276 . . . . . . . . . . . . 13 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
378377rspcev 3340 . . . . . . . . . . . 12 (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
379295, 358, 378syl2anc 694 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
380188ad2antrr 762 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 ∈ (𝔼‘𝑁))
381185ad2antrr 762 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑍 ∈ (𝔼‘𝑁))
382280adantr 480 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
383 brbtwn 25824 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
384380, 381, 382, 383syl3anc 1366 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
385379, 384mpbird 247 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
386385ex 449 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
387 simpll 805 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
388 simplr 807 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
389 simpr 476 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
390387, 388, 3893jca 1261 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
391177anbi1i 731 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
39249, 50elicc2i 12277 . . . . . . . . . . . . . 14 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
393390, 391, 3923imtr4i 281 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
394393adantll 750 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
395372rgen 2951 . . . . . . . . . . . 12 𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))
396 oveq2 6698 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
397396oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
398 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → (𝑠 · (𝑈𝑖)) = (𝑡 · (𝑈𝑖)))
399397, 398oveq12d 6708 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
400399eqeq2d 2661 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
401400ralbidv 3015 . . . . . . . . . . . . 13 (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
402401rspcev 3340 . . . . . . . . . . . 12 ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
403394, 395, 402sylancl 695 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
404280adantr 480 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
405185ad2antrr 762 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
406188ad2antrr 762 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
407 brbtwn 25824 . . . . . . . . . . . 12 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
408404, 405, 406, 407syl3anc 1366 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
409403, 408mpbird 247 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
410409ex 449 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
411386, 410orim12d 901 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((1 ≤ 𝑡𝑡 ≤ 1) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
412283, 411mpd 15 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
413 opeq2 4434 . . . . . . . . . 10 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
414413breq2d 4697 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
415 breq1 4688 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
416414, 415orbi12d 746 . . . . . . . 8 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
417416, 5elrab2 3399 . . . . . . 7 ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
418280, 412, 417sylanbrc 699 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷)
419 fveq1 6228 . . . . . . . . 9 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑥𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))
420419eqeq1d 2653 . . . . . . . 8 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
421420ralbidv 3015 . . . . . . 7 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
422421rspcev 3340 . . . . . 6 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
423418, 395, 422sylancl 695 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
4246simplbi 475 . . . . . . . . 9 (𝑥𝐷𝑥 ∈ (𝔼‘𝑁))
425 ssrab2 3720 . . . . . . . . . . 11 {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ⊆ (𝔼‘𝑁)
4265, 425eqsstri 3668 . . . . . . . . . 10 𝐷 ⊆ (𝔼‘𝑁)
427426sseli 3632 . . . . . . . . 9 (𝑦𝐷𝑦 ∈ (𝔼‘𝑁))
428424, 427anim12i 589 . . . . . . . 8 ((𝑥𝐷𝑦𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
429 r19.26 3093 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
430 eqtr3 2672 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → (𝑥𝑖) = (𝑦𝑖))
431430ralimi 2981 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
432429, 431sylbir 225 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
433 eqeefv 25828 . . . . . . . . . 10 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
434433adantl 481 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
435432, 434syl5ibr 236 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
436428, 435sylan2 490 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥𝐷𝑦𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
437436ralrimivva 3000 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
438437adantr 480 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
439 df-reu 2948 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
440 fveq1 6228 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
441440eqeq1d 2653 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
442441ralbidv 3015 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
443442reu4 3433 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
444439, 443bitr3i 266 . . . . 5 (∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
445423, 438, 444sylanbrc 699 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
446445ralrimiva 2995 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
447 an12 855 . . . . . . . 8 ((𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
448447opabbii 4750 . . . . . . 7 {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
449257, 448eqtri 2673 . . . . . 6 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
450449cnveqi 5329 . . . . 5 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
451 cnvopab 5568 . . . . 5 {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
452450, 451eqtri 2673 . . . 4 𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
453452fnopabg 6055 . . 3 (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn (0[,)+∞))
454446, 453sylib 208 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn (0[,)+∞))
455 dff1o4 6183 . 2 (𝐹:𝐷1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷𝐹 Fn (0[,)+∞)))
456259, 454, 455sylanbrc 699 1 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹:𝐷1-1-onto→(0[,)+∞))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∃!weu 2498   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  ∃!wreu 2943  {crab 2945   ⊆ wss 3607  ⟨cop 4216   class class class wbr 4685  {copab 4745   ↦ cmpt 4762  ◡ccnv 5142   Fn wfn 5921  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  [,)cico 12215  [,]cicc 12216  ...cfz 12364  𝔼cee 25813   Btwn cbtwn 25814 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-z 11416  df-uz 11726  df-ico 12219  df-icc 12220  df-fz 12365  df-ee 25816  df-btwn 25817 This theorem is referenced by:  axcontlem5  25893  axcontlem9  25897  axcontlem10  25898
 Copyright terms: Public domain W3C validator