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

Theorem axcontlem4 28850
Description: Lemma for axcont 28859. Given the separation assumption, 𝐴 is a subset of 𝐷. (Contributed by Scott Fenton, 18-Jun-2013.)
Hypothesis
Ref Expression
axcontlem4.1 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
Assertion
Ref Expression
axcontlem4 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴𝐷)
Distinct variable groups:   𝐴,𝑝,𝑥   𝐵,𝑝,𝑥,𝑦   𝑁,𝑝,𝑥,𝑦   𝑈,𝑝,𝑥,𝑦   𝑍,𝑝,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝐷(𝑥,𝑦,𝑝)

Proof of Theorem axcontlem4
Dummy variables 𝑏 𝑖 𝑟 𝑡 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr1 1212 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
2 n0 4346 . . . . . 6 (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏𝐵)
3 idd 24 . . . . . . . . . 10 (𝑏𝐵 → (𝐴 ⊆ (𝔼‘𝑁) → 𝐴 ⊆ (𝔼‘𝑁)))
4 ssel 3970 . . . . . . . . . . 11 (𝐵 ⊆ (𝔼‘𝑁) → (𝑏𝐵𝑏 ∈ (𝔼‘𝑁)))
54com12 32 . . . . . . . . . 10 (𝑏𝐵 → (𝐵 ⊆ (𝔼‘𝑁) → 𝑏 ∈ (𝔼‘𝑁)))
6 opeq2 4876 . . . . . . . . . . . . 13 (𝑦 = 𝑏 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑏⟩)
76breq2d 5161 . . . . . . . . . . . 12 (𝑦 = 𝑏 → (𝑥 Btwn ⟨𝑍, 𝑦⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑏⟩))
87rspcv 3602 . . . . . . . . . . 11 (𝑏𝐵 → (∀𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → 𝑥 Btwn ⟨𝑍, 𝑏⟩))
98ralimdv 3158 . . . . . . . . . 10 (𝑏𝐵 → (∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))
103, 5, 93anim123d 1439 . . . . . . . . 9 (𝑏𝐵 → ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩) → (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)))
1110anim2d 610 . . . . . . . 8 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))))
12 simplr1 1212 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
1312adantr 479 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝐴 ⊆ (𝔼‘𝑁))
14 simplr2 1213 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈𝐴)
1513, 14sseldd 3977 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 ∈ (𝔼‘𝑁))
16 simpr3 1193 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
17 simp2 1134 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈) → 𝑈𝐴)
18 breq1 5152 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑈 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
1918rspccva 3605 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑈𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2016, 17, 19syl2an 594 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2120adantr 479 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2215, 21jca 510 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
2312sselda 3976 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 ∈ (𝔼‘𝑁))
2416adantr 479 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
25 breq1 5152 . . . . . . . . . . . . . . 15 (𝑥 = 𝑝 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑝 Btwn ⟨𝑍, 𝑏⟩))
2625rspccva 3605 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2724, 26sylan 578 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2822, 23, 27jca32 514 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
29 an4 654 . . . . . . . . . . . 12 (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) ↔ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
3028, 29sylib 217 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
31 simp2 1134 . . . . . . . . . . . . . 14 ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩) → 𝑏 ∈ (𝔼‘𝑁))
32 simpl2r 1224 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍𝑈)
3332adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑍𝑈)
34 simpl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
3534ralimi 3072 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
36 eqcom 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖))
37 oveq2 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
38 1m0e1 12366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (1 − 0) = 1
3937, 38eqtrdi 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 0 → (1 − 𝑡) = 1)
4039oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → ((1 − 𝑡) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
41 oveq1 7426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → (𝑡 · (𝑏𝑖)) = (0 · (𝑏𝑖)))
4240, 41oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 0 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))))
4342eqeq1d 2727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 0 → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4436, 43bitrid 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 0 → ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4544ralbidv 3167 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4645biimpac 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖))
47 simpl2l 1223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
48 simpl3l 1225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
49 eqeefv 28786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
5047, 48, 49syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
51 fveecn 28785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
5247, 51sylan 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
53 simp1r 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
5453ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
55 fveecn 28785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
5654, 55sylancom 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
57 mullid 11245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
58 mul02 11424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏𝑖) ∈ ℂ → (0 · (𝑏𝑖)) = 0)
5957, 58oveqan12d 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = ((𝑍𝑖) + 0))
60 addrid 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
6160adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
6259, 61eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6352, 56, 62syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6463eqeq1d 2727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ (𝑍𝑖) = (𝑈𝑖)))
6564ralbidva 3165 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
6650, 65bitr4d 281 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
6746, 66imbitrrid 245 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → 𝑍 = 𝑈))
6867expdimp 451 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) → (𝑡 = 0 → 𝑍 = 𝑈))
6935, 68sylan2 591 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑡 = 0 → 𝑍 = 𝑈))
7069necon3d 2950 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑍𝑈𝑡 ≠ 0))
7133, 70mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑡 ≠ 0)
72 simp1l 1194 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73 simp2l 1196 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑍 ∈ (𝔼‘𝑁))
7472, 73, 533jca 1125 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))
75 simp2l 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ (0[,]1))
76 elicc01 13478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
7776simp1bi 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
7875, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
79 simp2r 1197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ (0[,]1))
80 elicc01 13478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
8180simp1bi 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
8279, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℝ)
8378, 82letrid 11398 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠𝑠𝑡))
84 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡𝑠)
8578adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡 ∈ ℝ)
8676simp2bi 1143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
8775, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑡)
8887adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ≤ 𝑡)
8982adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑠 ∈ ℝ)
90 0red 11249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ∈ ℝ)
91 simp3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
9278, 87, 91ne0gt0d 11383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 < 𝑡)
9392adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑡)
9490, 85, 89, 93, 84ltletrd 11406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑠)
95 divelunit 13506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9685, 88, 89, 94, 95syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9784, 96mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → (𝑡 / 𝑠) ∈ (0[,]1))
98 simp12 1201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑍 ∈ (𝔼‘𝑁))
9998ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
10099, 51sylancom 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
101 simp13 1202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑏 ∈ (𝔼‘𝑁))
102101ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
103102, 55sylancom 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
10477recnd 11274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
10575, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
106105ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
10781recnd 11274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℂ)
10879, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
109108ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
110 0red 11249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ∈ ℝ)
11178ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
11282ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
11387ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ 𝑡)
114 simpll3 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
115111, 113, 114ne0gt0d 11383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑡)
116 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡𝑠)
117110, 111, 112, 115, 116ltletrd 11406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑠)
118117gt0ne0d 11810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
119 divcl 11911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (𝑡 / 𝑠) ∈ ℂ)
120119adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑡 / 𝑠) ∈ ℂ)
121 ax-1cn 11198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ ℂ
122 simpr2 1192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → 𝑠 ∈ ℂ)
123 subcl 11491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
124121, 122, 123sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − 𝑠) ∈ ℂ)
125 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
126124, 125mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
127 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
128122, 127mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑠 · (𝑏𝑖)) ∈ ℂ)
129120, 126, 128adddid 11270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))))
130129oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
131 subcl 11491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
132121, 120, 131sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
133132, 125mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
134120, 126mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
135120, 128mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) ∈ ℂ)
136133, 134, 135addassd 11268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
137120, 124mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
138132, 137, 125adddird 11271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
139 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
140 subdi 11679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑡 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
141121, 140mp3an2 1445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
142119, 139, 141syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
143119mulridd 11263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 1) = (𝑡 / 𝑠))
144 divcan1 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
145143, 144oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
146142, 145eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
147146oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)))
148 simp1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑡 ∈ ℂ)
149 npncan 11513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
150121, 119, 148, 149mp3an2i 1462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
151147, 150eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
152151adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
153152oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
154120, 124, 125mulassd 11269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
155154oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
156138, 153, 1553eqtr3rd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = ((1 − 𝑡) · (𝑍𝑖)))
157120, 122, 127mulassd 11269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))
158144adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
159158oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = (𝑡 · (𝑏𝑖)))
160157, 159eqtr3d 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) = (𝑡 · (𝑏𝑖)))
161156, 160oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
162130, 136, 1613eqtr2rd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
163100, 103, 106, 109, 118, 162syl23anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
164163ralrimiva 3135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
165 oveq2 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑡 / 𝑠) → (1 − 𝑟) = (1 − (𝑡 / 𝑠)))
166165oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)))
167 oveq1 7426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
168166, 167oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑡 / 𝑠) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
169168eqeq2d 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑡 / 𝑠) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
170169ralbidv 3167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑡 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
171170rspcev 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑡 / 𝑠) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
17297, 164, 171syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
173172ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
17480simp2bi 1143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
17579, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑠)
176 divelunit 13506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑠 ∈ ℝ ∧ 0 ≤ 𝑠) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
17782, 175, 78, 92, 176syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
178177biimpar 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → (𝑠 / 𝑡) ∈ (0[,]1))
179 simp112 1300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
180 simp3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
181179, 180, 51syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
182 simp113 1301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
183182, 180, 55syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
184 simp12r 1284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
185184, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
186 simp12l 1283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
187186, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
188 simp13 1202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
189 divcl 11911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (𝑠 / 𝑡) ∈ ℂ)
190189adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑠 / 𝑡) ∈ ℂ)
191 simpr2 1192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → 𝑡 ∈ ℂ)
192 subcl 11491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
193121, 191, 192sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − 𝑡) ∈ ℂ)
194 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
195193, 194mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
196 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
197191, 196mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑡 · (𝑏𝑖)) ∈ ℂ)
198190, 195, 197adddid 11270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))))
199198oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
200 subcl 11491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
201121, 190, 200sylancr 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
202201, 194mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
203190, 195mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
204190, 197mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) ∈ ℂ)
205202, 203, 204addassd 11268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
206 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
207 subdi 11679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑠 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
208121, 207mp3an2 1445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
209189, 206, 208syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
210189mulridd 11263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 1) = (𝑠 / 𝑡))
211 divcan1 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 𝑡) = 𝑠)
212210, 211oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
213209, 212eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
214213oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)))
215 simp1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
216 npncan 11513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
217121, 189, 215, 216mp3an2i 1462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
218214, 217eqtr2d 2766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑠) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))))
219218oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
220219adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
221190, 193mulcld 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
222201, 221, 194adddird 11271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
223190, 193, 194mulassd 11269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
224223oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
225220, 222, 2243eqtrrd 2770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = ((1 − 𝑠) · (𝑍𝑖)))
226190, 191, 196mulassd 11269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))
227211oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
228227adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
229226, 228eqtr3d 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) = (𝑠 · (𝑏𝑖)))
230225, 229oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))
231199, 205, 2303eqtr2rd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
232181, 183, 185, 187, 188, 231syl23anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
2332323expa 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
234233ralrimiva 3135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
235 oveq2 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑠 / 𝑡) → (1 − 𝑟) = (1 − (𝑠 / 𝑡)))
236235oveq1d 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)))
237 oveq1 7426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
238236, 237oveq12d 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑠 / 𝑡) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
239238eqeq2d 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑠 / 𝑡) → ((((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
240239ralbidv 3167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑠 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
241240rspcev 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑠 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
242178, 234, 241syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
243242ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑠𝑡 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
244173, 243orim12d 962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡𝑠𝑠𝑡) → (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
245 r19.43 3111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
246244, 245imbitrrdi 251 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡𝑠𝑠𝑡) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
24783, 246mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
248 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
249 oveq2 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (𝑟 · (𝑝𝑖)) = (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
250249oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
251248, 250eqeqan12d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
252251ralimi 3072 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
253 ralbi 3092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
254252, 253syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
255 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))
256 oveq2 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (𝑟 · (𝑈𝑖)) = (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
257256oveq2d 7435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
258255, 257eqeqan12rd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
259258ralimi 3072 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
260 ralbi 3092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
261259, 260syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
262254, 261orbi12d 916 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
263262rexbidv 3168 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
264247, 263syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
2652643expia 1118 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑡 ≠ 0 → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
266265com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
26774, 266sylan 578 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
268267imp 405 . . . . . . . . . . . . . . . . . . . 20 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
26971, 268mpd 15 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
270269ex 411 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
271270rexlimdvva 3201 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
272 simp3l 1198 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑈 ∈ (𝔼‘𝑁))
273 brbtwn 28782 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
274272, 73, 53, 273syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
275 simp3r 1199 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑝 ∈ (𝔼‘𝑁))
276 brbtwn 28782 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
277275, 73, 53, 276syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
278274, 277anbi12d 630 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
279 r19.26 3100 . . . . . . . . . . . . . . . . . . . 20 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
2802792rexbii 3118 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
281 reeanv 3216 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
282280, 281bitri 274 . . . . . . . . . . . . . . . . . 18 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
283278, 282bitr4di 288 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
284 brbtwn 28782 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
285272, 73, 275, 284syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
286 brbtwn 28782 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
287275, 73, 272, 286syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
288285, 287orbi12d 916 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
289 r19.43 3111 . . . . . . . . . . . . . . . . . 18 (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
290288, 289bitr4di 288 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
291271, 283, 2903imtr4d 293 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2922913expia 1118 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
293292impd 409 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29431, 293sylanl2 679 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2952943adantr2 1167 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
296295adantr 479 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29730, 296mpd 15 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
298297ralrimiva 3135 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
2992983exp2 1351 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))))
30011, 299syl6 35 . . . . . . 7 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
301300exlimiv 1925 . . . . . 6 (∃𝑏 𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3022, 301sylbi 216 . . . . 5 (𝐵 ≠ ∅ → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
303302com4l 92 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝐵 ≠ ∅ → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3043033impd 1345 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
305304imp32 417 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
306 axcontlem4.1 . . . 4 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
307306sseq2i 4006 . . 3 (𝐴𝐷𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)})
308 ssrab 4066 . . 3 (𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
309307, 308bitri 274 . 2 (𝐴𝐷 ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
3101, 305, 309sylanbrc 581 1 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2929  wral 3050  wrex 3059  {crab 3418  wss 3944  c0 4322  cop 4636   class class class wbr 5149  cfv 6549  (class class class)co 7419  cc 11138  cr 11139  0cc0 11140  1c1 11141   + caddc 11143   · cmul 11145   < clt 11280  cle 11281  cmin 11476   / cdiv 11903  cn 12245  [,]cicc 13362  ...cfz 13519  𝔼cee 28771   Btwn cbtwn 28772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-z 12592  df-uz 12856  df-icc 13366  df-fz 13520  df-ee 28774  df-btwn 28775
This theorem is referenced by:  axcontlem9  28855  axcontlem10  28856
  Copyright terms: Public domain W3C validator