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

Theorem axcontlem4 27471
Description: Lemma for axcont 27480. 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 1214 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
2 n0 4291 . . . . . 6 (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏𝐵)
3 idd 24 . . . . . . . . . 10 (𝑏𝐵 → (𝐴 ⊆ (𝔼‘𝑁) → 𝐴 ⊆ (𝔼‘𝑁)))
4 ssel 3924 . . . . . . . . . . 11 (𝐵 ⊆ (𝔼‘𝑁) → (𝑏𝐵𝑏 ∈ (𝔼‘𝑁)))
54com12 32 . . . . . . . . . 10 (𝑏𝐵 → (𝐵 ⊆ (𝔼‘𝑁) → 𝑏 ∈ (𝔼‘𝑁)))
6 opeq2 4816 . . . . . . . . . . . . 13 (𝑦 = 𝑏 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑏⟩)
76breq2d 5099 . . . . . . . . . . . 12 (𝑦 = 𝑏 → (𝑥 Btwn ⟨𝑍, 𝑦⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑏⟩))
87rspcv 3566 . . . . . . . . . . 11 (𝑏𝐵 → (∀𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → 𝑥 Btwn ⟨𝑍, 𝑏⟩))
98ralimdv 3163 . . . . . . . . . 10 (𝑏𝐵 → (∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))
103, 5, 93anim123d 1442 . . . . . . . . 9 (𝑏𝐵 → ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩) → (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)))
1110anim2d 612 . . . . . . . 8 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))))
12 simplr1 1214 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
1312adantr 481 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝐴 ⊆ (𝔼‘𝑁))
14 simplr2 1215 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈𝐴)
1513, 14sseldd 3932 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 ∈ (𝔼‘𝑁))
16 simpr3 1195 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
17 simp2 1136 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈) → 𝑈𝐴)
18 breq1 5090 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑈 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
1918rspccva 3569 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑈𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2016, 17, 19syl2an 596 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2120adantr 481 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2215, 21jca 512 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
2312sselda 3931 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 ∈ (𝔼‘𝑁))
2416adantr 481 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
25 breq1 5090 . . . . . . . . . . . . . . 15 (𝑥 = 𝑝 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑝 Btwn ⟨𝑍, 𝑏⟩))
2625rspccva 3569 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2724, 26sylan 580 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2822, 23, 27jca32 516 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
29 an4 653 . . . . . . . . . . . 12 (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) ↔ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
3028, 29sylib 217 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
31 simp2 1136 . . . . . . . . . . . . . 14 ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩) → 𝑏 ∈ (𝔼‘𝑁))
32 simpl2r 1226 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍𝑈)
3332adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑍𝑈)
34 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
3534ralimi 3083 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
36 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖))
37 oveq2 7325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
38 1m0e1 12174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (1 − 0) = 1
3937, 38eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 0 → (1 − 𝑡) = 1)
4039oveq1d 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → ((1 − 𝑡) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
41 oveq1 7324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → (𝑡 · (𝑏𝑖)) = (0 · (𝑏𝑖)))
4240, 41oveq12d 7335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 0 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))))
4342eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 0 → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4436, 43bitrid 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 0 → ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4544ralbidv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4645biimpac 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖))
47 simpl2l 1225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
48 simpl3l 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
49 eqeefv 27407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
5047, 48, 49syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
51 fveecn 27406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
5247, 51sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
53 simp1r 1197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
5453ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
55 fveecn 27406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
5654, 55sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
57 mulid2 11054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
58 mul02 11233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏𝑖) ∈ ℂ → (0 · (𝑏𝑖)) = 0)
5957, 58oveqan12d 7336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = ((𝑍𝑖) + 0))
60 addid1 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
6160adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
6259, 61eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6352, 56, 62syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6463eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ (𝑍𝑖) = (𝑈𝑖)))
6564ralbidva 3169 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2962 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑍𝑈𝑡 ≠ 0))
7133, 70mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑡 ≠ 0)
72 simp1l 1196 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73 simp2l 1198 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑍 ∈ (𝔼‘𝑁))
7472, 73, 533jca 1127 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))
75 simp2l 1198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ (0[,]1))
76 elicc01 13278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
7776simp1bi 1144 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
7875, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
79 simp2r 1199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ (0[,]1))
80 elicc01 13278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
8180simp1bi 1144 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
8279, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℝ)
8378, 82letrid 11207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠𝑠𝑡))
84 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡𝑠)
8578adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡 ∈ ℝ)
8676simp2bi 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ∈ ℝ)
91 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
9278, 87, 91ne0gt0d 11192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 < 𝑡)
9392adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑡)
9490, 85, 89, 93, 84ltletrd 11215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑠)
95 divelunit 13306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9685, 88, 89, 94, 95syl22anc 836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9784, 96mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → (𝑡 / 𝑠) ∈ (0[,]1))
98 simp12 1203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑍 ∈ (𝔼‘𝑁))
9998ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
10099, 51sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
101 simp13 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑏 ∈ (𝔼‘𝑁))
102101ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
103102, 55sylancom 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
10477recnd 11083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
10575, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
106105ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
10781recnd 11083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℂ)
10879, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
109108ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
110 0red 11058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ∈ ℝ)
11178ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
11282ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
11387ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ 𝑡)
114 simpll3 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
115111, 113, 114ne0gt0d 11192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑡)
116 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡𝑠)
117110, 111, 112, 115, 116ltletrd 11215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑠)
118117gt0ne0d 11619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
119 divcl 11719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (𝑡 / 𝑠) ∈ ℂ)
120119adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑡 / 𝑠) ∈ ℂ)
121 ax-1cn 11009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ ℂ
122 simpr2 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → 𝑠 ∈ ℂ)
123 subcl 11300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
124121, 122, 123sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − 𝑠) ∈ ℂ)
125 simpll 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
126124, 125mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
127 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
128122, 127mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑠 · (𝑏𝑖)) ∈ ℂ)
129120, 126, 128adddid 11079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))))
130129oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
131 subcl 11300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
132121, 120, 131sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
133132, 125mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
134120, 126mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
135120, 128mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) ∈ ℂ)
136133, 134, 135addassd 11077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
137120, 124mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
138132, 137, 125adddird 11080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
139 simp2 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
140 subdi 11488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑡 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
141121, 140mp3an2 1448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
142119, 139, 141syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
143119mulid1d 11072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 1) = (𝑡 / 𝑠))
144 divcan1 11722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
145143, 144oveq12d 7335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
146142, 145eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
147146oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)))
148 simp1 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑡 ∈ ℂ)
149 npncan 11322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
150121, 119, 148, 149mp3an2i 1465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
151147, 150eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
152151adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
153152oveq1d 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
154120, 124, 125mulassd 11078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
155154oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
156138, 153, 1553eqtr3rd 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = ((1 − 𝑡) · (𝑍𝑖)))
157120, 122, 127mulassd 11078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))
158144adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
159158oveq1d 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = (𝑡 · (𝑏𝑖)))
160157, 159eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) = (𝑡 · (𝑏𝑖)))
161156, 160oveq12d 7335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
162130, 136, 1613eqtr2rd 2784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
163100, 103, 106, 109, 118, 162syl23anc 1376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
164163ralrimiva 3140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
165 oveq2 7325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑡 / 𝑠) → (1 − 𝑟) = (1 − (𝑡 / 𝑠)))
166165oveq1d 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)))
167 oveq1 7324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
168166, 167oveq12d 7335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑡 / 𝑠) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
169168eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑡 / 𝑠) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
170169ralbidv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑡 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
171170rspcev 3570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
17579, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑠)
176 divelunit 13306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑠 ∈ ℝ ∧ 0 ≤ 𝑠) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
17782, 175, 78, 92, 176syl22anc 836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
178177biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → (𝑠 / 𝑡) ∈ (0[,]1))
179 simp112 1302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
180 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
181179, 180, 51syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
182 simp113 1303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
183182, 180, 55syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
184 simp12r 1286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
185184, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
186 simp12l 1285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
187186, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
188 simp13 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
189 divcl 11719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (𝑠 / 𝑡) ∈ ℂ)
190189adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑠 / 𝑡) ∈ ℂ)
191 simpr2 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → 𝑡 ∈ ℂ)
192 subcl 11300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
193121, 191, 192sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − 𝑡) ∈ ℂ)
194 simpll 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
195193, 194mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
196 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
197191, 196mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑡 · (𝑏𝑖)) ∈ ℂ)
198190, 195, 197adddid 11079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))))
199198oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
200 subcl 11300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
201121, 190, 200sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
202201, 194mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
203190, 195mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
204190, 197mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) ∈ ℂ)
205202, 203, 204addassd 11077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
206 simp2 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
207 subdi 11488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑠 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
208121, 207mp3an2 1448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
209189, 206, 208syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
210189mulid1d 11072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 1) = (𝑠 / 𝑡))
211 divcan1 11722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 𝑡) = 𝑠)
212210, 211oveq12d 7335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
213209, 212eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
214213oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)))
215 simp1 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
216 npncan 11322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
217121, 189, 215, 216mp3an2i 1465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
218214, 217eqtr2d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑠) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))))
219218oveq1d 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
220219adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
221190, 193mulcld 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
222201, 221, 194adddird 11080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
223190, 193, 194mulassd 11078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
224223oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
225220, 222, 2243eqtrrd 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = ((1 − 𝑠) · (𝑍𝑖)))
226190, 191, 196mulassd 11078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))
227211oveq1d 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
228227adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
229226, 228eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) = (𝑠 · (𝑏𝑖)))
230225, 229oveq12d 7335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))
231199, 205, 2303eqtr2rd 2784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
232181, 183, 185, 187, 188, 231syl23anc 1376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
2332323expa 1117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
234233ralrimiva 3140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
235 oveq2 7325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑠 / 𝑡) → (1 − 𝑟) = (1 − (𝑠 / 𝑡)))
236235oveq1d 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)))
237 oveq1 7324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
238236, 237oveq12d 7335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑠 / 𝑡) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
239238eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑠 / 𝑡) → ((((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
240239ralbidv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑠 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
241240rspcev 3570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡𝑠𝑠𝑡) → (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
245 r19.43 3122 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (𝑟 · (𝑝𝑖)) = (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
250249oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
251248, 250eqeqan12d 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
252251ralimi 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
253 ralbi 3103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (𝑟 · (𝑈𝑖)) = (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
257256oveq2d 7333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
258255, 257eqeqan12rd 2752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
259258ralimi 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
260 ralbi 3103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3172 . . . . . . . . . . . . . . . . . . . . . . . . 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 1120 . . . . . . . . . . . . . . . . . . . . . . 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 3202 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
272 simp3l 1200 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑈 ∈ (𝔼‘𝑁))
273 brbtwn 27403 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
274272, 73, 53, 273syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
275 simp3r 1201 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑝 ∈ (𝔼‘𝑁))
276 brbtwn 27403 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
277275, 73, 53, 276syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
278274, 277anbi12d 631 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
279 r19.26 3111 . . . . . . . . . . . . . . . . . . . 20 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
2802792rexbii 3125 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
281 reeanv 3214 . . . . . . . . . . . . . . . . . . 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 27403 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
285272, 73, 275, 284syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
286 brbtwn 27403 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
287275, 73, 272, 286syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
288285, 287orbi12d 916 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
289 r19.43 3122 . . . . . . . . . . . . . . . . . 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 1120 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
293292impd 411 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29431, 293sylanl2 678 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2952943adantr2 1169 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
296295adantr 481 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29730, 296mpd 15 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
298297ralrimiva 3140 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
2992983exp2 1353 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))))
30011, 299syl6 35 . . . . . . 7 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
301300exlimiv 1932 . . . . . 6 (∃𝑏 𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3022, 301sylbi 216 . . . . 5 (𝐵 ≠ ∅ → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
303302com4l 92 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝐵 ≠ ∅ → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3043033impd 1347 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
305304imp32 419 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
306 axcontlem4.1 . . . 4 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
307306sseq2i 3960 . . 3 (𝐴𝐷𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)})
308 ssrab 4017 . . 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 844  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2941  wral 3062  wrex 3071  {crab 3404  wss 3897  c0 4267  cop 4577   class class class wbr 5087  cfv 6466  (class class class)co 7317  cc 10949  cr 10950  0cc0 10951  1c1 10952   + caddc 10954   · cmul 10956   < clt 11089  cle 11090  cmin 11285   / cdiv 11712  cn 12053  [,]cicc 13162  ...cfz 13319  𝔼cee 27392   Btwn cbtwn 27393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-1st 7878  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-er 8548  df-map 8667  df-en 8784  df-dom 8785  df-sdom 8786  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-div 11713  df-nn 12054  df-z 12400  df-uz 12663  df-icc 13166  df-fz 13320  df-ee 27395  df-btwn 27396
This theorem is referenced by:  axcontlem9  27476  axcontlem10  27477
  Copyright terms: Public domain W3C validator