# Metamath Proof Explorer

## Theorem axcontlem4

Description: Lemma for axcont . Given the separation assumption, A is a subset of D . (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypothesis axcontlem4.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
Assertion axcontlem4 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\wedge \left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\to {A}\subseteq {D}$

### Proof

Step Hyp Ref Expression
1 axcontlem4.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
2 simplr1 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\wedge \left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\to {A}\subseteq 𝔼\left({N}\right)$
3 n0 ${⊢}{B}\ne \varnothing ↔\exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {B}$
4 idd ${⊢}{b}\in {B}\to \left({A}\subseteq 𝔼\left({N}\right)\to {A}\subseteq 𝔼\left({N}\right)\right)$
5 ssel ${⊢}{B}\subseteq 𝔼\left({N}\right)\to \left({b}\in {B}\to {b}\in 𝔼\left({N}\right)\right)$
6 5 com12 ${⊢}{b}\in {B}\to \left({B}\subseteq 𝔼\left({N}\right)\to {b}\in 𝔼\left({N}\right)\right)$
7 opeq2 ${⊢}{y}={b}\to ⟨{Z},{y}⟩=⟨{Z},{b}⟩$
8 7 breq2d ${⊢}{y}={b}\to \left({x}\mathrm{Btwn}⟨{Z},{y}⟩↔{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
9 8 rspcv ${⊢}{b}\in {B}\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\to {x}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
10 9 ralimdv ${⊢}{b}\in {B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
11 4 6 10 3anim123d ${⊢}{b}\in {B}\to \left(\left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\to \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)$
12 11 anim2d ${⊢}{b}\in {B}\to \left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\to \left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\right)$
13 simplr1 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to {A}\subseteq 𝔼\left({N}\right)$
14 13 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to {A}\subseteq 𝔼\left({N}\right)$
15 simplr2 ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to {U}\in {A}$
16 14 15 sseldd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to {U}\in 𝔼\left({N}\right)$
17 simpr3 ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩$
18 simp2 ${⊢}\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\to {U}\in {A}$
19 breq1 ${⊢}{x}={U}\to \left({x}\mathrm{Btwn}⟨{Z},{b}⟩↔{U}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
20 19 rspccva ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {U}\in {A}\right)\to {U}\mathrm{Btwn}⟨{Z},{b}⟩$
21 17 18 20 syl2an ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to {U}\mathrm{Btwn}⟨{Z},{b}⟩$
22 21 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to {U}\mathrm{Btwn}⟨{Z},{b}⟩$
23 16 22 jca ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to \left({U}\in 𝔼\left({N}\right)\wedge {U}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
24 13 sselda ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to {p}\in 𝔼\left({N}\right)$
25 17 adantr ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩$
26 breq1 ${⊢}{x}={p}\to \left({x}\mathrm{Btwn}⟨{Z},{b}⟩↔{p}\mathrm{Btwn}⟨{Z},{b}⟩\right)$
27 26 rspccva ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\in {A}\right)\to {p}\mathrm{Btwn}⟨{Z},{b}⟩$
28 25 27 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to {p}\mathrm{Btwn}⟨{Z},{b}⟩$
29 23 24 28 jca32 ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to \left(\left({U}\in 𝔼\left({N}\right)\wedge {U}\mathrm{Btwn}⟨{Z},{b}⟩\right)\wedge \left({p}\in 𝔼\left({N}\right)\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)$
30 an4 ${⊢}\left(\left({U}\in 𝔼\left({N}\right)\wedge {U}\mathrm{Btwn}⟨{Z},{b}⟩\right)\wedge \left({p}\in 𝔼\left({N}\right)\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)↔\left(\left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)$
31 29 30 sylib ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to \left(\left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)$
32 simp2 ${⊢}\left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\to {b}\in 𝔼\left({N}\right)$
33 simpl2r ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to {Z}\ne {U}$
34 33 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to {Z}\ne {U}$
35 simpl ${⊢}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to {U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)$
36 35 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)$
37 eqcom ${⊢}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)↔\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)={U}\left({i}\right)$
38 oveq2 ${⊢}{t}=0\to 1-{t}=1-0$
39 1m0e1 ${⊢}1-0=1$
40 38 39 syl6eq ${⊢}{t}=0\to 1-{t}=1$
41 40 oveq1d ${⊢}{t}=0\to \left(1-{t}\right){Z}\left({i}\right)=1{Z}\left({i}\right)$
42 oveq1 ${⊢}{t}=0\to {t}{b}\left({i}\right)=0\cdot {b}\left({i}\right)$
43 41 42 oveq12d ${⊢}{t}=0\to \left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)$
44 43 eqeq1d ${⊢}{t}=0\to \left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)={U}\left({i}\right)↔1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={U}\left({i}\right)\right)$
45 37 44 syl5bb ${⊢}{t}=0\to \left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)↔1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={U}\left({i}\right)\right)$
46 45 ralbidv ${⊢}{t}=0\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={U}\left({i}\right)\right)$
47 46 biimpac ${⊢}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {t}=0\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={U}\left({i}\right)$
48 simpl2l ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to {Z}\in 𝔼\left({N}\right)$
49 simpl3l ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to {U}\in 𝔼\left({N}\right)$
50 eqeefv ${⊢}\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\to \left({Z}={U}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)$
51 48 49 50 syl2anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left({Z}={U}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)$
52 fveecn ${⊢}\left({Z}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
53 48 52 sylan ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
54 simp1r ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to {b}\in 𝔼\left({N}\right)$
55 54 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {b}\in 𝔼\left({N}\right)$
56 fveecn ${⊢}\left({b}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {b}\left({i}\right)\in ℂ$
57 55 56 sylancom ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {b}\left({i}\right)\in ℂ$
58 mulid2 ${⊢}{Z}\left({i}\right)\in ℂ\to 1{Z}\left({i}\right)={Z}\left({i}\right)$
59 mul02 ${⊢}{b}\left({i}\right)\in ℂ\to 0\cdot {b}\left({i}\right)=0$
60 58 59 oveqan12d ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\to 1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={Z}\left({i}\right)+0$
61 addid1 ${⊢}{Z}\left({i}\right)\in ℂ\to {Z}\left({i}\right)+0={Z}\left({i}\right)$
62 61 adantr ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\to {Z}\left({i}\right)+0={Z}\left({i}\right)$
63 60 62 eqtrd ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\to 1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={Z}\left({i}\right)$
64 53 57 63 syl2anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={Z}\left({i}\right)$
65 64 eqeq1d ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={U}\left({i}\right)↔{Z}\left({i}\right)={U}\left({i}\right)\right)$
66 65 ralbidva ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)$
67 51 66 bitr4d ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left({Z}={U}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}1{Z}\left({i}\right)+0\cdot {b}\left({i}\right)={U}\left({i}\right)\right)$
68 47 67 syl5ibr ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {t}=0\right)\to {Z}={U}\right)$
69 68 expdimp ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\to \left({t}=0\to {Z}={U}\right)$
70 36 69 sylan2 ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to \left({t}=0\to {Z}={U}\right)$
71 70 necon3d ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to \left({Z}\ne {U}\to {t}\ne 0\right)$
72 34 71 mpd ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to {t}\ne 0$
73 simp1l ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
74 simp2l ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to {Z}\in 𝔼\left({N}\right)$
75 73 74 54 3jca ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)$
76 simp2l ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {t}\in \left[0,1\right]$
77 elicc01 ${⊢}{t}\in \left[0,1\right]↔\left({t}\in ℝ\wedge 0\le {t}\wedge {t}\le 1\right)$
78 77 simp1bi ${⊢}{t}\in \left[0,1\right]\to {t}\in ℝ$
79 76 78 syl ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {t}\in ℝ$
80 simp2r ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {s}\in \left[0,1\right]$
81 elicc01 ${⊢}{s}\in \left[0,1\right]↔\left({s}\in ℝ\wedge 0\le {s}\wedge {s}\le 1\right)$
82 81 simp1bi ${⊢}{s}\in \left[0,1\right]\to {s}\in ℝ$
83 80 82 syl ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {s}\in ℝ$
84 79 83 letrid ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \left({t}\le {s}\vee {s}\le {t}\right)$
85 simpr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to {t}\le {s}$
86 79 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to {t}\in ℝ$
87 77 simp2bi ${⊢}{t}\in \left[0,1\right]\to 0\le {t}$
88 76 87 syl ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to 0\le {t}$
89 88 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to 0\le {t}$
90 83 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to {s}\in ℝ$
91 0red ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to 0\in ℝ$
92 simp3 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {t}\ne 0$
93 79 88 92 ne0gt0d ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to 0<{t}$
94 93 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to 0<{t}$
95 91 86 90 94 85 ltletrd ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to 0<{s}$
96 divelunit ${⊢}\left(\left({t}\in ℝ\wedge 0\le {t}\right)\wedge \left({s}\in ℝ\wedge 0<{s}\right)\right)\to \left(\frac{{t}}{{s}}\in \left[0,1\right]↔{t}\le {s}\right)$
97 86 89 90 95 96 syl22anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to \left(\frac{{t}}{{s}}\in \left[0,1\right]↔{t}\le {s}\right)$
98 85 97 mpbird ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to \frac{{t}}{{s}}\in \left[0,1\right]$
99 simp12 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {Z}\in 𝔼\left({N}\right)$
100 99 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
101 100 52 sylancom ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
102 simp13 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {b}\in 𝔼\left({N}\right)$
103 102 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {b}\in 𝔼\left({N}\right)$
104 103 56 sylancom ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {b}\left({i}\right)\in ℂ$
105 78 recnd ${⊢}{t}\in \left[0,1\right]\to {t}\in ℂ$
106 76 105 syl ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {t}\in ℂ$
107 106 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in ℂ$
108 82 recnd ${⊢}{s}\in \left[0,1\right]\to {s}\in ℂ$
109 80 108 syl ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to {s}\in ℂ$
110 109 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in ℂ$
111 0red ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0\in ℝ$
112 79 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in ℝ$
113 83 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in ℝ$
114 88 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0\le {t}$
115 simpll3 ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\ne 0$
116 112 114 115 ne0gt0d ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0<{t}$
117 simplr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\le {s}$
118 111 112 113 116 117 ltletrd ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 0<{s}$
119 118 gt0ne0d ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\ne 0$
120 divcl ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to \frac{{t}}{{s}}\in ℂ$
121 120 adantl ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \frac{{t}}{{s}}\in ℂ$
122 ax-1cn ${⊢}1\in ℂ$
123 simpr2 ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to {s}\in ℂ$
124 subcl ${⊢}\left(1\in ℂ\wedge {s}\in ℂ\right)\to 1-{s}\in ℂ$
125 122 123 124 sylancr ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to 1-{s}\in ℂ$
126 simpll ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to {Z}\left({i}\right)\in ℂ$
127 125 126 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-{s}\right){Z}\left({i}\right)\in ℂ$
128 simplr ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to {b}\left({i}\right)\in ℂ$
129 123 128 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to {s}{b}\left({i}\right)\in ℂ$
130 121 127 129 adddid ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)=\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)$
131 130 oveq2d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)$
132 subcl ${⊢}\left(1\in ℂ\wedge \frac{{t}}{{s}}\in ℂ\right)\to 1-\left(\frac{{t}}{{s}}\right)\in ℂ$
133 122 121 132 sylancr ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to 1-\left(\frac{{t}}{{s}}\right)\in ℂ$
134 133 126 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)\in ℂ$
135 121 127 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)\in ℂ$
136 121 129 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)\in ℂ$
137 134 135 136 addassd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)$
138 121 125 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right)\left(1-{s}\right)\in ℂ$
139 133 138 126 adddird ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right)\right){Z}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)$
140 simp2 ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to {s}\in ℂ$
141 subdi ${⊢}\left(\frac{{t}}{{s}}\in ℂ\wedge 1\in ℂ\wedge {s}\in ℂ\right)\to \left(\frac{{t}}{{s}}\right)\left(1-{s}\right)=\left(\frac{{t}}{{s}}\right)\cdot 1-\left(\frac{{t}}{{s}}\right){s}$
142 122 141 mp3an2 ${⊢}\left(\frac{{t}}{{s}}\in ℂ\wedge {s}\in ℂ\right)\to \left(\frac{{t}}{{s}}\right)\left(1-{s}\right)=\left(\frac{{t}}{{s}}\right)\cdot 1-\left(\frac{{t}}{{s}}\right){s}$
143 120 140 142 syl2anc ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{{t}}{{s}}\right)\left(1-{s}\right)=\left(\frac{{t}}{{s}}\right)\cdot 1-\left(\frac{{t}}{{s}}\right){s}$
144 120 mulid1d ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{{t}}{{s}}\right)\cdot 1=\frac{{t}}{{s}}$
145 divcan1 ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{{t}}{{s}}\right){s}={t}$
146 144 145 oveq12d ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{{t}}{{s}}\right)\cdot 1-\left(\frac{{t}}{{s}}\right){s}=\left(\frac{{t}}{{s}}\right)-{t}$
147 143 146 eqtrd ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{{t}}{{s}}\right)\left(1-{s}\right)=\left(\frac{{t}}{{s}}\right)-{t}$
148 147 oveq2d ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to 1-\left(\frac{{t}}{{s}}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right)+\left(\frac{{t}}{{s}}\right)-{t}$
149 simp1 ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to {t}\in ℂ$
150 npncan ${⊢}\left(1\in ℂ\wedge \frac{{t}}{{s}}\in ℂ\wedge {t}\in ℂ\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right)+\left(\frac{{t}}{{s}}\right)-{t}=1-{t}$
151 122 120 149 150 mp3an2i ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right)+\left(\frac{{t}}{{s}}\right)-{t}=1-{t}$
152 148 151 eqtrd ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\to 1-\left(\frac{{t}}{{s}}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right)=1-{t}$
153 152 adantl ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to 1-\left(\frac{{t}}{{s}}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right)=1-{t}$
154 153 oveq1d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right)\right){Z}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)$
155 121 125 126 mulassd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)=\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)$
156 155 oveq2d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)$
157 139 154 156 3eqtr3rd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)$
158 121 123 128 mulassd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)=\left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)$
159 145 adantl ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right){s}={t}$
160 159 oveq1d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)={t}{b}\left({i}\right)$
161 158 160 eqtr3d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)={t}{b}\left({i}\right)$
162 157 161 oveq12d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right){s}{b}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)$
163 131 137 162 3eqtr2rd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\wedge {s}\ne 0\right)\right)\to \left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
164 101 104 107 110 119 163 syl23anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
165 164 ralrimiva ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
166 oveq2 ${⊢}{r}=\frac{{t}}{{s}}\to 1-{r}=1-\left(\frac{{t}}{{s}}\right)$
167 166 oveq1d ${⊢}{r}=\frac{{t}}{{s}}\to \left(1-{r}\right){Z}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)$
168 oveq1 ${⊢}{r}=\frac{{t}}{{s}}\to {r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)=\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
169 167 168 oveq12d ${⊢}{r}=\frac{{t}}{{s}}\to \left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
170 169 eqeq2d ${⊢}{r}=\frac{{t}}{{s}}\to \left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)↔\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
171 170 ralbidv ${⊢}{r}=\frac{{t}}{{s}}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
172 171 rspcev ${⊢}\left(\frac{{t}}{{s}}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-\left(\frac{{t}}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{{t}}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
173 98 165 172 syl2anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {t}\le {s}\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
174 173 ex ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \left({t}\le {s}\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
175 81 simp2bi ${⊢}{s}\in \left[0,1\right]\to 0\le {s}$
176 80 175 syl ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to 0\le {s}$
177 divelunit ${⊢}\left(\left({s}\in ℝ\wedge 0\le {s}\right)\wedge \left({t}\in ℝ\wedge 0<{t}\right)\right)\to \left(\frac{{s}}{{t}}\in \left[0,1\right]↔{s}\le {t}\right)$
178 83 176 79 93 177 syl22anc ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \left(\frac{{s}}{{t}}\in \left[0,1\right]↔{s}\le {t}\right)$
179 178 biimpar ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\right)\to \frac{{s}}{{t}}\in \left[0,1\right]$
180 simp112 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
181 simp3 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {i}\in \left(1\dots {N}\right)$
182 180 181 52 syl2anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
183 simp113 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {b}\in 𝔼\left({N}\right)$
184 183 181 56 syl2anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {b}\left({i}\right)\in ℂ$
185 simp12r ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in \left[0,1\right]$
186 185 108 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in ℂ$
187 simp12l ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in \left[0,1\right]$
188 187 105 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in ℂ$
189 simp13 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\ne 0$
190 divcl ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \frac{{s}}{{t}}\in ℂ$
191 190 adantl ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \frac{{s}}{{t}}\in ℂ$
192 simpr2 ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to {t}\in ℂ$
193 subcl ${⊢}\left(1\in ℂ\wedge {t}\in ℂ\right)\to 1-{t}\in ℂ$
194 122 192 193 sylancr ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to 1-{t}\in ℂ$
195 simpll ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to {Z}\left({i}\right)\in ℂ$
196 194 195 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-{t}\right){Z}\left({i}\right)\in ℂ$
197 simplr ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to {b}\left({i}\right)\in ℂ$
198 192 197 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to {t}{b}\left({i}\right)\in ℂ$
199 191 196 198 adddid ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)=\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)$
200 199 oveq2d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)$
201 subcl ${⊢}\left(1\in ℂ\wedge \frac{{s}}{{t}}\in ℂ\right)\to 1-\left(\frac{{s}}{{t}}\right)\in ℂ$
202 122 191 201 sylancr ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to 1-\left(\frac{{s}}{{t}}\right)\in ℂ$
203 202 195 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)\in ℂ$
204 191 196 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)\in ℂ$
205 191 198 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)\in ℂ$
206 203 204 205 addassd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)$
207 simp2 ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to {t}\in ℂ$
208 subdi ${⊢}\left(\frac{{s}}{{t}}\in ℂ\wedge 1\in ℂ\wedge {t}\in ℂ\right)\to \left(\frac{{s}}{{t}}\right)\left(1-{t}\right)=\left(\frac{{s}}{{t}}\right)\cdot 1-\left(\frac{{s}}{{t}}\right){t}$
209 122 208 mp3an2 ${⊢}\left(\frac{{s}}{{t}}\in ℂ\wedge {t}\in ℂ\right)\to \left(\frac{{s}}{{t}}\right)\left(1-{t}\right)=\left(\frac{{s}}{{t}}\right)\cdot 1-\left(\frac{{s}}{{t}}\right){t}$
210 190 207 209 syl2anc ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{{s}}{{t}}\right)\left(1-{t}\right)=\left(\frac{{s}}{{t}}\right)\cdot 1-\left(\frac{{s}}{{t}}\right){t}$
211 190 mulid1d ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{{s}}{{t}}\right)\cdot 1=\frac{{s}}{{t}}$
212 divcan1 ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{{s}}{{t}}\right){t}={s}$
213 211 212 oveq12d ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{{s}}{{t}}\right)\cdot 1-\left(\frac{{s}}{{t}}\right){t}=\left(\frac{{s}}{{t}}\right)-{s}$
214 210 213 eqtrd ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{{s}}{{t}}\right)\left(1-{t}\right)=\left(\frac{{s}}{{t}}\right)-{s}$
215 214 oveq2d ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to 1-\left(\frac{{s}}{{t}}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right)+\left(\frac{{s}}{{t}}\right)-{s}$
216 simp1 ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to {s}\in ℂ$
217 npncan ${⊢}\left(1\in ℂ\wedge \frac{{s}}{{t}}\in ℂ\wedge {s}\in ℂ\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right)+\left(\frac{{s}}{{t}}\right)-{s}=1-{s}$
218 122 190 216 217 mp3an2i ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right)+\left(\frac{{s}}{{t}}\right)-{s}=1-{s}$
219 215 218 eqtr2d ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to 1-{s}=1-\left(\frac{{s}}{{t}}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right)$
220 219 oveq1d ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(1-{s}\right){Z}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right)\right){Z}\left({i}\right)$
221 220 adantl ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-{s}\right){Z}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right)\right){Z}\left({i}\right)$
222 191 194 mulcld ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right)\left(1-{t}\right)\in ℂ$
223 202 222 195 adddird ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-\left(\frac{{s}}{{t}}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right)\right){Z}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)$
224 191 194 195 mulassd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)=\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)$
225 224 oveq2d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)$
226 221 223 225 3eqtrrd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)$
227 191 192 197 mulassd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)=\left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)$
228 212 oveq1d ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)={s}{b}\left({i}\right)$
229 228 adantl ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)={s}{b}\left({i}\right)$
230 227 229 eqtr3d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)={s}{b}\left({i}\right)$
231 226 230 oveq12d ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right){t}{b}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)$
232 200 206 231 3eqtr2rd ${⊢}\left(\left({Z}\left({i}\right)\in ℂ\wedge {b}\left({i}\right)\in ℂ\right)\wedge \left({s}\in ℂ\wedge {t}\in ℂ\wedge {t}\ne 0\right)\right)\to \left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
233 182 184 186 188 189 232 syl23anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
234 233 3expa ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
235 234 ralrimiva ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
236 oveq2 ${⊢}{r}=\frac{{s}}{{t}}\to 1-{r}=1-\left(\frac{{s}}{{t}}\right)$
237 236 oveq1d ${⊢}{r}=\frac{{s}}{{t}}\to \left(1-{r}\right){Z}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)$
238 oveq1 ${⊢}{r}=\frac{{s}}{{t}}\to {r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)=\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
239 237 238 oveq12d ${⊢}{r}=\frac{{s}}{{t}}\to \left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
240 239 eqeq2d ${⊢}{r}=\frac{{s}}{{t}}\to \left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)↔\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
241 240 ralbidv ${⊢}{r}=\frac{{s}}{{t}}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
242 241 rspcev ${⊢}\left(\frac{{s}}{{t}}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-\left(\frac{{s}}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{{s}}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
243 179 235 242 syl2anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\wedge {s}\le {t}\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
244 243 ex ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \left({s}\le {t}\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
245 174 244 orim12d ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \left(\left({t}\le {s}\vee {s}\le {t}\right)\to \left(\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\vee \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)\right)$
246 r19.43 ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)↔\left(\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\vee \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
247 245 246 syl6ibr ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \left(\left({t}\le {s}\vee {s}\le {t}\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)\right)$
248 84 247 mpd ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
249 id ${⊢}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\to {U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)$
250 oveq2 ${⊢}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\to {r}{p}\left({i}\right)={r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
251 250 oveq2d ${⊢}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\to \left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
252 249 251 eqeqan12d ${⊢}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left({U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)↔\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
253 252 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)↔\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
254 ralbi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)↔\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
255 253 254 syl ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
256 id ${⊢}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\to {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)$
257 oveq2 ${⊢}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\to {r}{U}\left({i}\right)={r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
258 257 oveq2d ${⊢}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\to \left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
259 256 258 eqeqan12rd ${⊢}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left({p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)↔\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
260 259 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)↔\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
261 ralbi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)↔\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
262 260 261 syl ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)$
263 255 262 orbi12d ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)↔\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)\right)$
264 263 rexbidv ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left(\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)\right)\right)$
265 248 264 syl5ibrcom ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\wedge {t}\ne 0\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)$
266 265 3expia ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left({t}\ne 0\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)\right)$
267 266 com23 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left({t}\ne 0\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)\right)$
268 75 267 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \left({t}\ne 0\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)\right)$
269 268 imp ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to \left({t}\ne 0\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)$
270 72 269 mpd ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)$
271 270 ex ${⊢}\left(\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)$
272 271 rexlimdvva ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)$
273 simp3l ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to {U}\in 𝔼\left({N}\right)$
274 brbtwn ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{b}⟩↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
275 273 74 54 274 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{b}⟩↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\right)$
276 simp3r ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to {p}\in 𝔼\left({N}\right)$
277 brbtwn ${⊢}\left({p}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\right)\to \left({p}\mathrm{Btwn}⟨{Z},{b}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
278 276 74 54 277 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left({p}\mathrm{Btwn}⟨{Z},{b}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
279 275 278 anbi12d ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)↔\left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
280 r19.26 ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)↔\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
281 280 2rexbii ${⊢}\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
282 reeanv ${⊢}\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)↔\left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
283 281 282 bitri ${⊢}\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)↔\left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)$
284 279 283 syl6bbr ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{b}\left({i}\right)\wedge {p}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{b}\left({i}\right)\right)\right)$
285 brbtwn ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\right)$
286 273 74 276 285 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\right)$
287 brbtwn ${⊢}\left({p}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\to \left({p}\mathrm{Btwn}⟨{Z},{U}⟩↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)$
288 276 74 273 287 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left({p}\mathrm{Btwn}⟨{Z},{U}⟩↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)$
289 286 288 orbi12d ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)↔\left(\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)$
290 r19.43 ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)↔\left(\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)$
291 289 290 syl6bbr ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{p}\left({i}\right)\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)=\left(1-{r}\right){Z}\left({i}\right)+{r}{U}\left({i}\right)\right)\right)$
292 272 284 291 3imtr4d ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\wedge \left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
293 292 3expia ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\right)\to \left(\left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\to \left(\left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)$
294 293 impd ${⊢}\left(\left({N}\in ℕ\wedge {b}\in 𝔼\left({N}\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\right)\to \left(\left(\left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
295 32 294 sylanl2 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {Z}\ne {U}\right)\right)\to \left(\left(\left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
296 295 3adantr2 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to \left(\left(\left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
297 296 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to \left(\left(\left({U}\in 𝔼\left({N}\right)\wedge {p}\in 𝔼\left({N}\right)\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{b}⟩\wedge {p}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
298 31 297 mpd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\wedge {p}\in {A}\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)$
299 298 ralrimiva ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\wedge \left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {Z}\ne {U}\right)\right)\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)$
300 299 3exp2 ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{b}⟩\right)\right)\to \left({Z}\in 𝔼\left({N}\right)\to \left({U}\in {A}\to \left({Z}\ne {U}\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)\right)$
301 12 300 syl6 ${⊢}{b}\in {B}\to \left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\to \left({Z}\in 𝔼\left({N}\right)\to \left({U}\in {A}\to \left({Z}\ne {U}\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)\right)\right)$
302 301 exlimiv ${⊢}\exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {B}\to \left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\to \left({Z}\in 𝔼\left({N}\right)\to \left({U}\in {A}\to \left({Z}\ne {U}\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)\right)\right)$
303 3 302 sylbi ${⊢}{B}\ne \varnothing \to \left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\to \left({Z}\in 𝔼\left({N}\right)\to \left({U}\in {A}\to \left({Z}\ne {U}\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)\right)\right)$
304 303 com4l ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\to \left({Z}\in 𝔼\left({N}\right)\to \left({U}\in {A}\to \left({B}\ne \varnothing \to \left({Z}\ne {U}\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)\right)\right)$
305 304 3impd ${⊢}\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\to \left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\to \left({Z}\ne {U}\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)$
306 305 imp32 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\wedge \left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)$
307 1 sseq2i ${⊢}{A}\subseteq {D}↔{A}\subseteq \left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
308 ssrab ${⊢}{A}\subseteq \left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}↔\left({A}\subseteq 𝔼\left({N}\right)\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
309 307 308 bitri ${⊢}{A}\subseteq {D}↔\left({A}\subseteq 𝔼\left({N}\right)\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
310 2 306 309 sylanbrc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\subseteq 𝔼\left({N}\right)\wedge {B}\subseteq 𝔼\left({N}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\mathrm{Btwn}⟨{Z},{y}⟩\right)\right)\wedge \left(\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in {A}\wedge {B}\ne \varnothing \right)\wedge {Z}\ne {U}\right)\right)\to {A}\subseteq {D}$