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

Theorem axcontlem4 25892
Description: Lemma for axcont 25901. 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 1123 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
2 n0 3964 . . . . . 6 (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏𝐵)
3 idd 24 . . . . . . . . . 10 (𝑏𝐵 → (𝐴 ⊆ (𝔼‘𝑁) → 𝐴 ⊆ (𝔼‘𝑁)))
4 ssel 3630 . . . . . . . . . . 11 (𝐵 ⊆ (𝔼‘𝑁) → (𝑏𝐵𝑏 ∈ (𝔼‘𝑁)))
54com12 32 . . . . . . . . . 10 (𝑏𝐵 → (𝐵 ⊆ (𝔼‘𝑁) → 𝑏 ∈ (𝔼‘𝑁)))
6 opeq2 4434 . . . . . . . . . . . . 13 (𝑦 = 𝑏 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑏⟩)
76breq2d 4697 . . . . . . . . . . . 12 (𝑦 = 𝑏 → (𝑥 Btwn ⟨𝑍, 𝑦⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑏⟩))
87rspcv 3336 . . . . . . . . . . 11 (𝑏𝐵 → (∀𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → 𝑥 Btwn ⟨𝑍, 𝑏⟩))
98ralimdv 2992 . . . . . . . . . 10 (𝑏𝐵 → (∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))
103, 5, 93anim123d 1446 . . . . . . . . 9 (𝑏𝐵 → ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩) → (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)))
1110anim2d 588 . . . . . . . 8 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))))
12 simplr1 1123 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
1312adantr 480 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝐴 ⊆ (𝔼‘𝑁))
14 simplr2 1124 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈𝐴)
1513, 14sseldd 3637 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 ∈ (𝔼‘𝑁))
16 simpr3 1089 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
17 simp2 1082 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈) → 𝑈𝐴)
18 breq1 4688 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑈 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
1918rspccva 3339 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑈𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2016, 17, 19syl2an 493 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2120adantr 480 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2215, 21jca 553 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
2312sselda 3636 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 ∈ (𝔼‘𝑁))
2416adantr 480 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
25 breq1 4688 . . . . . . . . . . . . . . 15 (𝑥 = 𝑝 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑝 Btwn ⟨𝑍, 𝑏⟩))
2625rspccva 3339 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2724, 26sylan 487 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2822, 23, 27jca32 557 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
29 an4 882 . . . . . . . . . . . 12 (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) ↔ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
3028, 29sylib 208 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
31 simp2 1082 . . . . . . . . . . . . . 14 ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩) → 𝑏 ∈ (𝔼‘𝑁))
32 simpl2r 1135 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍𝑈)
3332adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑍𝑈)
34 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
3534ralimi 2981 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
36 eqcom 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖))
37 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
38 1m0e1 11169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (1 − 0) = 1
3937, 38syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 0 → (1 − 𝑡) = 1)
4039oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → ((1 − 𝑡) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
41 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → (𝑡 · (𝑏𝑖)) = (0 · (𝑏𝑖)))
4240, 41oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 0 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))))
4342eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 0 → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4436, 43syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 0 → ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4544ralbidv 3015 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4645biimpac 502 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖))
47 simpl2l 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
48 simpl3l 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
49 eqeefv 25828 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
5047, 48, 49syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
51 fveecn 25827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
5247, 51sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
53 simp1r 1106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
5453ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
55 fveecn 25827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
5654, 55sylancom 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
57 mulid2 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
58 mul02 10252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏𝑖) ∈ ℂ → (0 · (𝑏𝑖)) = 0)
5957, 58oveqan12d 6709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = ((𝑍𝑖) + 0))
60 addid1 10254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
6160adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
6259, 61eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6352, 56, 62syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6463eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ (𝑍𝑖) = (𝑈𝑖)))
6564ralbidva 3014 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
6650, 65bitr4d 271 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
6746, 66syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → 𝑍 = 𝑈))
6867expdimp 452 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) → (𝑡 = 0 → 𝑍 = 𝑈))
6935, 68sylan2 490 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑡 = 0 → 𝑍 = 𝑈))
7069necon3d 2844 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑍𝑈𝑡 ≠ 0))
7133, 70mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑡 ≠ 0)
72 simp1l 1105 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73 simp2l 1107 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑍 ∈ (𝔼‘𝑁))
7472, 73, 533jca 1261 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))
75 simp2l 1107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ (0[,]1))
76 0re 10078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 ∈ ℝ
77 1re 10077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
7876, 77elicc2i 12277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
7978simp1bi 1096 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
8075, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
81 simp2r 1108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ (0[,]1))
8276, 77elicc2i 12277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
8382simp1bi 1096 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
8481, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℝ)
8580, 84letrid 10227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠𝑠𝑡))
86 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡𝑠)
8780adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡 ∈ ℝ)
8878simp2bi 1097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
8975, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑡)
9089adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ≤ 𝑡)
9184adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑠 ∈ ℝ)
92 0red 10079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ∈ ℝ)
93 simp3 1083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
9480, 89, 93ne0gt0d 10212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 < 𝑡)
9594adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑡)
9692, 87, 91, 95, 86ltletrd 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑠)
97 divelunit 12352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9887, 90, 91, 96, 97syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9986, 98mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → (𝑡 / 𝑠) ∈ (0[,]1))
100 simp12 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑍 ∈ (𝔼‘𝑁))
101100ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
102101, 51sylancom 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
103 simp13 1113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑏 ∈ (𝔼‘𝑁))
104103ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
105104, 55sylancom 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
10679recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
10775, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
108107ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
10983recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℂ)
11081, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
111110ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
112 0red 10079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ∈ ℝ)
11380ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
11484ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
11589ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ 𝑡)
116 simpll3 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
117113, 115, 116ne0gt0d 10212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑡)
118 simplr 807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡𝑠)
119112, 113, 114, 117, 118ltletrd 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑠)
120119gt0ne0d 10630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
121 divcl 10729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (𝑡 / 𝑠) ∈ ℂ)
122121adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑡 / 𝑠) ∈ ℂ)
123 ax-1cn 10032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ ℂ
124 simpr2 1088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → 𝑠 ∈ ℂ)
125 subcl 10318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
126123, 124, 125sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − 𝑠) ∈ ℂ)
127 simpll 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
128126, 127mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
129 simplr 807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
130124, 129mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑠 · (𝑏𝑖)) ∈ ℂ)
131122, 128, 130adddid 10102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))))
132131oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
133 subcl 10318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
134123, 122, 133sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
135134, 127mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
136122, 128mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
137122, 130mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) ∈ ℂ)
138135, 136, 137addassd 10100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
139122, 126mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
140134, 139, 127adddird 10103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
141 simp2 1082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
142 subdi 10501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑡 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
143123, 142mp3an2 1452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
144121, 141, 143syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
145121mulid1d 10095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 1) = (𝑡 / 𝑠))
146 divcan1 10732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
147145, 146oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
148144, 147eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
149148oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)))
150 simp1 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑡 ∈ ℂ)
151 npncan 10340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
152123, 151mp3an1 1451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
153121, 150, 152syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
154149, 153eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
155154adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
156155oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
157122, 126, 127mulassd 10101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
158157oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
159140, 156, 1583eqtr3rd 2694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = ((1 − 𝑡) · (𝑍𝑖)))
160122, 124, 129mulassd 10101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))
161146adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
162161oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = (𝑡 · (𝑏𝑖)))
163160, 162eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) = (𝑡 · (𝑏𝑖)))
164159, 163oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
165132, 138, 1643eqtr2rd 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
166102, 105, 108, 111, 120, 165syl23anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
167166ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
168 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑡 / 𝑠) → (1 − 𝑟) = (1 − (𝑡 / 𝑠)))
169168oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)))
170 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
171169, 170oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑡 / 𝑠) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
172171eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑡 / 𝑠) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
173172ralbidv 3015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑡 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
174173rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑡 / 𝑠) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
17599, 167, 174syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
176175ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
17782simp2bi 1097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
17881, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑠)
179 divelunit 12352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑠 ∈ ℝ ∧ 0 ≤ 𝑠) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
18084, 178, 80, 94, 179syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
181180biimpar 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → (𝑠 / 𝑡) ∈ (0[,]1))
182 simp112 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
183 simp3 1083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
184182, 183, 51syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
185 simp113 1212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
186185, 183, 55syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
187 simp12r 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
188187, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
189 simp12l 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
190189, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
191 simp13 1113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
192 divcl 10729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (𝑠 / 𝑡) ∈ ℂ)
193192adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑠 / 𝑡) ∈ ℂ)
194 simpr2 1088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → 𝑡 ∈ ℂ)
195 subcl 10318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
196123, 194, 195sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − 𝑡) ∈ ℂ)
197 simpll 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
198196, 197mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
199 simplr 807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
200194, 199mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑡 · (𝑏𝑖)) ∈ ℂ)
201193, 198, 200adddid 10102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))))
202201oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
203 subcl 10318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
204123, 193, 203sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
205204, 197mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
206193, 198mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
207193, 200mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) ∈ ℂ)
208205, 206, 207addassd 10100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
209 simp2 1082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
210 subdi 10501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑠 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
211123, 210mp3an2 1452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
212192, 209, 211syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
213192mulid1d 10095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 1) = (𝑠 / 𝑡))
214 divcan1 10732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 𝑡) = 𝑠)
215213, 214oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
216212, 215eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
217216oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)))
218 simp1 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
219 npncan 10340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
220123, 219mp3an1 1451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
221192, 218, 220syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
222217, 221eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑠) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))))
223222oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
224223adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
225193, 196mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
226204, 225, 197adddird 10103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
227193, 196, 197mulassd 10101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
228227oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
229224, 226, 2283eqtrrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = ((1 − 𝑠) · (𝑍𝑖)))
230193, 194, 199mulassd 10101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))
231214oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
232231adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
233230, 232eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) = (𝑠 · (𝑏𝑖)))
234229, 233oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))
235202, 208, 2343eqtr2rd 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
236184, 186, 188, 190, 191, 235syl23anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
2372363expa 1284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
238237ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
239 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑠 / 𝑡) → (1 − 𝑟) = (1 − (𝑠 / 𝑡)))
240239oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)))
241 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
242240, 241oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑠 / 𝑡) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
243242eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑠 / 𝑡) → ((((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
244243ralbidv 3015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑠 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
245244rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑠 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
246181, 238, 245syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
247246ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑠𝑡 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
248176, 247orim12d 901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡𝑠𝑠𝑡) → (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
249 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 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
250248, 249syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡𝑠𝑠𝑡) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
25185, 250mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
252 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
253 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (𝑟 · (𝑝𝑖)) = (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
254253oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
255252, 254eqeqan12d 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
256255ralimi 2981 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
257 ralbi 3097 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
258256, 257syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
259 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))
260 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (𝑟 · (𝑈𝑖)) = (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
261260oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
262259, 261eqeqan12rd 2669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
263262ralimi 2981 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
264 ralbi 3097 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
265263, 264syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
266258, 265orbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
267266rexbidv 3081 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
268251, 267syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
2692683expia 1286 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑡 ≠ 0 → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
270269com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
27174, 270sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
272271imp 444 . . . . . . . . . . . . . . . . . . . 20 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
27371, 272mpd 15 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
274273ex 449 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
275274rexlimdvva 3067 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
276 simp3l 1109 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑈 ∈ (𝔼‘𝑁))
277 brbtwn 25824 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
278276, 73, 53, 277syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
279 simp3r 1110 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑝 ∈ (𝔼‘𝑁))
280 brbtwn 25824 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
281279, 73, 53, 280syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
282278, 281anbi12d 747 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
283 r19.26 3093 . . . . . . . . . . . . . . . . . . . 20 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
2842832rexbii 3071 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
285 reeanv 3136 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
286284, 285bitri 264 . . . . . . . . . . . . . . . . . 18 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
287282, 286syl6bbr 278 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
288 brbtwn 25824 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
289276, 73, 279, 288syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
290 brbtwn 25824 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
291279, 73, 276, 290syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
292289, 291orbi12d 746 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
293 r19.43 3122 . . . . . . . . . . . . . . . . . 18 (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
294292, 293syl6bbr 278 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
295275, 287, 2943imtr4d 283 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2962953expia 1286 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
297296impd 446 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29831, 297sylanl2 684 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2992983adantr2 1241 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
300299adantr 480 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
30130, 300mpd 15 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
302301ralrimiva 2995 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
3033023exp2 1307 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))))
30411, 303syl6 35 . . . . . . 7 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
305304exlimiv 1898 . . . . . 6 (∃𝑏 𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3062, 305sylbi 207 . . . . 5 (𝐵 ≠ ∅ → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
307306com4l 92 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝐵 ≠ ∅ → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3083073impd 1303 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
309308imp32 448 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
310 axcontlem4.1 . . . 4 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
311310sseq2i 3663 . . 3 (𝐴𝐷𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)})
312 ssrab 3713 . . 3 (𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
313311, 312bitri 264 . 2 (𝐴𝐷 ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
3141, 309, 313sylanbrc 699 1 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  wss 3607  c0 3948  cop 4216   class class class wbr 4685  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  [,]cicc 12216  ...cfz 12364  𝔼cee 25813   Btwn cbtwn 25814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-z 11416  df-uz 11726  df-icc 12220  df-fz 12365  df-ee 25816  df-btwn 25817
This theorem is referenced by:  axcontlem9  25897  axcontlem10  25898
  Copyright terms: Public domain W3C validator