Metamath Proof Explorer

Theorem axpasch

Description: The inner Pasch axiom. Take a triangle A C E , a point D on A C , and a point B extending C E . Then A E and D B intersect at some point x . Axiom A7 of Schwabhauser p. 12. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axpasch ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({D}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{B},{C}⟩\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{Btwn}⟨{D},{B}⟩\wedge {x}\mathrm{Btwn}⟨{E},{A}⟩\right)\right)$

Proof

Step Hyp Ref Expression
1 axpaschlem ${⊢}\left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)$
2 1 3ad2ant3 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)$
3 simp1 ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to {q}=\left(1-{r}\right)\left(1-{t}\right)$
4 3 oveq1d ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to {q}{A}\left({i}\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)$
5 4 eqcomd ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)={q}{A}\left({i}\right)$
6 simp2 ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to {r}=\left(1-{q}\right)\left(1-{s}\right)$
7 6 oveq1d ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to {r}{B}\left({i}\right)=\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)$
8 5 7 oveq12d ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+{r}{B}\left({i}\right)={q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)$
9 simp3 ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to \left(1-{r}\right){t}=\left(1-{q}\right){s}$
10 9 oveq1d ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to \left(1-{r}\right){t}{C}\left({i}\right)=\left(1-{q}\right){s}{C}\left({i}\right)$
11 8 10 oveq12d ${⊢}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+{r}{B}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)={q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)$
12 11 3ad2ant3 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+{r}{B}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)={q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)$
13 12 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+{r}{B}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)={q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)$
14 1re ${⊢}1\in ℝ$
15 simpl2l ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {r}\in \left[0,1\right]$
16 elicc01 ${⊢}{r}\in \left[0,1\right]↔\left({r}\in ℝ\wedge 0\le {r}\wedge {r}\le 1\right)$
17 16 simp1bi ${⊢}{r}\in \left[0,1\right]\to {r}\in ℝ$
18 15 17 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {r}\in ℝ$
19 resubcl ${⊢}\left(1\in ℝ\wedge {r}\in ℝ\right)\to 1-{r}\in ℝ$
20 14 18 19 sylancr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{r}\in ℝ$
21 20 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{r}\in ℂ$
22 simp13l ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\to {t}\in \left[0,1\right]$
23 22 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in \left[0,1\right]$
24 elicc01 ${⊢}{t}\in \left[0,1\right]↔\left({t}\in ℝ\wedge 0\le {t}\wedge {t}\le 1\right)$
25 24 simp1bi ${⊢}{t}\in \left[0,1\right]\to {t}\in ℝ$
26 23 25 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in ℝ$
27 resubcl ${⊢}\left(1\in ℝ\wedge {t}\in ℝ\right)\to 1-{t}\in ℝ$
28 14 26 27 sylancr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{t}\in ℝ$
29 simp121 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\to {A}\in 𝔼\left({N}\right)$
30 fveere ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {A}\left({i}\right)\in ℝ$
31 29 30 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {A}\left({i}\right)\in ℝ$
32 28 31 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{t}\right){A}\left({i}\right)\in ℝ$
33 32 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{t}\right){A}\left({i}\right)\in ℂ$
34 simp123 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\to {C}\in 𝔼\left({N}\right)$
35 fveere ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {C}\left({i}\right)\in ℝ$
36 34 35 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {C}\left({i}\right)\in ℝ$
37 26 36 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}{C}\left({i}\right)\in ℝ$
38 37 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}{C}\left({i}\right)\in ℂ$
39 21 33 38 adddid ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)$
40 28 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{t}\in ℂ$
41 31 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {A}\left({i}\right)\in ℂ$
42 21 40 41 mulassd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)$
43 26 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in ℂ$
44 fveecn ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {C}\left({i}\right)\in ℂ$
45 34 44 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {C}\left({i}\right)\in ℂ$
46 21 43 45 mulassd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right){t}{C}\left({i}\right)=\left(1-{r}\right){t}{C}\left({i}\right)$
47 42 46 oveq12d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)$
48 39 47 eqtr4d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)$
49 48 oveq1d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)+{r}{B}\left({i}\right)$
50 20 28 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right)\in ℝ$
51 50 31 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)\in ℝ$
52 51 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)\in ℂ$
53 20 26 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right){t}\in ℝ$
54 53 36 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right){t}{C}\left({i}\right)\in ℝ$
55 54 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right){t}{C}\left({i}\right)\in ℂ$
56 simp122 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\to {B}\in 𝔼\left({N}\right)$
57 fveere ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {B}\left({i}\right)\in ℝ$
58 56 57 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {B}\left({i}\right)\in ℝ$
59 18 58 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {r}{B}\left({i}\right)\in ℝ$
60 59 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {r}{B}\left({i}\right)\in ℂ$
61 52 55 60 add32d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+{r}{B}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)$
62 49 61 eqtrd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(1-{t}\right){A}\left({i}\right)+{r}{B}\left({i}\right)+\left(1-{r}\right){t}{C}\left({i}\right)$
63 simpl2r ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {q}\in \left[0,1\right]$
64 elicc01 ${⊢}{q}\in \left[0,1\right]↔\left({q}\in ℝ\wedge 0\le {q}\wedge {q}\le 1\right)$
65 64 simp1bi ${⊢}{q}\in \left[0,1\right]\to {q}\in ℝ$
66 63 65 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {q}\in ℝ$
67 resubcl ${⊢}\left(1\in ℝ\wedge {q}\in ℝ\right)\to 1-{q}\in ℝ$
68 14 66 67 sylancr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{q}\in ℝ$
69 simp13r ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\to {s}\in \left[0,1\right]$
70 69 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in \left[0,1\right]$
71 elicc01 ${⊢}{s}\in \left[0,1\right]↔\left({s}\in ℝ\wedge 0\le {s}\wedge {s}\le 1\right)$
72 71 simp1bi ${⊢}{s}\in \left[0,1\right]\to {s}\in ℝ$
73 70 72 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in ℝ$
74 resubcl ${⊢}\left(1\in ℝ\wedge {s}\in ℝ\right)\to 1-{s}\in ℝ$
75 14 73 74 sylancr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{s}\in ℝ$
76 75 58 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{s}\right){B}\left({i}\right)\in ℝ$
77 68 76 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)\in ℝ$
78 77 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)\in ℂ$
79 73 36 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}{C}\left({i}\right)\in ℝ$
80 68 79 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right){s}{C}\left({i}\right)\in ℝ$
81 80 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right){s}{C}\left({i}\right)\in ℂ$
82 66 31 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {q}{A}\left({i}\right)\in ℝ$
83 82 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {q}{A}\left({i}\right)\in ℂ$
84 78 81 83 add32d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)+{q}{A}\left({i}\right)=\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+{q}{A}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)$
85 68 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{q}\in ℂ$
86 76 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{s}\right){B}\left({i}\right)\in ℂ$
87 79 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}{C}\left({i}\right)\in ℂ$
88 85 86 87 adddid ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)=\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)$
89 88 oveq1d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)=\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)+{q}{A}\left({i}\right)$
90 75 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to 1-{s}\in ℂ$
91 58 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {B}\left({i}\right)\in ℂ$
92 85 90 91 mulassd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)=\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)$
93 92 oveq2d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)={q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)$
94 83 78 93 comraddd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)=\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+{q}{A}\left({i}\right)$
95 73 recnd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in ℂ$
96 85 95 45 mulassd ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right){s}{C}\left({i}\right)=\left(1-{q}\right){s}{C}\left({i}\right)$
97 94 96 oveq12d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)=\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+{q}{A}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)$
98 84 89 97 3eqtr4d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)={q}{A}\left({i}\right)+\left(1-{q}\right)\left(1-{s}\right){B}\left({i}\right)+\left(1-{q}\right){s}{C}\left({i}\right)$
99 13 62 98 3eqtr4d ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)$
100 99 ralrimiva ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\wedge \left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)$
101 100 3expia ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\to \left(\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
102 101 reximdvva ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left(\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left({q}=\left(1-{r}\right)\left(1-{t}\right)\wedge {r}=\left(1-{q}\right)\left(1-{s}\right)\wedge \left(1-{r}\right){t}=\left(1-{q}\right){s}\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
103 2 102 mpd ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)$
104 simplrl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {r}\in \left[0,1\right]$
105 104 17 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {r}\in ℝ$
106 14 105 19 sylancr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to 1-{r}\in ℝ$
107 simpl3l ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\to {t}\in \left[0,1\right]$
108 107 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {t}\in \left[0,1\right]$
109 108 25 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {t}\in ℝ$
110 14 109 27 sylancr ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to 1-{t}\in ℝ$
111 simpl21 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\to {A}\in 𝔼\left({N}\right)$
112 fveere ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {A}\left({k}\right)\in ℝ$
113 111 112 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {A}\left({k}\right)\in ℝ$
114 110 113 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to \left(1-{t}\right){A}\left({k}\right)\in ℝ$
115 simpl23 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\to {C}\in 𝔼\left({N}\right)$
116 fveere ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {C}\left({k}\right)\in ℝ$
117 115 116 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {C}\left({k}\right)\in ℝ$
118 109 117 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {t}{C}\left({k}\right)\in ℝ$
119 114 118 readdcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to \left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\in ℝ$
120 106 119 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)\in ℝ$
121 simpl22 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\to {B}\in 𝔼\left({N}\right)$
122 fveere ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {B}\left({k}\right)\in ℝ$
123 121 122 sylan ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {B}\left({k}\right)\in ℝ$
124 105 123 remulcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {r}{B}\left({k}\right)\in ℝ$
125 120 124 readdcld ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\in ℝ$
126 125 ralrimiva ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge \left({r}\in \left[0,1\right]\wedge {q}\in \left[0,1\right]\right)\right)\to \forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\in ℝ$
127 126 anassrs ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {r}\in \left[0,1\right]\right)\wedge {q}\in \left[0,1\right]\right)\to \forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\in ℝ$
128 simpll1 ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {r}\in \left[0,1\right]\right)\wedge {q}\in \left[0,1\right]\right)\to {N}\in ℕ$
129 mptelee ${⊢}{N}\in ℕ\to \left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\in 𝔼\left({N}\right)↔\forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\in ℝ\right)$
130 128 129 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {r}\in \left[0,1\right]\right)\wedge {q}\in \left[0,1\right]\right)\to \left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\in 𝔼\left({N}\right)↔\forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\in ℝ\right)$
131 127 130 mpbird ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {r}\in \left[0,1\right]\right)\wedge {q}\in \left[0,1\right]\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\in 𝔼\left({N}\right)$
132 fveq1 ${⊢}{x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\to {x}\left({i}\right)=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\left({i}\right)$
133 fveq2 ${⊢}{k}={i}\to {A}\left({k}\right)={A}\left({i}\right)$
134 133 oveq2d ${⊢}{k}={i}\to \left(1-{t}\right){A}\left({k}\right)=\left(1-{t}\right){A}\left({i}\right)$
135 fveq2 ${⊢}{k}={i}\to {C}\left({k}\right)={C}\left({i}\right)$
136 135 oveq2d ${⊢}{k}={i}\to {t}{C}\left({k}\right)={t}{C}\left({i}\right)$
137 134 136 oveq12d ${⊢}{k}={i}\to \left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)$
138 137 oveq2d ${⊢}{k}={i}\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)$
139 fveq2 ${⊢}{k}={i}\to {B}\left({k}\right)={B}\left({i}\right)$
140 139 oveq2d ${⊢}{k}={i}\to {r}{B}\left({k}\right)={r}{B}\left({i}\right)$
141 138 140 oveq12d ${⊢}{k}={i}\to \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)$
142 eqid ${⊢}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)$
143 ovex ${⊢}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\in \mathrm{V}$
144 141 142 143 fvmpt ${⊢}{i}\in \left(1\dots {N}\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)$
145 132 144 sylan9eq ${⊢}\left({x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)$
146 145 eqeq1d ${⊢}\left({x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)↔\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\right)$
147 145 eqeq1d ${⊢}\left({x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left({x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)↔\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
148 146 147 anbi12d ${⊢}\left({x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)↔\left(\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
149 eqid ${⊢}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)$
150 149 biantrur ${⊢}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)↔\left(\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge \left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
151 148 150 syl6bbr ${⊢}\left({x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)↔\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
152 151 ralbidva ${⊢}{x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
153 152 rspcev ${⊢}\left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\in 𝔼\left({N}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
154 153 ex ${⊢}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({k}\right)+{t}{C}\left({k}\right)\right)+{r}{B}\left({k}\right)\right)\in 𝔼\left({N}\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
155 131 154 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {r}\in \left[0,1\right]\right)\wedge {q}\in \left[0,1\right]\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
156 155 reximdva ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\wedge {r}\in \left[0,1\right]\right)\to \left(\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\to \exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
157 156 reximdva ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \left(\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
158 103 157 mpd ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
159 rexcom ${⊢}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)↔\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
160 159 rexbii ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
161 rexcom ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)↔\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
162 160 161 bitri ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)↔\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
163 158 162 sylib ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
164 oveq2 ${⊢}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\to \left(1-{r}\right){D}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)$
165 164 oveq1d ${⊢}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\to \left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)$
166 165 eqeq2d ${⊢}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\to \left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)↔{x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\right)$
167 oveq2 ${⊢}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\to \left(1-{q}\right){E}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)$
168 167 oveq1d ${⊢}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\to \left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)$
169 168 eqeq2d ${⊢}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\to \left({x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)↔{x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)$
170 166 169 bi2anan9 ${⊢}\left({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \left(\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
171 170 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
172 ralbi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
173 171 172 syl ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
174 173 rexbidv ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \left(\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
175 174 2rexbidv ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \left(\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right)\left(\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right)\left(\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)+{q}{A}\left({i}\right)\right)\right)$
176 163 175 syl5ibrcom ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\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({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)\right)$
177 176 3expia ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({t}\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)\right)\right)$
178 177 rexlimdvv ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\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({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)\right)$
179 178 3adant3 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\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({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)\right)$
180 simp3l ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
181 simp21 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {A}\in 𝔼\left({N}\right)$
182 simp23 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
183 brbtwn ${⊢}\left({D}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({D}\mathrm{Btwn}⟨{A},{C}⟩↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)$
184 180 181 182 183 syl3anc ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left({D}\mathrm{Btwn}⟨{A},{C}⟩↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\right)$
185 simp3r ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {E}\in 𝔼\left({N}\right)$
186 simp22 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to {B}\in 𝔼\left({N}\right)$
187 brbtwn ${⊢}\left({E}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({E}\mathrm{Btwn}⟨{B},{C}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)$
188 185 186 182 187 syl3anc ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left({E}\mathrm{Btwn}⟨{B},{C}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)$
189 184 188 anbi12d ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({D}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{B},{C}⟩\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}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\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}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\right)$
190 r19.26 ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)↔\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)$
191 190 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({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\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}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)$
192 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}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\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}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\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}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)$
193 191 192 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({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\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}}{D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\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}}{E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)$
194 189 193 syl6bbr ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({D}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{B},{C}⟩\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({D}\left({i}\right)=\left(1-{t}\right){A}\left({i}\right)+{t}{C}\left({i}\right)\wedge {E}\left({i}\right)=\left(1-{s}\right){B}\left({i}\right)+{s}{C}\left({i}\right)\right)\right)$
195 simpr ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {x}\in 𝔼\left({N}\right)$
196 simpl3l ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {D}\in 𝔼\left({N}\right)$
197 simpl22 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {B}\in 𝔼\left({N}\right)$
198 brbtwn ${⊢}\left({x}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{D},{B}⟩↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\right)$
199 195 196 197 198 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{D},{B}⟩↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\right)$
200 simpl3r ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {E}\in 𝔼\left({N}\right)$
201 simpl21 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {A}\in 𝔼\left({N}\right)$
202 brbtwn ${⊢}\left({x}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{E},{A}⟩↔\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)$
203 195 200 201 202 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{E},{A}⟩↔\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)$
204 199 203 anbi12d ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left(\left({x}\mathrm{Btwn}⟨{D},{B}⟩\wedge {x}\mathrm{Btwn}⟨{E},{A}⟩\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}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge \exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)\right)$
205 r19.26 ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)$
206 205 2rexbii ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)$
207 reeanv ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\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}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge \exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)$
208 206 207 bitri ${⊢}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\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}}{x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge \exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)$
209 204 208 syl6bbr ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left(\left({x}\mathrm{Btwn}⟨{D},{B}⟩\wedge {x}\mathrm{Btwn}⟨{E},{A}⟩\right)↔\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)\right)$
210 209 rexbidva ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{Btwn}⟨{D},{B}⟩\wedge {x}\mathrm{Btwn}⟨{E},{A}⟩\right)↔\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {q}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{r}\right){D}\left({i}\right)+{r}{B}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{q}\right){E}\left({i}\right)+{q}{A}\left({i}\right)\right)\right)$
211 179 194 210 3imtr4d ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({D}\mathrm{Btwn}⟨{A},{C}⟩\wedge {E}\mathrm{Btwn}⟨{B},{C}⟩\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{Btwn}⟨{D},{B}⟩\wedge {x}\mathrm{Btwn}⟨{E},{A}⟩\right)\right)$