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

Theorem axcontlem2 26873
 Description: Lemma for axcont 26884. The idea here is to set up a mapping 𝐹 that will allow us to transfer dedekind 10855 to two sets of points. Here, we set up 𝐹 and show its domain and range. (Contributed by Scott Fenton, 17-Jun-2013.)
Hypotheses
Ref Expression
axcontlem2.1 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
axcontlem2.2 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
Assertion
Ref Expression
axcontlem2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹:𝐷1-1-onto→(0[,)+∞))
Distinct variable groups:   𝑍,𝑝,𝑥,𝑡,𝑖   𝑈,𝑝,𝑥,𝑡,𝑖   𝑁,𝑝,𝑥,𝑡,𝑖   𝑥,𝐷,𝑡
Allowed substitution hints:   𝐷(𝑖,𝑝)   𝐹(𝑥,𝑡,𝑖,𝑝)

Proof of Theorem axcontlem2
Dummy variables 𝑘 𝑦 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq2 4767 . . . . . . . . . 10 (𝑝 = 𝑥 → ⟨𝑍, 𝑝⟩ = ⟨𝑍, 𝑥⟩)
21breq2d 5049 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑥⟩))
3 breq1 5040 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑈⟩))
42, 3orbi12d 916 . . . . . . . 8 (𝑝 = 𝑥 → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
5 axcontlem2.1 . . . . . . . 8 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
64, 5elrab2 3608 . . . . . . 7 (𝑥𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)))
7 simpll3 1212 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
8 simpll2 1211 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
9 simpr 488 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
10 brbtwn 26807 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
117, 8, 9, 10syl3anc 1369 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑥⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
1211biimpa 480 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))
13 simp-4r 783 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑍𝑈)
14 oveq2 7165 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 0 → (1 − 𝑠) = (1 − 0))
15 1m0e1 11809 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 0) = 1
1614, 15eqtrdi 2810 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (1 − 𝑠) = 1)
1716oveq1d 7172 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → ((1 − 𝑠) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
18 oveq1 7164 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 · (𝑥𝑖)) = (0 · (𝑥𝑖)))
1917, 18oveq12d 7175 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
2019eqeq2d 2770 . . . . . . . . . . . . . . . . . 18 (𝑠 = 0 → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ (𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2120ralbidv 3127 . . . . . . . . . . . . . . . . 17 (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
2221biimpac 482 . . . . . . . . . . . . . . . 16 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))))
23 eqcom 2766 . . . . . . . . . . . . . . . . 17 (𝑍 = 𝑈𝑈 = 𝑍)
247adantr 484 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁))
258adantr 484 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁))
26 eqeefv 26811 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
2724, 25, 26syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
288ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
29 fveecn 26810 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3028, 29sylancom 591 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
31 fveecn 26810 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
3231ad4ant24 753 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
33 mulid2 10692 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
34 mul02 10870 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝑖) ∈ ℂ → (0 · (𝑥𝑖)) = 0)
3533, 34oveqan12d 7176 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = ((𝑍𝑖) + 0))
36 addid1 10872 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
3736adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
3835, 37eqtrd 2794 . . . . . . . . . . . . . . . . . . . . 21 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) = (𝑍𝑖))
3938eqeq2d 2770 . . . . . . . . . . . . . . . . . . . 20 (((𝑍𝑖) ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4030, 32, 39syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ (𝑈𝑖) = (𝑍𝑖)))
4140ralbidva 3126 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (𝑍𝑖)))
4227, 41bitr4d 285 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4323, 42syl5bb 286 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = ((1 · (𝑍𝑖)) + (0 · (𝑥𝑖)))))
4422, 43syl5ibr 249 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈))
4544expdimp 456 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈))
4645necon3d 2973 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑍𝑈𝑠 ≠ 0))
4713, 46mpd 15 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → 𝑠 ≠ 0)
48 elicc01 12912 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
4948simp1bi 1143 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
50 rereccl 11410 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5149, 50sylan 583 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℝ)
5249adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℝ)
5348simp2bi 1144 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
5453adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠)
55 simpr 488 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0)
5652, 54, 55ne0gt0d 10829 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠)
57 1re 10693 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
58 0le1 11215 . . . . . . . . . . . . . . . . . . 19 0 ≤ 1
59 divge0 11561 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠))
6057, 58, 59mpanl12 701 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ℝ ∧ 0 < 𝑠) → 0 ≤ (1 / 𝑠))
6152, 56, 60syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 / 𝑠))
62 elrege0 12900 . . . . . . . . . . . . . . . . 17 ((1 / 𝑠) ∈ (0[,)+∞) ↔ ((1 / 𝑠) ∈ ℝ ∧ 0 ≤ (1 / 𝑠)))
6351, 61, 62sylanbrc 586 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6463adantll 713 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞))
6549ad3antlr 730 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
6665recnd 10721 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
67 simplr 768 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
6831ad5ant25 761 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) ∈ ℂ)
698ad3antrrr 729 . . . . . . . . . . . . . . . . . 18 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
7069, 29sylancom 591 . . . . . . . . . . . . . . . . 17 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
71 ax-1cn 10647 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℂ
72 reccl 11357 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ ℂ)
73 subcl 10937 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 / 𝑠)) ∈ ℂ)
7471, 72, 73sylancr 590 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 / 𝑠)) ∈ ℂ)
7574adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − (1 / 𝑠)) ∈ ℂ)
76 subcl 10937 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
7771, 76mpan 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ → (1 − 𝑠) ∈ ℂ)
7877adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈ ℂ)
7972, 78mulcld 10713 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
8079adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
81 simprr 772 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
8275, 80, 81adddird 10718 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
83 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
84 subdi 11125 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8571, 84mp3an2 1447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8672, 83, 85syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))
8786oveq2d 7173 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))))
8872mulid1d 10710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠))
89 recid2 11365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1)
9088, 89oveq12d 7175 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)) = ((1 / 𝑠) − 1))
9190oveq2d 7173 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
92 addsubass 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9371, 92mp3an3 1448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 − (1 / 𝑠)) ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9474, 72, 93syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1)))
9574, 72addcld 10712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) ∈ ℂ)
96 npcan 10947 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 ∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
9771, 72, 96sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (1 / 𝑠)) = 1)
9895, 97subeq0bd 11118 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = 0)
9991, 94, 983eqtr2d 2800 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) = 0)
10087, 99eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
101100adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0)
102101oveq1d 7172 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
10372adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 / 𝑠) ∈ ℂ)
10477ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
105103, 104, 81mulassd 10716 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
106105oveq2d 7173 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
10782, 102, 1063eqtr3rd 2803 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = (0 · (𝑍𝑖)))
108 mul02 10870 . . . . . . . . . . . . . . . . . . . . 21 ((𝑍𝑖) ∈ ℂ → (0 · (𝑍𝑖)) = 0)
109108ad2antll 728 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
110107, 109eqtrd 2794 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = 0)
111 simpll 766 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
112 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) ∈ ℂ)
113103, 111, 112mulassd 10716 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))
11489oveq1d 7172 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (1 · (𝑥𝑖)))
115 mulid2 10692 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑖) ∈ ℂ → (1 · (𝑥𝑖)) = (𝑥𝑖))
116115adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (1 · (𝑥𝑖)) = (𝑥𝑖))
117114, 116sylan9eq 2814 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥𝑖)) = (𝑥𝑖))
118113, 117eqtr3d 2796 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) = (𝑥𝑖))
119110, 118oveq12d 7175 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (0 + (𝑥𝑖)))
12075, 81mulcld 10713 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − (1 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
121 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
122 mulcl 10673 . . . . . . . . . . . . . . . . . . . . . 22 (((1 − 𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
12378, 121, 122syl2an 598 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
124103, 123mulcld 10713 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
125 mulcl 10673 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ℂ ∧ (𝑥𝑖) ∈ ℂ) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
126125ad2ant2r 746 . . . . . . . . . . . . . . . . . . . . 21 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑠 · (𝑥𝑖)) ∈ ℂ)
127103, 126mulcld 10713 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥𝑖))) ∈ ℂ)
128120, 124, 127addassd 10715 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
129103, 123, 126adddid 10717 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))))
130129oveq2d 7173 . . . . . . . . . . . . . . . . . . 19 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖))))))
131128, 130eqtr4d 2797 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
132 addid2 10875 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑖) ∈ ℂ → (0 + (𝑥𝑖)) = (𝑥𝑖))
133132ad2antrl 727 . . . . . . . . . . . . . . . . . 18 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (0 + (𝑥𝑖)) = (𝑥𝑖))
134119, 131, 1333eqtr3rd 2803 . . . . . . . . . . . . . . . . 17 (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥𝑖) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
13566, 67, 68, 70, 134syl22anc 837 . . . . . . . . . . . . . . . 16 (((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
136135ralrimiva 3114 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
137 oveq2 7165 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠)))
138137oveq1d 7172 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − (1 / 𝑠)) · (𝑍𝑖)))
139 oveq1 7164 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
140138, 139oveq12d 7175 . . . . . . . . . . . . . . . . . 18 (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
141140eqeq2d 2770 . . . . . . . . . . . . . . . . 17 (𝑡 = (1 / 𝑠) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ (𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
142141ralbidv 3127 . . . . . . . . . . . . . . . 16 (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
143142rspcev 3544 . . . . . . . . . . . . . . 15 (((1 / 𝑠) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − (1 / 𝑠)) · (𝑍𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
14464, 136, 143syl2anc 587 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
145 oveq2 7165 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (𝑡 · (𝑈𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))
146145oveq2d 7173 . . . . . . . . . . . . . . . . . 18 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))))))
147146eqeq2d 2770 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
148147ralimi 3093 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
149 ralbi 3100 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
150148, 149syl 17 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
151150rexbidv 3222 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))))))
152144, 151syl5ibrcom 250 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
153152impancom 455 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → (𝑠 ≠ 0 → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
15447, 153mpd 15 . . . . . . . . . . 11 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
155154r19.29an 3213 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑥𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
15612, 155syldan 594 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn ⟨𝑍, 𝑥⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
157 3simpa 1146 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
158 elicc01 12912 . . . . . . . . . . . 12 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥𝑥 ≤ 1))
159 elrege0 12900 . . . . . . . . . . . 12 (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
160157, 158, 1593imtr4i 295 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) → 𝑥 ∈ (0[,)+∞))
161160ssriv 3899 . . . . . . . . . 10 (0[,]1) ⊆ (0[,)+∞)
162 brbtwn 26807 . . . . . . . . . . . 12 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
1639, 8, 7, 162syl3anc 1369 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
164163biimpa 480 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
165 ssrexv 3962 . . . . . . . . . 10 ((0[,]1) ⊆ (0[,)+∞) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
166161, 164, 165mpsyl 68 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn ⟨𝑍, 𝑈⟩) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
167156, 166jaodan 955 . . . . . . . 8 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
168167anasss 470 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, 𝑥⟩ ∨ 𝑥 Btwn ⟨𝑍, 𝑈⟩))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
1696, 168sylan2b 596 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
170 r19.26 3102 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
171 eqtr2 2780 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
172171ralimi 3093 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
173170, 172sylbir 238 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
174 elrege0 12900 . . . . . . . . . . . . 13 (𝑡 ∈ (0[,)+∞) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡))
175174simplbi 501 . . . . . . . . . . . 12 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℝ)
176175recnd 10721 . . . . . . . . . . 11 (𝑡 ∈ (0[,)+∞) → 𝑡 ∈ ℂ)
177 elrege0 12900 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,)+∞) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠))
178177simplbi 501 . . . . . . . . . . . 12 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℝ)
179178recnd 10721 . . . . . . . . . . 11 (𝑠 ∈ (0[,)+∞) → 𝑠 ∈ ℂ)
180176, 179anim12i 615 . . . . . . . . . 10 ((𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
181 simplr 768 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ))
182 simpl2 1190 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑍 ∈ (𝔼‘𝑁))
183182ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
184183, 29sylancom 591 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
185 simpl3 1191 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑈 ∈ (𝔼‘𝑁))
186185ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
187 fveecn 26810 . . . . . . . . . . . . . 14 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
188186, 187sylancom 591 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
189 subcl 10937 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
19071, 189mpan 689 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
191190adantr 484 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
192 simpl 486 . . . . . . . . . . . . . . . 16 (((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑍𝑖) ∈ ℂ)
193 mulcl 10673 . . . . . . . . . . . . . . . 16 (((1 − 𝑡) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
194191, 192, 193syl2an 598 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
195 mulcl 10673 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
196195ad2ant2rl 748 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
19777adantl 485 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
198197, 192, 122syl2an 598 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
199 mulcl 10673 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
200199ad2ant2l 745 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑠 · (𝑈𝑖)) ∈ ℂ)
201194, 196, 198, 200addsubeq4d 11100 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
202 nnncan1 10974 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
20371, 202mp3an1 1446 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
204203ancoms 462 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡𝑠))
205204oveq1d 7172 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
206205adantr 484 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑍𝑖)))
20777ad2antlr 726 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑠) ∈ ℂ)
208190ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
209 simprl 770 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
210207, 208, 209subdird 11149 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
211206, 210eqtr3d 2796 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑍𝑖)) = (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))))
212 simpll 766 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
213 simplr 768 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ)
214 simprr 772 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
215212, 213, 214subdird 11149 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝑡𝑠) · (𝑈𝑖)) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖))))
216211, 215eqeq12d 2775 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ (((1 − 𝑠) · (𝑍𝑖)) − ((1 − 𝑡) · (𝑍𝑖))) = ((𝑡 · (𝑈𝑖)) − (𝑠 · (𝑈𝑖)))))
217 subcl 10937 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡𝑠) ∈ ℂ)
218217adantr 484 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡𝑠) ∈ ℂ)
219 mulcan1g 11345 . . . . . . . . . . . . . . 15 (((𝑡𝑠) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
220218, 209, 214, 219syl3anc 1369 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝑡𝑠) · (𝑍𝑖)) = ((𝑡𝑠) · (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
221201, 216, 2203bitr2d 310 . . . . . . . . . . . . 13 (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
222181, 184, 188, 221syl12anc 835 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
223222ralbidva 3126 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
224 r19.32v 3260 . . . . . . . . . . . 12 (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) ↔ ((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
225 simplr 768 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍𝑈)
226225neneqd 2957 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈)
227 simpll2 1211 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁))
228 simpll3 1212 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁))
229 eqeefv 26811 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
230227, 228, 229syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
231226, 230mtbid 327 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖))
232 orel2 888 . . . . . . . . . . . . . 14 (¬ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
233231, 232syl 17 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → (𝑡𝑠) = 0))
234 subeq0 10964 . . . . . . . . . . . . . 14 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
235234adantl 485 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡𝑠) = 0 ↔ 𝑡 = 𝑠))
236233, 235sylibd 242 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
237224, 236syl5bi 245 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡𝑠) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) → 𝑡 = 𝑠))
238223, 237sylbid 243 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
239180, 238sylan2 595 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) → 𝑡 = 𝑠))
240173, 239syl5 34 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
241240ralrimivva 3121 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
242241adantr 484 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠))
243 oveq2 7165 . . . . . . . . . . 11 (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠))
244243oveq1d 7172 . . . . . . . . . 10 (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍𝑖)) = ((1 − 𝑠) · (𝑍𝑖)))
245 oveq1 7164 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑡 · (𝑈𝑖)) = (𝑠 · (𝑈𝑖)))
246244, 245oveq12d 7175 . . . . . . . . 9 (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
247246eqeq2d 2770 . . . . . . . 8 (𝑡 = 𝑠 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
248247ralbidv 3127 . . . . . . 7 (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
249248reu4 3648 . . . . . 6 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈ (0[,)+∞)((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))) → 𝑡 = 𝑠)))
250169, 242, 249sylanbrc 586 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
251 df-reu 3078 . . . . 5 (∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
252250, 251sylib 221 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑥𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
253252ralrimiva 3114 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
254 axcontlem2.2 . . . 4 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
255254fnopabg 6474 . . 3 (∀𝑥𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn 𝐷)
256253, 255sylib 221 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn 𝐷)
257175ad2antlr 726 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
258182ad2antrr 725 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
259 fveere 26809 . . . . . . . . . . 11 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
260258, 259sylancom 591 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍𝑘) ∈ ℝ)
261185ad2antrr 725 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
262 fveere 26809 . . . . . . . . . . 11 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
263261, 262sylancom 591 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈𝑘) ∈ ℝ)
264 resubcl 11002 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
26557, 264mpan 689 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (1 − 𝑡) ∈ ℝ)
266 remulcl 10674 . . . . . . . . . . . . 13 (((1 − 𝑡) ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
267265, 266sylan 583 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
2682673adant3 1130 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍𝑘)) ∈ ℝ)
269 remulcl 10674 . . . . . . . . . . . 12 ((𝑡 ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
2702693adant2 1129 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (𝑡 · (𝑈𝑘)) ∈ ℝ)
271268, 270readdcld 10722 . . . . . . . . . 10 ((𝑡 ∈ ℝ ∧ (𝑍𝑘) ∈ ℝ ∧ (𝑈𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
272257, 260, 263, 271syl3anc 1369 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
273272ralrimiva 3114 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ)
274 simpll1 1210 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈ ℕ)
275 mptelee 26803 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
276274, 275syl 17 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) ∈ ℝ))
277273, 276mpbird 260 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
278 letric 10792 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 ≤ 𝑡𝑡 ≤ 1))
27957, 175, 278sylancr 590 . . . . . . . . 9 (𝑡 ∈ (0[,)+∞) → (1 ≤ 𝑡𝑡 ≤ 1))
280279adantl 485 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑡 ≤ 1))
281 simpr 488 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ≤ 𝑡)
282175adantr 484 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ∈ ℝ)
283 0red 10696 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 ∈ ℝ)
284 1red 10694 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 1 ∈ ℝ)
285 0lt1 11214 . . . . . . . . . . . . . . . . 17 0 < 1
286285a1i 11 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 1)
287283, 284, 282, 286, 281ltletrd 10852 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 0 < 𝑡)
288 divelunit 12940 . . . . . . . . . . . . . . . 16 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
28957, 58, 288mpanl12 701 . . . . . . . . . . . . . . 15 ((𝑡 ∈ ℝ ∧ 0 < 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
290282, 287, 289syl2anc 587 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤ 𝑡))
291281, 290mpbird 260 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
292291adantll 713 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1))
293175ad3antlr 730 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
294293recnd 10721 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
295287gt0ne0d 11256 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (0[,)+∞) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
296295adantll 713 . . . . . . . . . . . . . . 15 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0)
297296adantr 484 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
298182ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
299298, 29sylancom 591 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
300185ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
301300, 187sylancom 591 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
302 reccl 11357 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈ ℂ)
303302adantr 484 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 / 𝑡) ∈ ℂ)
304190adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈ ℂ)
305304, 192, 193syl2an 598 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
306195ad2ant2rl 748 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑡 · (𝑈𝑖)) ∈ ℂ)
307303, 305, 306adddid 10717 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))))
308307oveq2d 7173 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
309 subcl 10937 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 / 𝑡)) ∈ ℂ)
31071, 302, 309sylancr 590 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 / 𝑡)) ∈ ℂ)
311 mulcl 10673 . . . . . . . . . . . . . . . . 17 (((1 − (1 / 𝑡)) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
312310, 192, 311syl2an 598 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
313303, 305mulcld 10713 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
314 recid2 11365 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1)
315314oveq1d 7172 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
316315adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = (1 · (𝑈𝑖)))
317 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ)
318 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
319303, 317, 318mulassd 10716 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))
320 mulid2 10692 . . . . . . . . . . . . . . . . . . 19 ((𝑈𝑖) ∈ ℂ → (1 · (𝑈𝑖)) = (𝑈𝑖))
321320ad2antll 728 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (𝑈𝑖)) = (𝑈𝑖))
322316, 319, 3213eqtr3d 2802 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) = (𝑈𝑖))
323322, 318eqeltrd 2853 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈𝑖))) ∈ ℂ)
324312, 313, 323addassd 10715 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖))))))
325310adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (1 / 𝑡)) ∈ ℂ)
326302, 304mulcld 10713 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
327326adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
328 simprl 770 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
329325, 327, 328adddird 10718 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
330 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
331 subdi 11125 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
33271, 331mp3an2 1447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
333302, 330, 332syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)))
334302mulid1d 10710 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡))
335334, 314oveq12d 7175 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡)) = ((1 / 𝑡) − 1))
336333, 335eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1))
337336oveq2d 7173 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)))
338 npncan2 10965 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
33971, 302, 338sylancr 590 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1)) = 0)
340337, 339eqtrd 2794 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
341340adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0)
342341oveq1d 7172 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (0 · (𝑍𝑖)))
343108ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (𝑍𝑖)) = 0)
344342, 343eqtrd 2794 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = 0)
345190ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
346303, 345, 328mulassd 10716 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
347346oveq2d 7173 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
348329, 344, 3473eqtr3rd 2803 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = 0)
349348, 322oveq12d 7175 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (0 + (𝑈𝑖)))
350 addid2 10875 . . . . . . . . . . . . . . . . 17 ((𝑈𝑖) ∈ ℂ → (0 + (𝑈𝑖)) = (𝑈𝑖))
351350ad2antll 728 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 + (𝑈𝑖)) = (𝑈𝑖))
352349, 351eqtrd 2794 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈𝑖)))) = (𝑈𝑖))
353308, 324, 3523eqtr2rd 2801 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
354294, 297, 299, 301, 353syl22anc 837 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
355354ralrimiva 3114 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
356 oveq2 7165 . . . . . . . . . . . . . . . . . 18 (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡)))
357356oveq1d 7172 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − (1 / 𝑡)) · (𝑍𝑖)))
358 oveq1 7164 . . . . . . . . . . . . . . . . 17 (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))
359357, 358oveq12d 7175 . . . . . . . . . . . . . . . 16 (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
360359eqeq2d 2770 . . . . . . . . . . . . . . 15 (𝑠 = (1 / 𝑡) → ((𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
361360ralbidv 3127 . . . . . . . . . . . . . 14 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
362 fveq2 6664 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑍𝑘) = (𝑍𝑖))
363362oveq2d 7173 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍𝑘)) = ((1 − 𝑡) · (𝑍𝑖)))
364 fveq2 6664 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝑈𝑘) = (𝑈𝑖))
365364oveq2d 7173 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (𝑡 · (𝑈𝑘)) = (𝑡 · (𝑈𝑖)))
366363, 365oveq12d 7175 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
367 eqid 2759 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))
368 ovex 7190 . . . . . . . . . . . . . . . . . . 19 (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∈ V
369366, 367, 368fvmpt 6765 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
370369oveq2d 7173 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
371370oveq2d 7173 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
372371eqeq2d 2770 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑁) → ((𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ (𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
373372ralbiia 3097 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
374361, 373bitrdi 290 . . . . . . . . . . . . 13 (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))))
375374rspcev 3544 . . . . . . . . . . . 12 (((1 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − (1 / 𝑡)) · (𝑍𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
376292, 355, 375syl2anc 587 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))))
377185ad2antrr 725 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 ∈ (𝔼‘𝑁))
378182ad2antrr 725 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑍 ∈ (𝔼‘𝑁))
379277adantr 484 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
380 brbtwn 26807 . . . . . . . . . . . 12 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
381377, 378, 379, 380syl3anc 1369 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖)))))
382376, 381mpbird 260 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
383382ex 416 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
384 simpll 766 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ)
385 simplr 768 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡)
386 simpr 488 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1)
387384, 385, 3863jca 1126 . . . . . . . . . . . . . 14 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
388174anbi1i 626 . . . . . . . . . . . . . 14 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ 𝑡 ≤ 1))
389 elicc01 12912 . . . . . . . . . . . . . 14 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
390387, 388, 3893imtr4i 295 . . . . . . . . . . . . 13 ((𝑡 ∈ (0[,)+∞) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
391390adantll 713 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈ (0[,]1))
392369rgen 3081 . . . . . . . . . . . 12 𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))
393 oveq2 7165 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡))
394393oveq1d 7172 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
395 oveq1 7164 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑡 → (𝑠 · (𝑈𝑖)) = (𝑡 · (𝑈𝑖)))
396394, 395oveq12d 7175 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
397396eqeq2d 2770 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
398397ralbidv 3127 . . . . . . . . . . . . 13 (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
399398rspcev 3544 . . . . . . . . . . . 12 ((𝑡 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
400391, 392, 399sylancl 589 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖))))
401277adantr 484 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁))
402182ad2antrr 725 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁))
403185ad2antrr 725 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁))
404 brbtwn 26807 . . . . . . . . . . . 12 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
405401, 402, 403, 404syl3anc 1369 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑈𝑖)))))
406400, 405mpbird 260 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)
407406ex 416 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
408383, 407orim12d 962 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((1 ≤ 𝑡𝑡 ≤ 1) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
409280, 408mpd 15 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
410 opeq2 4767 . . . . . . . . . 10 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ⟨𝑍, 𝑝⟩ = ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩)
411410breq2d 5049 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ 𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩))
412 breq1 5040 . . . . . . . . 9 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩))
413411, 412orbi12d 916 . . . . . . . 8 (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
414413, 5elrab2 3608 . . . . . . 7 ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn ⟨𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))⟩ ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) Btwn ⟨𝑍, 𝑈⟩)))
415277, 409, 414sylanbrc 586 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷)
416 fveq1 6663 . . . . . . . . 9 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (𝑥𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖))
417416eqeq1d 2761 . . . . . . . 8 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
418417ralbidv 3127 . . . . . . 7 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
419418rspcev 3544 . . . . . 6 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍𝑘)) + (𝑡 · (𝑈𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
420415, 392, 419sylancl 589 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))
4216simplbi 501 . . . . . . . . 9 (𝑥𝐷𝑥 ∈ (𝔼‘𝑁))
4225ssrab3 3989 . . . . . . . . . 10 𝐷 ⊆ (𝔼‘𝑁)
423422sseli 3891 . . . . . . . . 9 (𝑦𝐷𝑦 ∈ (𝔼‘𝑁))
424421, 423anim12i 615 . . . . . . . 8 ((𝑥𝐷𝑦𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))
425 r19.26 3102 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
426 eqtr3 2781 . . . . . . . . . . 11 (((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → (𝑥𝑖) = (𝑦𝑖))
427426ralimi 3093 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
428425, 427sylbir 238 . . . . . . . . 9 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖))
429 eqeefv 26811 . . . . . . . . . 10 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
430429adantl 485 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (𝑦𝑖)))
431428, 430syl5ibr 249 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
432424, 431sylan2 595 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑥𝐷𝑦𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
433432ralrimivva 3121 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
434433adantr 484 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦))
435 df-reu 3078 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
436 fveq1 6663 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
437436eqeq1d 2761 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
438437ralbidv 3127 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
439438reu4 3648 . . . . . 6 (∃!𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
440435, 439bitr3i 280 . . . . 5 (∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ (∃𝑥𝐷𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑥𝐷𝑦𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) → 𝑥 = 𝑦)))
441420, 434, 440sylanbrc 586 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
442441ralrimiva 3114 . . 3 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))
443 an12 644 . . . . . . . 8 ((𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖))))))
444443opabbii 5104 . . . . . . 7 {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
445254, 444eqtri 2782 . . . . . 6 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
446445cnveqi 5721 . . . . 5 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
447 cnvopab 5975 . . . . 5 {⟨𝑥, 𝑡⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))} = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
448446, 447eqtri 2782 . . . 4 𝐹 = {⟨𝑡, 𝑥⟩ ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
449448fnopabg 6474 . . 3 (∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))) ↔ 𝐹 Fn (0[,)+∞))
450442, 449sylib 221 . 2 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹 Fn (0[,)+∞))
451 dff1o4 6616 . 2 (𝐹:𝐷1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷𝐹 Fn (0[,)+∞)))
452256, 450, 451sylanbrc 586 1 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝐹:𝐷1-1-onto→(0[,)+∞))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∃!weu 2588   ≠ wne 2952  ∀wral 3071  ∃wrex 3072  ∃!wreu 3073  {crab 3075   ⊆ wss 3861  ⟨cop 4532   class class class wbr 5037  {copab 5099   ↦ cmpt 5117  ◡ccnv 5528   Fn wfn 6336  –1-1-onto→wf1o 6340  ‘cfv 6341  (class class class)co 7157  ℂcc 10587  ℝcr 10588  0cc0 10589  1c1 10590   + caddc 10592   · cmul 10594  +∞cpnf 10724   < clt 10727   ≤ cle 10728   − cmin 10922   / cdiv 11349  ℕcn 11688  [,)cico 12795  [,]cicc 12796  ...cfz 12953  𝔼cee 26796   Btwn cbtwn 26797 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1st 7700  df-2nd 7701  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-er 8306  df-map 8425  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-div 11350  df-nn 11689  df-z 12035  df-uz 12297  df-ico 12799  df-icc 12800  df-fz 12954  df-ee 26799  df-btwn 26800 This theorem is referenced by:  axcontlem5  26876  axcontlem9  26880  axcontlem10  26881
 Copyright terms: Public domain W3C validator