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

Theorem axcontlem4 27916
Description: Lemma for axcont 27925. 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 1215 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
2 n0 4306 . . . . . 6 (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏𝐵)
3 idd 24 . . . . . . . . . 10 (𝑏𝐵 → (𝐴 ⊆ (𝔼‘𝑁) → 𝐴 ⊆ (𝔼‘𝑁)))
4 ssel 3937 . . . . . . . . . . 11 (𝐵 ⊆ (𝔼‘𝑁) → (𝑏𝐵𝑏 ∈ (𝔼‘𝑁)))
54com12 32 . . . . . . . . . 10 (𝑏𝐵 → (𝐵 ⊆ (𝔼‘𝑁) → 𝑏 ∈ (𝔼‘𝑁)))
6 opeq2 4831 . . . . . . . . . . . . 13 (𝑦 = 𝑏 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑏⟩)
76breq2d 5117 . . . . . . . . . . . 12 (𝑦 = 𝑏 → (𝑥 Btwn ⟨𝑍, 𝑦⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑏⟩))
87rspcv 3577 . . . . . . . . . . 11 (𝑏𝐵 → (∀𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → 𝑥 Btwn ⟨𝑍, 𝑏⟩))
98ralimdv 3166 . . . . . . . . . 10 (𝑏𝐵 → (∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))
103, 5, 93anim123d 1443 . . . . . . . . 9 (𝑏𝐵 → ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩) → (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)))
1110anim2d 612 . . . . . . . 8 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))))
12 simplr1 1215 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
1312adantr 481 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝐴 ⊆ (𝔼‘𝑁))
14 simplr2 1216 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈𝐴)
1513, 14sseldd 3945 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 ∈ (𝔼‘𝑁))
16 simpr3 1196 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
17 simp2 1137 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈) → 𝑈𝐴)
18 breq1 5108 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑈 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
1918rspccva 3580 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑈𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2016, 17, 19syl2an 596 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2120adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2215, 21jca 512 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
2312sselda 3944 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 ∈ (𝔼‘𝑁))
2416adantr 481 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
25 breq1 5108 . . . . . . . . . . . . . . 15 (𝑥 = 𝑝 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑝 Btwn ⟨𝑍, 𝑏⟩))
2625rspccva 3580 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2724, 26sylan 580 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2822, 23, 27jca32 516 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
29 an4 654 . . . . . . . . . . . 12 (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) ↔ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
3028, 29sylib 217 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
31 simp2 1137 . . . . . . . . . . . . . 14 ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩) → 𝑏 ∈ (𝔼‘𝑁))
32 simpl2r 1227 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍𝑈)
3332adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑍𝑈)
34 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
3534ralimi 3086 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
36 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖))
37 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
38 1m0e1 12274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (1 − 0) = 1
3937, 38eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 0 → (1 − 𝑡) = 1)
4039oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → ((1 − 𝑡) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
41 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → (𝑡 · (𝑏𝑖)) = (0 · (𝑏𝑖)))
4240, 41oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 0 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))))
4342eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 0 → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4436, 43bitrid 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 0 → ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4544ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4645biimpac 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖))
47 simpl2l 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
48 simpl3l 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
49 eqeefv 27852 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
5047, 48, 49syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
51 fveecn 27851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
5247, 51sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
53 simp1r 1198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
5453ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
55 fveecn 27851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
5654, 55sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
57 mulid2 11154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
58 mul02 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏𝑖) ∈ ℂ → (0 · (𝑏𝑖)) = 0)
5957, 58oveqan12d 7376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = ((𝑍𝑖) + 0))
60 addid1 11335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
6160adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
6259, 61eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6352, 56, 62syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6463eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ (𝑍𝑖) = (𝑈𝑖)))
6564ralbidva 3172 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
6650, 65bitr4d 281 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
6746, 66syl5ibr 245 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → 𝑍 = 𝑈))
6867expdimp 453 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) → (𝑡 = 0 → 𝑍 = 𝑈))
6935, 68sylan2 593 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑡 = 0 → 𝑍 = 𝑈))
7069necon3d 2964 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑍𝑈𝑡 ≠ 0))
7133, 70mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑡 ≠ 0)
72 simp1l 1197 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73 simp2l 1199 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑍 ∈ (𝔼‘𝑁))
7472, 73, 533jca 1128 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))
75 simp2l 1199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ (0[,]1))
76 elicc01 13383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
7776simp1bi 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
7875, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
79 simp2r 1200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ (0[,]1))
80 elicc01 13383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
8180simp1bi 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
8279, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℝ)
8378, 82letrid 11307 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠𝑠𝑡))
84 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡𝑠)
8578adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡 ∈ ℝ)
8676simp2bi 1146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
8775, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑡)
8887adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ≤ 𝑡)
8982adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑠 ∈ ℝ)
90 0red 11158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ∈ ℝ)
91 simp3 1138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
9278, 87, 91ne0gt0d 11292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 < 𝑡)
9392adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑡)
9490, 85, 89, 93, 84ltletrd 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑠)
95 divelunit 13411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑍 ∈ (𝔼‘𝑁))
9998ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
10099, 51sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
101 simp13 1205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑏 ∈ (𝔼‘𝑁))
102101ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
103102, 55sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
10477recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
10575, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
106105ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
10781recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℂ)
10879, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
109108ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
110 0red 11158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
115111, 113, 114ne0gt0d 11292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑡)
116 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡𝑠)
117110, 111, 112, 115, 116ltletrd 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑠)
118117gt0ne0d 11719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
119 divcl 11819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (𝑡 / 𝑠) ∈ ℂ)
120119adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑡 / 𝑠) ∈ ℂ)
121 ax-1cn 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ ℂ
122 simpr2 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → 𝑠 ∈ ℂ)
123 subcl 11400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
124121, 122, 123sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − 𝑠) ∈ ℂ)
125 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
126124, 125mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
127 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
128122, 127mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑠 · (𝑏𝑖)) ∈ ℂ)
129120, 126, 128adddid 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))))
130129oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
131 subcl 11400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
132121, 120, 131sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
133132, 125mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
134120, 126mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
135120, 128mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) ∈ ℂ)
136133, 134, 135addassd 11177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
137120, 124mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
138132, 137, 125adddird 11180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
139 simp2 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
140 subdi 11588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑡 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
141121, 140mp3an2 1449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
142119, 139, 141syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
143119mulid1d 11172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 1) = (𝑡 / 𝑠))
144 divcan1 11822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
145143, 144oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
146142, 145eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
147146oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)))
148 simp1 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑡 ∈ ℂ)
149 npncan 11422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
150121, 119, 148, 149mp3an2i 1466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
151147, 150eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
152151adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
153152oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
154120, 124, 125mulassd 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
155154oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
156138, 153, 1553eqtr3rd 2785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = ((1 − 𝑡) · (𝑍𝑖)))
157120, 122, 127mulassd 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))
158144adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
159158oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = (𝑡 · (𝑏𝑖)))
160157, 159eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) = (𝑡 · (𝑏𝑖)))
161156, 160oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
162130, 136, 1613eqtr2rd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
163100, 103, 106, 109, 118, 162syl23anc 1377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
164163ralrimiva 3143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
165 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑡 / 𝑠) → (1 − 𝑟) = (1 − (𝑡 / 𝑠)))
166165oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)))
167 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
168166, 167oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑡 / 𝑠) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
169168eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑡 / 𝑠) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
170169ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑡 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
171170rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑡 / 𝑠) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
17297, 164, 171syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
173172ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
17480simp2bi 1146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
17579, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑠)
176 divelunit 13411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑠 ∈ ℝ ∧ 0 ≤ 𝑠) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
17782, 175, 78, 92, 176syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
178177biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → (𝑠 / 𝑡) ∈ (0[,]1))
179 simp112 1303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
180 simp3 1138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
181179, 180, 51syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
182 simp113 1304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
183182, 180, 55syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
184 simp12r 1287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
185184, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
186 simp12l 1286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
187186, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
188 simp13 1205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
189 divcl 11819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (𝑠 / 𝑡) ∈ ℂ)
190189adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑠 / 𝑡) ∈ ℂ)
191 simpr2 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → 𝑡 ∈ ℂ)
192 subcl 11400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
193121, 191, 192sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − 𝑡) ∈ ℂ)
194 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
195193, 194mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
196 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
197191, 196mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑡 · (𝑏𝑖)) ∈ ℂ)
198190, 195, 197adddid 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))))
199198oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
200 subcl 11400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
201121, 190, 200sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
202201, 194mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
203190, 195mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
204190, 197mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) ∈ ℂ)
205202, 203, 204addassd 11177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
206 simp2 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
207 subdi 11588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑠 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
208121, 207mp3an2 1449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
209189, 206, 208syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
210189mulid1d 11172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 1) = (𝑠 / 𝑡))
211 divcan1 11822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 𝑡) = 𝑠)
212210, 211oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
213209, 212eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
214213oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)))
215 simp1 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
216 npncan 11422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
217121, 189, 215, 216mp3an2i 1466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
218214, 217eqtr2d 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑠) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))))
219218oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
220219adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
221190, 193mulcld 11175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
222201, 221, 194adddird 11180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
223190, 193, 194mulassd 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
224223oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
225220, 222, 2243eqtrrd 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = ((1 − 𝑠) · (𝑍𝑖)))
226190, 191, 196mulassd 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))
227211oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
228227adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
229226, 228eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) = (𝑠 · (𝑏𝑖)))
230225, 229oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))
231199, 205, 2303eqtr2rd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
232181, 183, 185, 187, 188, 231syl23anc 1377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
2332323expa 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
234233ralrimiva 3143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
235 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑠 / 𝑡) → (1 − 𝑟) = (1 − (𝑠 / 𝑡)))
236235oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)))
237 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
238236, 237oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑠 / 𝑡) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
239238eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑠 / 𝑡) → ((((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
240239ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑠 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
241240rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑠 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
242178, 234, 241syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
243242ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑠𝑡 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
244173, 243orim12d 963 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡𝑠𝑠𝑡) → (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
245 r19.43 3125 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
246244, 245syl6ibr 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 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (𝑟 · (𝑝𝑖)) = (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
250249oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
251248, 250eqeqan12d 2750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
252251ralimi 3086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
253 ralbi 3106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (𝑟 · (𝑈𝑖)) = (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
257256oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
258255, 257eqeqan12rd 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
259258ralimi 3086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
260 ralbi 3106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 917 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
263262rexbidv 3175 . . . . . . . . . . . . . . . . . . . . . . . . 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 1121 . . . . . . . . . . . . . . . . . . . . . . 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 580 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
268267imp 407 . . . . . . . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
271270rexlimdvva 3205 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
272 simp3l 1201 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑈 ∈ (𝔼‘𝑁))
273 brbtwn 27848 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
274272, 73, 53, 273syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
275 simp3r 1202 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑝 ∈ (𝔼‘𝑁))
276 brbtwn 27848 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
277275, 73, 53, 276syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
278274, 277anbi12d 631 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
279 r19.26 3114 . . . . . . . . . . . . . . . . . . . 20 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
2802792rexbii 3128 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
281 reeanv 3217 . . . . . . . . . . . . . . . . . . 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 27848 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
285272, 73, 275, 284syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
286 brbtwn 27848 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
287275, 73, 272, 286syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
288285, 287orbi12d 917 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
289 r19.43 3125 . . . . . . . . . . . . . . . . . 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 1121 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
293292impd 411 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29431, 293sylanl2 679 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2952943adantr2 1170 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
296295adantr 481 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29730, 296mpd 15 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
298297ralrimiva 3143 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
2992983exp2 1354 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))))
30011, 299syl6 35 . . . . . . 7 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
301300exlimiv 1933 . . . . . 6 (∃𝑏 𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3022, 301sylbi 216 . . . . 5 (𝐵 ≠ ∅ → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
303302com4l 92 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝐵 ≠ ∅ → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3043033impd 1348 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
305304imp32 419 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
306 axcontlem4.1 . . . 4 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
307306sseq2i 3973 . . 3 (𝐴𝐷𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)})
308 ssrab 4030 . . 3 (𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
309307, 308bitri 274 . 2 (𝐴𝐷 ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
3101, 305, 309sylanbrc 583 1 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  wss 3910  c0 4282  cop 4592   class class class wbr 5105  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  [,]cicc 13267  ...cfz 13424  𝔼cee 27837   Btwn cbtwn 27838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-z 12500  df-uz 12764  df-icc 13271  df-fz 13425  df-ee 27840  df-btwn 27841
This theorem is referenced by:  axcontlem9  27921  axcontlem10  27922
  Copyright terms: Public domain W3C validator