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

Theorem axcontlem4 25565
Description: Lemma for axcont 25574. 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 1095 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
2 n0 3889 . . . . . 6 (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏𝐵)
3 idd 24 . . . . . . . . . 10 (𝑏𝐵 → (𝐴 ⊆ (𝔼‘𝑁) → 𝐴 ⊆ (𝔼‘𝑁)))
4 ssel 3561 . . . . . . . . . . 11 (𝐵 ⊆ (𝔼‘𝑁) → (𝑏𝐵𝑏 ∈ (𝔼‘𝑁)))
54com12 32 . . . . . . . . . 10 (𝑏𝐵 → (𝐵 ⊆ (𝔼‘𝑁) → 𝑏 ∈ (𝔼‘𝑁)))
6 opeq2 4335 . . . . . . . . . . . . 13 (𝑦 = 𝑏 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑏⟩)
76breq2d 4589 . . . . . . . . . . . 12 (𝑦 = 𝑏 → (𝑥 Btwn ⟨𝑍, 𝑦⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑏⟩))
87rspcv 3277 . . . . . . . . . . 11 (𝑏𝐵 → (∀𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → 𝑥 Btwn ⟨𝑍, 𝑏⟩))
98ralimdv 2945 . . . . . . . . . 10 (𝑏𝐵 → (∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))
103, 5, 93anim123d 1397 . . . . . . . . 9 (𝑏𝐵 → ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩) → (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)))
1110anim2d 586 . . . . . . . 8 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))))
12 simplr1 1095 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
1312adantr 479 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝐴 ⊆ (𝔼‘𝑁))
14 simplr2 1096 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈𝐴)
1513, 14sseldd 3568 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 ∈ (𝔼‘𝑁))
16 simpr3 1061 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
17 simp2 1054 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈) → 𝑈𝐴)
18 breq1 4580 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑈 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
1918rspccva 3280 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑈𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2016, 17, 19syl2an 492 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2120adantr 479 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
2215, 21jca 552 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
2312sselda 3567 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 ∈ (𝔼‘𝑁))
2416adantr 479 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
25 breq1 4580 . . . . . . . . . . . . . . 15 (𝑥 = 𝑝 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑝 Btwn ⟨𝑍, 𝑏⟩))
2625rspccva 3280 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2724, 26sylan 486 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
2822, 23, 27jca32 555 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
29 an4 860 . . . . . . . . . . . 12 (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) ↔ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
3028, 29sylib 206 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
31 simp2 1054 . . . . . . . . . . . . . 14 ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩) → 𝑏 ∈ (𝔼‘𝑁))
32 simpl2r 1107 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍𝑈)
3332adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑍𝑈)
34 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
3534ralimi 2935 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
36 eqcom 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖))
37 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
38 1m0e1 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (1 − 0) = 1
3937, 38syl6eq 2659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 0 → (1 − 𝑡) = 1)
4039oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → ((1 − 𝑡) · (𝑍𝑖)) = (1 · (𝑍𝑖)))
41 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 0 → (𝑡 · (𝑏𝑖)) = (0 · (𝑏𝑖)))
4240, 41oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 0 → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))))
4342eqeq1d 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 0 → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (𝑈𝑖) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4436, 43syl5bb 270 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 0 → ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4544ralbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
4645biimpac 501 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖))
47 simpl2l 1106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
48 simpl3l 1108 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
49 eqeefv 25501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
5047, 48, 49syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
51 fveecn 25500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
5247, 51sylan 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
53 simp1r 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
5453ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
55 fveecn 25500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
5654, 55sylancom 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
57 mulid2 9894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → (1 · (𝑍𝑖)) = (𝑍𝑖))
58 mul02 10065 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏𝑖) ∈ ℂ → (0 · (𝑏𝑖)) = 0)
5957, 58oveqan12d 6546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = ((𝑍𝑖) + 0))
60 addid1 10067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑍𝑖) ∈ ℂ → ((𝑍𝑖) + 0) = (𝑍𝑖))
6160adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((𝑍𝑖) + 0) = (𝑍𝑖))
6259, 61eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6352, 56, 62syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑍𝑖))
6463eqeq1d 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ (𝑍𝑖) = (𝑈𝑖)))
6564ralbidva 2967 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖) ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
6650, 65bitr4d 269 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍𝑖)) + (0 · (𝑏𝑖))) = (𝑈𝑖)))
6746, 66syl5ibr 234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ 𝑡 = 0) → 𝑍 = 𝑈))
6867expdimp 451 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) → (𝑡 = 0 → 𝑍 = 𝑈))
6935, 68sylan2 489 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑡 = 0 → 𝑍 = 𝑈))
7069necon3d 2802 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → (𝑍𝑈𝑡 ≠ 0))
7133, 70mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) → 𝑡 ≠ 0)
72 simp1l 1077 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73 simp2l 1079 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑍 ∈ (𝔼‘𝑁))
7472, 73, 533jca 1234 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))
75 simp2l 1079 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ (0[,]1))
76 0re 9896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 ∈ ℝ
77 1re 9895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
7876, 77elicc2i 12066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
7978simp1bi 1068 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
8075, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
81 simp2r 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ (0[,]1))
8276, 77elicc2i 12066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
8382simp1bi 1068 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
8481, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℝ)
8580, 84letrid 10040 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠𝑠𝑡))
86 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡𝑠)
8780adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑡 ∈ ℝ)
8878simp2bi 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
8975, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑡)
9089adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ≤ 𝑡)
9184adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 𝑠 ∈ ℝ)
92 0red 9897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 ∈ ℝ)
93 simp3 1055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
9480, 89, 93ne0gt0d 10025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 < 𝑡)
9594adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑡)
9692, 87, 91, 95, 86ltletrd 10048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → 0 < 𝑠)
97 divelunit 12141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9887, 90, 91, 96, 97syl22anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡𝑠))
9986, 98mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → (𝑡 / 𝑠) ∈ (0[,]1))
100 simp12 1084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑍 ∈ (𝔼‘𝑁))
101100ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
102101, 51sylancom 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
103 simp13 1085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑏 ∈ (𝔼‘𝑁))
104103ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
105104, 55sylancom 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
10679recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
10775, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
108107ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
10983recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℂ)
11081, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
111110ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
112 0red 9897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ∈ ℝ)
11380ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
11484ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
11589ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ 𝑡)
116 simpll3 1094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
117113, 115, 116ne0gt0d 10025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑡)
118 simplr 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡𝑠)
119112, 113, 114, 117, 118ltletrd 10048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑠)
120119gt0ne0d 10441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
121 divcl 10540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (𝑡 / 𝑠) ∈ ℂ)
122121adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑡 / 𝑠) ∈ ℂ)
123 ax-1cn 9850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ ℂ
124 simpr2 1060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → 𝑠 ∈ ℂ)
125 subcl 10131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
126123, 124, 125sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − 𝑠) ∈ ℂ)
127 simpll 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
128126, 127mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) ∈ ℂ)
129 simplr 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
130124, 129mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑠 · (𝑏𝑖)) ∈ ℂ)
131122, 128, 130adddid 9920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))))
132131oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
133 subcl 10131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
134123, 122, 133sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
135134, 127mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) ∈ ℂ)
136122, 128mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) ∈ ℂ)
137122, 130mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) ∈ ℂ)
138135, 136, 137addassd 9918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))))
139122, 126mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
140134, 139, 127adddird 9921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))))
141 simp2 1054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
142 subdi 10314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑡 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
143123, 142mp3an2 1403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
144121, 141, 143syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
145121mulid1d 9913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 1) = (𝑡 / 𝑠))
146 divcan1 10543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
147145, 146oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
148144, 147eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
149148oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)))
150 simp1 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑡 ∈ ℂ)
151 npncan 10153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
152123, 151mp3an1 1402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
153121, 150, 152syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
154149, 153eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
155154adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
156155oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍𝑖)) = ((1 − 𝑡) · (𝑍𝑖)))
157122, 126, 127mulassd 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖)) = ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖))))
158157oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))))
159140, 156, 1583eqtr3rd 2652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) = ((1 − 𝑡) · (𝑍𝑖)))
160122, 124, 129mulassd 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))))
161146adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
162161oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏𝑖)) = (𝑡 · (𝑏𝑖)))
163160, 162eqtr3d 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖))) = (𝑡 · (𝑏𝑖)))
164159, 163oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏𝑖)))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))
165132, 138, 1643eqtr2rd 2650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
166102, 105, 108, 111, 120, 165syl23anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
167166ralrimiva 2948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
168 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑡 / 𝑠) → (1 − 𝑟) = (1 − (𝑡 / 𝑠)))
169168oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑡 / 𝑠)) · (𝑍𝑖)))
170 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑡 / 𝑠) → (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) = ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
171169, 170oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑡 / 𝑠) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
172171eqeq2d 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑡 / 𝑠) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
173172ralbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑡 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
174173rspcev 3281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑡 / 𝑠) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
17599, 167, 174syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡𝑠) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
176175ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡𝑠 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
17782simp2bi 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
17881, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑠)
179 divelunit 12141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑠 ∈ ℝ ∧ 0 ≤ 𝑠) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
18084, 178, 80, 94, 179syl22anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠𝑡))
181180biimpar 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → (𝑠 / 𝑡) ∈ (0[,]1))
182 simp112 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
183 simp3 1055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
184182, 183, 51syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
185 simp113 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
186185, 183, 55syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (𝑏𝑖) ∈ ℂ)
187 simp12r 1167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
188187, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
189 simp12l 1166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
190189, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
191 simp13 1085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
192 divcl 10540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (𝑠 / 𝑡) ∈ ℂ)
193192adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑠 / 𝑡) ∈ ℂ)
194 simpr2 1060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → 𝑡 ∈ ℂ)
195 subcl 10131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
196123, 194, 195sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − 𝑡) ∈ ℂ)
197 simpll 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑍𝑖) ∈ ℂ)
198196, 197mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
199 simplr 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑏𝑖) ∈ ℂ)
200194, 199mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑡 · (𝑏𝑖)) ∈ ℂ)
201193, 198, 200adddid 9920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))))
202201oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
203 subcl 10131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
204123, 193, 203sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
205204, 197mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) ∈ ℂ)
206193, 198mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) ∈ ℂ)
207193, 200mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) ∈ ℂ)
208205, 206, 207addassd 9918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))))
209 simp2 1054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
210 subdi 10314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑠 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
211123, 210mp3an2 1403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
212192, 209, 211syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
213192mulid1d 9913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 1) = (𝑠 / 𝑡))
214 divcan1 10543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 𝑡) = 𝑠)
215213, 214oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
216212, 215eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
217216oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)))
218 simp1 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
219 npncan 10153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
220123, 219mp3an1 1402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
221192, 218, 220syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
222217, 221eqtr2d 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑠) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))))
223222oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
224223adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑠) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)))
225193, 196mulcld 9916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
226204, 225, 197adddird 9921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍𝑖)) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))))
227193, 196, 197mulassd 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖)) = ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖))))
228227oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))))
229224, 226, 2283eqtrrd 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) = ((1 − 𝑠) · (𝑍𝑖)))
230193, 194, 199mulassd 9919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))))
231214oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
232231adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏𝑖)) = (𝑠 · (𝑏𝑖)))
233230, 232eqtr3d 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖))) = (𝑠 · (𝑏𝑖)))
234229, 233oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏𝑖)))) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))
235202, 208, 2343eqtr2rd 2650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑍𝑖) ∈ ℂ ∧ (𝑏𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
236184, 186, 188, 190, 191, 235syl23anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
2372363expa 1256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
238237ralrimiva 2948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
239 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑟 = (𝑠 / 𝑡) → (1 − 𝑟) = (1 − (𝑠 / 𝑡)))
240239oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → ((1 − 𝑟) · (𝑍𝑖)) = ((1 − (𝑠 / 𝑡)) · (𝑍𝑖)))
241 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟 = (𝑠 / 𝑡) → (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))) = ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
242240, 241oveq12d 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑠 / 𝑡) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
243242eqeq2d 2619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 = (𝑠 / 𝑡) → ((((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
244243ralbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑠 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
245244rspcev 3281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑠 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
246181, 238, 245syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠𝑡) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
247246ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑠𝑡 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
248176, 247orim12d 878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡𝑠𝑠𝑡) → (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
249 r19.43 3073 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (𝑟 · (𝑝𝑖)) = (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
254253oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
255252, 254eqeqan12d 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
256255ralimi 2935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ↔ (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))))
257 ralbi 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (𝑟 · (𝑈𝑖)) = (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
261260oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) → (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))
262259, 261eqeqan12rd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
263262ralimi 2935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))) ↔ (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))))
264 ralbi 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ((∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
267266rexbidv 3033 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))))))))
268251, 267syl5ibrcom 235 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
2692683expia 1258 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑡 ≠ 0 → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
270269com23 83 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
27174, 270sylan 486 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))))
272271imp 443 . . . . . . . . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
275274rexlimdvva 3019 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
276 simp3l 1081 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑈 ∈ (𝔼‘𝑁))
277 brbtwn 25497 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
278276, 73, 53, 277syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖)))))
279 simp3r 1082 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑝 ∈ (𝔼‘𝑁))
280 brbtwn 25497 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
281279, 73, 53, 280syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
282278, 281anbi12d 742 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
283 r19.26 3045 . . . . . . . . . . . . . . . . . . . 20 (∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
2842832rexbii 3023 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
285 reeanv 3085 . . . . . . . . . . . . . . . . . . 19 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
286284, 285bitri 262 . . . . . . . . . . . . . . . . . 18 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖)))))
287282, 286syl6bbr 276 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑏𝑖))) ∧ (𝑝𝑖) = (((1 − 𝑠) · (𝑍𝑖)) + (𝑠 · (𝑏𝑖))))))
288 brbtwn 25497 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
289276, 73, 279, 288syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖)))))
290 brbtwn 25497 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
291279, 73, 276, 290syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
292289, 291orbi12d 741 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
293 r19.43 3073 . . . . . . . . . . . . . . . . . 18 (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖)))))
294292, 293syl6bbr 276 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑝𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝𝑖) = (((1 − 𝑟) · (𝑍𝑖)) + (𝑟 · (𝑈𝑖))))))
295275, 287, 2943imtr4d 281 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2962953expia 1258 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
297296impd 445 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
29831, 297sylanl2 680 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
2992983adantr2 1213 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
300299adantr 479 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
30130, 300mpd 15 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) ∧ 𝑝𝐴) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
302301ralrimiva 2948 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
3033023exp2 1276 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))))
30411, 303syl6 34 . . . . . . 7 (𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
305304exlimiv 1844 . . . . . 6 (∃𝑏 𝑏𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3062, 305sylbi 205 . . . . 5 (𝐵 ≠ ∅ → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
307306com4l 89 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈𝐴 → (𝐵 ≠ ∅ → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
3083073impd 1272 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) → (𝑍𝑈 → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
309308imp32 447 . 2 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
310 axcontlem4.1 . . . 4 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
311310sseq2i 3592 . . 3 (𝐴𝐷𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)})
312 ssrab 3642 . . 3 (𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
313311, 312bitri 262 . 2 (𝐴𝐷 ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
3141, 309, 313sylanbrc 694 1 (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥𝐴𝑦𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈𝐴𝐵 ≠ ∅) ∧ 𝑍𝑈)) → 𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  wne 2779  wral 2895  wrex 2896  {crab 2899  wss 3539  c0 3873  cop 4130   class class class wbr 4577  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  cmin 10117   / cdiv 10533  cn 10867  [,]cicc 12005  ...cfz 12152  𝔼cee 25486   Btwn cbtwn 25487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-map 7723  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-z 11211  df-uz 11520  df-icc 12009  df-fz 12153  df-ee 25489  df-btwn 25490
This theorem is referenced by:  axcontlem9  25570  axcontlem10  25571
  Copyright terms: Public domain W3C validator