# Metamath Proof Explorer

## Theorem axcontlem2

Description: Lemma for axcont . The idea here is to set up a mapping F that will allow us to transfer dedekind to two sets of points. Here, we set up F and show its domain and range. (Contributed by Scott Fenton, 17-Jun-2013)

Ref Expression
Hypotheses axcontlem2.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
axcontlem2.2 ${⊢}{F}=\left\{⟨{x},{t}⟩|\left({x}\in {D}\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
Assertion axcontlem2 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to {F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 axcontlem2.1 ${⊢}{D}=\left\{{p}\in 𝔼\left({N}\right)|\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right\}$
2 axcontlem2.2 ${⊢}{F}=\left\{⟨{x},{t}⟩|\left({x}\in {D}\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
3 opeq2 ${⊢}{p}={x}\to ⟨{Z},{p}⟩=⟨{Z},{x}⟩$
4 3 breq2d ${⊢}{p}={x}\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩↔{U}\mathrm{Btwn}⟨{Z},{x}⟩\right)$
5 breq1 ${⊢}{p}={x}\to \left({p}\mathrm{Btwn}⟨{Z},{U}⟩↔{x}\mathrm{Btwn}⟨{Z},{U}⟩\right)$
6 4 5 orbi12d ${⊢}{p}={x}\to \left(\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)↔\left({U}\mathrm{Btwn}⟨{Z},{x}⟩\vee {x}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
7 6 1 elrab2 ${⊢}{x}\in {D}↔\left({x}\in 𝔼\left({N}\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{x}⟩\vee {x}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
8 simpll3 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {U}\in 𝔼\left({N}\right)$
9 simpll2 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
10 simpr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {x}\in 𝔼\left({N}\right)$
11 brbtwn ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{x}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
12 8 9 10 11 syl3anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{x}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
13 12 biimpa ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {U}\mathrm{Btwn}⟨{Z},{x}⟩\right)\to \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)$
14 simp-4r ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\to {Z}\ne {U}$
15 oveq2 ${⊢}{s}=0\to 1-{s}=1-0$
16 1m0e1 ${⊢}1-0=1$
17 15 16 syl6eq ${⊢}{s}=0\to 1-{s}=1$
18 17 oveq1d ${⊢}{s}=0\to \left(1-{s}\right){Z}\left({i}\right)=1{Z}\left({i}\right)$
19 oveq1 ${⊢}{s}=0\to {s}{x}\left({i}\right)=0\cdot {x}\left({i}\right)$
20 18 19 oveq12d ${⊢}{s}=0\to \left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)$
21 20 eqeq2d ${⊢}{s}=0\to \left({U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)↔{U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)\right)$
22 21 ralbidv ${⊢}{s}=0\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)\right)$
23 22 biimpac ${⊢}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\wedge {s}=0\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)$
24 eqcom ${⊢}{Z}={U}↔{U}={Z}$
25 8 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\to {U}\in 𝔼\left({N}\right)$
26 9 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\to {Z}\in 𝔼\left({N}\right)$
27 eqeefv ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\right)\to \left({U}={Z}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)={Z}\left({i}\right)\right)$
28 25 26 27 syl2anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\to \left({U}={Z}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)={Z}\left({i}\right)\right)$
29 9 ad2antrr ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
30 fveecn ${⊢}\left({Z}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
31 29 30 sylancom ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
32 fveecn ${⊢}\left({x}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)\in ℂ$
33 32 ad4ant24 ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)\in ℂ$
34 mulid2 ${⊢}{Z}\left({i}\right)\in ℂ\to 1{Z}\left({i}\right)={Z}\left({i}\right)$
35 mul02 ${⊢}{x}\left({i}\right)\in ℂ\to 0\cdot {x}\left({i}\right)=0$
36 34 35 oveqan12d ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {x}\left({i}\right)\in ℂ\right)\to 1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)={Z}\left({i}\right)+0$
37 addid1 ${⊢}{Z}\left({i}\right)\in ℂ\to {Z}\left({i}\right)+0={Z}\left({i}\right)$
38 37 adantr ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {x}\left({i}\right)\in ℂ\right)\to {Z}\left({i}\right)+0={Z}\left({i}\right)$
39 36 38 eqtrd ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {x}\left({i}\right)\in ℂ\right)\to 1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)={Z}\left({i}\right)$
40 39 eqeq2d ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {x}\left({i}\right)\in ℂ\right)\to \left({U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)↔{U}\left({i}\right)={Z}\left({i}\right)\right)$
41 31 33 40 syl2anc ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left({U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)↔{U}\left({i}\right)={Z}\left({i}\right)\right)$
42 41 ralbidva ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)={Z}\left({i}\right)\right)$
43 28 42 bitr4d ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\to \left({U}={Z}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)\right)$
44 24 43 syl5bb ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\to \left({Z}={U}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=1{Z}\left({i}\right)+0\cdot {x}\left({i}\right)\right)$
45 23 44 syl5ibr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\wedge {s}=0\right)\to {Z}={U}\right)$
46 45 expdimp ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\to \left({s}=0\to {Z}={U}\right)$
47 46 necon3d ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\to \left({Z}\ne {U}\to {s}\ne 0\right)$
48 14 47 mpd ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\to {s}\ne 0$
49 elicc01 ${⊢}{s}\in \left[0,1\right]↔\left({s}\in ℝ\wedge 0\le {s}\wedge {s}\le 1\right)$
50 49 simp1bi ${⊢}{s}\in \left[0,1\right]\to {s}\in ℝ$
51 rereccl ${⊢}\left({s}\in ℝ\wedge {s}\ne 0\right)\to \frac{1}{{s}}\in ℝ$
52 50 51 sylan ${⊢}\left({s}\in \left[0,1\right]\wedge {s}\ne 0\right)\to \frac{1}{{s}}\in ℝ$
53 50 adantr ${⊢}\left({s}\in \left[0,1\right]\wedge {s}\ne 0\right)\to {s}\in ℝ$
54 49 simp2bi ${⊢}{s}\in \left[0,1\right]\to 0\le {s}$
55 54 adantr ${⊢}\left({s}\in \left[0,1\right]\wedge {s}\ne 0\right)\to 0\le {s}$
56 simpr ${⊢}\left({s}\in \left[0,1\right]\wedge {s}\ne 0\right)\to {s}\ne 0$
57 53 55 56 ne0gt0d ${⊢}\left({s}\in \left[0,1\right]\wedge {s}\ne 0\right)\to 0<{s}$
58 1re ${⊢}1\in ℝ$
59 0le1 ${⊢}0\le 1$
60 divge0 ${⊢}\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left({s}\in ℝ\wedge 0<{s}\right)\right)\to 0\le \frac{1}{{s}}$
61 58 59 60 mpanl12 ${⊢}\left({s}\in ℝ\wedge 0<{s}\right)\to 0\le \frac{1}{{s}}$
62 53 57 61 syl2anc ${⊢}\left({s}\in \left[0,1\right]\wedge {s}\ne 0\right)\to 0\le \frac{1}{{s}}$
63 elrege0 ${⊢}\frac{1}{{s}}\in \left[0,\mathrm{+\infty }\right)↔\left(\frac{1}{{s}}\in ℝ\wedge 0\le \frac{1}{{s}}\right)$
64 52 62 63 sylanbrc ${⊢}\left({s}\in \left[0,1\right]\wedge {s}\ne 0\right)\to \frac{1}{{s}}\in \left[0,\mathrm{+\infty }\right)$
65 64 adantll ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\to \frac{1}{{s}}\in \left[0,\mathrm{+\infty }\right)$
66 50 ad3antlr ${⊢}\left(\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in ℝ$
67 66 recnd ${⊢}\left(\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\in ℂ$
68 simplr ${⊢}\left(\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {s}\ne 0$
69 32 ad5ant25 ${⊢}\left(\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)\in ℂ$
70 9 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
71 70 30 sylancom ${⊢}\left(\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
72 ax-1cn ${⊢}1\in ℂ$
73 reccl ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \frac{1}{{s}}\in ℂ$
74 subcl ${⊢}\left(1\in ℂ\wedge \frac{1}{{s}}\in ℂ\right)\to 1-\left(\frac{1}{{s}}\right)\in ℂ$
75 72 73 74 sylancr ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to 1-\left(\frac{1}{{s}}\right)\in ℂ$
76 75 adantr ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to 1-\left(\frac{1}{{s}}\right)\in ℂ$
77 subcl ${⊢}\left(1\in ℂ\wedge {s}\in ℂ\right)\to 1-{s}\in ℂ$
78 72 77 mpan ${⊢}{s}\in ℂ\to 1-{s}\in ℂ$
79 78 adantr ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to 1-{s}\in ℂ$
80 73 79 mulcld ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{1}{{s}}\right)\left(1-{s}\right)\in ℂ$
81 80 adantr ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right)\left(1-{s}\right)\in ℂ$
82 simprr ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to {Z}\left({i}\right)\in ℂ$
83 76 81 82 adddird ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right)\right){Z}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)$
84 simpl ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to {s}\in ℂ$
85 subdi ${⊢}\left(\frac{1}{{s}}\in ℂ\wedge 1\in ℂ\wedge {s}\in ℂ\right)\to \left(\frac{1}{{s}}\right)\left(1-{s}\right)=\left(\frac{1}{{s}}\right)\cdot 1-\left(\frac{1}{{s}}\right){s}$
86 72 85 mp3an2 ${⊢}\left(\frac{1}{{s}}\in ℂ\wedge {s}\in ℂ\right)\to \left(\frac{1}{{s}}\right)\left(1-{s}\right)=\left(\frac{1}{{s}}\right)\cdot 1-\left(\frac{1}{{s}}\right){s}$
87 73 84 86 syl2anc ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{1}{{s}}\right)\left(1-{s}\right)=\left(\frac{1}{{s}}\right)\cdot 1-\left(\frac{1}{{s}}\right){s}$
88 87 oveq2d ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to 1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right)=\left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)\cdot 1-\left(\frac{1}{{s}}\right){s}$
89 73 mulid1d ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{1}{{s}}\right)\cdot 1=\frac{1}{{s}}$
90 recid2 ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{1}{{s}}\right){s}=1$
91 89 90 oveq12d ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{1}{{s}}\right)\cdot 1-\left(\frac{1}{{s}}\right){s}=\left(\frac{1}{{s}}\right)-1$
92 91 oveq2d ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)\cdot 1-\left(\frac{1}{{s}}\right){s}=\left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1$
93 addsubass ${⊢}\left(1-\left(\frac{1}{{s}}\right)\in ℂ\wedge \frac{1}{{s}}\in ℂ\wedge 1\in ℂ\right)\to \left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1=\left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1$
94 72 93 mp3an3 ${⊢}\left(1-\left(\frac{1}{{s}}\right)\in ℂ\wedge \frac{1}{{s}}\in ℂ\right)\to \left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1=\left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1$
95 75 73 94 syl2anc ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1=\left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1$
96 75 73 addcld ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to 1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)\in ℂ$
97 npcan ${⊢}\left(1\in ℂ\wedge \frac{1}{{s}}\in ℂ\right)\to 1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)=1$
98 72 73 97 sylancr ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to 1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)=1$
99 96 98 subeq0bd ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)-1=0$
100 92 95 99 3eqtr2d ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(1-\left(\frac{1}{{s}}\right)\right)+\left(\frac{1}{{s}}\right)\cdot 1-\left(\frac{1}{{s}}\right){s}=0$
101 88 100 eqtrd ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to 1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right)=0$
102 101 adantr ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to 1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right)=0$
103 102 oveq1d ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right)\right){Z}\left({i}\right)=0\cdot {Z}\left({i}\right)$
104 73 adantr ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \frac{1}{{s}}\in ℂ$
105 78 ad2antrr ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to 1-{s}\in ℂ$
106 104 105 82 mulassd ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)=\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)$
107 106 oveq2d ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)$
108 83 103 107 3eqtr3rd ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)=0\cdot {Z}\left({i}\right)$
109 mul02 ${⊢}{Z}\left({i}\right)\in ℂ\to 0\cdot {Z}\left({i}\right)=0$
110 109 ad2antll ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to 0\cdot {Z}\left({i}\right)=0$
111 108 110 eqtrd ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)=0$
112 simpll ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to {s}\in ℂ$
113 simprl ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to {x}\left({i}\right)\in ℂ$
114 104 112 113 mulassd ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right){s}{x}\left({i}\right)=\left(\frac{1}{{s}}\right){s}{x}\left({i}\right)$
115 90 oveq1d ${⊢}\left({s}\in ℂ\wedge {s}\ne 0\right)\to \left(\frac{1}{{s}}\right){s}{x}\left({i}\right)=1{x}\left({i}\right)$
116 mulid2 ${⊢}{x}\left({i}\right)\in ℂ\to 1{x}\left({i}\right)={x}\left({i}\right)$
117 116 adantr ${⊢}\left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\to 1{x}\left({i}\right)={x}\left({i}\right)$
118 115 117 sylan9eq ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right){s}{x}\left({i}\right)={x}\left({i}\right)$
119 114 118 eqtr3d ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right){s}{x}\left({i}\right)={x}\left({i}\right)$
120 111 119 oveq12d ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right){s}{x}\left({i}\right)=0+{x}\left({i}\right)$
121 76 82 mulcld ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)\in ℂ$
122 simpr ${⊢}\left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\to {Z}\left({i}\right)\in ℂ$
123 mulcl ${⊢}\left(1-{s}\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\to \left(1-{s}\right){Z}\left({i}\right)\in ℂ$
124 79 122 123 syl2an ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-{s}\right){Z}\left({i}\right)\in ℂ$
125 104 124 mulcld ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)\in ℂ$
126 mulcl ${⊢}\left({s}\in ℂ\wedge {x}\left({i}\right)\in ℂ\right)\to {s}{x}\left({i}\right)\in ℂ$
127 126 ad2ant2r ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to {s}{x}\left({i}\right)\in ℂ$
128 104 127 mulcld ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right){s}{x}\left({i}\right)\in ℂ$
129 121 125 128 addassd ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right){s}{x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right){s}{x}\left({i}\right)$
130 104 124 127 adddid ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)=\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right){s}{x}\left({i}\right)$
131 130 oveq2d ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right){s}{x}\left({i}\right)$
132 129 131 eqtr4d ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(1-{s}\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right){s}{x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
133 addid2 ${⊢}{x}\left({i}\right)\in ℂ\to 0+{x}\left({i}\right)={x}\left({i}\right)$
134 133 ad2antrl ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to 0+{x}\left({i}\right)={x}\left({i}\right)$
135 120 132 134 3eqtr3rd ${⊢}\left(\left({s}\in ℂ\wedge {s}\ne 0\right)\wedge \left({x}\left({i}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\right)\to {x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
136 67 68 69 71 135 syl22anc ${⊢}\left(\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
137 136 ralrimiva ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
138 oveq2 ${⊢}{t}=\frac{1}{{s}}\to 1-{t}=1-\left(\frac{1}{{s}}\right)$
139 138 oveq1d ${⊢}{t}=\frac{1}{{s}}\to \left(1-{t}\right){Z}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)$
140 oveq1 ${⊢}{t}=\frac{1}{{s}}\to {t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)=\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
141 139 140 oveq12d ${⊢}{t}=\frac{1}{{s}}\to \left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
142 141 eqeq2d ${⊢}{t}=\frac{1}{{s}}\to \left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)↔{x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)$
143 142 ralbidv ${⊢}{t}=\frac{1}{{s}}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)$
144 143 rspcev ${⊢}\left(\frac{1}{{s}}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-\left(\frac{1}{{s}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{s}}\right)\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
145 65 137 144 syl2anc ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
146 oveq2 ${⊢}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\to {t}{U}\left({i}\right)={t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
147 146 oveq2d ${⊢}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\to \left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)$
148 147 eqeq2d ${⊢}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\to \left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)$
149 148 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)$
150 ralbi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)$
151 149 150 syl ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)$
152 151 rexbidv ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\to \left(\exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}\left(\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\right)$
153 145 152 syl5ibrcom ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge {s}\ne 0\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
154 153 impancom ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\to \left({s}\ne 0\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
155 48 154 mpd ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {s}\in \left[0,1\right]\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
156 155 r19.29an ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\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}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{x}\left({i}\right)\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
157 13 156 syldan ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {U}\mathrm{Btwn}⟨{Z},{x}⟩\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
158 3simpa ${⊢}\left({x}\in ℝ\wedge 0\le {x}\wedge {x}\le 1\right)\to \left({x}\in ℝ\wedge 0\le {x}\right)$
159 elicc01 ${⊢}{x}\in \left[0,1\right]↔\left({x}\in ℝ\wedge 0\le {x}\wedge {x}\le 1\right)$
160 elrege0 ${⊢}{x}\in \left[0,\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge 0\le {x}\right)$
161 158 159 160 3imtr4i ${⊢}{x}\in \left[0,1\right]\to {x}\in \left[0,\mathrm{+\infty }\right)$
162 161 ssriv ${⊢}\left[0,1\right]\subseteq \left[0,\mathrm{+\infty }\right)$
163 brbtwn ${⊢}\left({x}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{Z},{U}⟩↔\exists {t}\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-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
164 10 9 8 163 syl3anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{Z},{U}⟩↔\exists {t}\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-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
165 164 biimpa ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {x}\mathrm{Btwn}⟨{Z},{U}⟩\right)\to \exists {t}\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-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
166 ssrexv ${⊢}\left[0,1\right]\subseteq \left[0,\mathrm{+\infty }\right)\to \left(\exists {t}\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-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
167 162 165 166 mpsyl ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge {x}\mathrm{Btwn}⟨{Z},{U}⟩\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
168 157 167 jaodan ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in 𝔼\left({N}\right)\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{x}⟩\vee {x}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
169 168 anasss ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({x}\in 𝔼\left({N}\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},{x}⟩\vee {x}\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
170 7 169 sylan2b ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in {D}\right)\to \exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
171 r19.26 ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)↔\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)$
172 eqtr2 ${⊢}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)\to \left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)$
173 172 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge {x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)$
174 171 173 sylbir ${⊢}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)$
175 elrege0 ${⊢}{t}\in \left[0,\mathrm{+\infty }\right)↔\left({t}\in ℝ\wedge 0\le {t}\right)$
176 175 simplbi ${⊢}{t}\in \left[0,\mathrm{+\infty }\right)\to {t}\in ℝ$
177 176 recnd ${⊢}{t}\in \left[0,\mathrm{+\infty }\right)\to {t}\in ℂ$
178 elrege0 ${⊢}{s}\in \left[0,\mathrm{+\infty }\right)↔\left({s}\in ℝ\wedge 0\le {s}\right)$
179 178 simplbi ${⊢}{s}\in \left[0,\mathrm{+\infty }\right)\to {s}\in ℝ$
180 179 recnd ${⊢}{s}\in \left[0,\mathrm{+\infty }\right)\to {s}\in ℂ$
181 177 180 anim12i ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge {s}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({t}\in ℂ\wedge {s}\in ℂ\right)$
182 simplr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left({t}\in ℂ\wedge {s}\in ℂ\right)$
183 simpl2 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to {Z}\in 𝔼\left({N}\right)$
184 183 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
185 184 30 sylancom ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
186 simpl3 ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to {U}\in 𝔼\left({N}\right)$
187 186 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\in 𝔼\left({N}\right)$
188 fveecn ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\left({i}\right)\in ℂ$
189 187 188 sylancom ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\left({i}\right)\in ℂ$
190 subcl ${⊢}\left(1\in ℂ\wedge {t}\in ℂ\right)\to 1-{t}\in ℂ$
191 72 190 mpan ${⊢}{t}\in ℂ\to 1-{t}\in ℂ$
192 191 adantr ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\right)\to 1-{t}\in ℂ$
193 simpl ${⊢}\left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\to {Z}\left({i}\right)\in ℂ$
194 mulcl ${⊢}\left(1-{t}\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\to \left(1-{t}\right){Z}\left({i}\right)\in ℂ$
195 192 193 194 syl2an ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{t}\right){Z}\left({i}\right)\in ℂ$
196 mulcl ${⊢}\left({t}\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\to {t}{U}\left({i}\right)\in ℂ$
197 196 ad2ant2rl ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {t}{U}\left({i}\right)\in ℂ$
198 78 adantl ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\right)\to 1-{s}\in ℂ$
199 198 193 123 syl2an ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{s}\right){Z}\left({i}\right)\in ℂ$
200 mulcl ${⊢}\left({s}\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\to {s}{U}\left({i}\right)\in ℂ$
201 200 ad2ant2l ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {s}{U}\left({i}\right)\in ℂ$
202 195 197 199 201 addsubeq4d ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)↔\left(1-{s}\right){Z}\left({i}\right)-\left(1-{t}\right){Z}\left({i}\right)={t}{U}\left({i}\right)-{s}{U}\left({i}\right)\right)$
203 nnncan1 ${⊢}\left(1\in ℂ\wedge {s}\in ℂ\wedge {t}\in ℂ\right)\to 1-{s}-\left(1-{t}\right)={t}-{s}$
204 72 203 mp3an1 ${⊢}\left({s}\in ℂ\wedge {t}\in ℂ\right)\to 1-{s}-\left(1-{t}\right)={t}-{s}$
205 204 ancoms ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\right)\to 1-{s}-\left(1-{t}\right)={t}-{s}$
206 205 oveq1d ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\right)\to \left(1-{s}-\left(1-{t}\right)\right){Z}\left({i}\right)=\left({t}-{s}\right){Z}\left({i}\right)$
207 206 adantr ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{s}-\left(1-{t}\right)\right){Z}\left({i}\right)=\left({t}-{s}\right){Z}\left({i}\right)$
208 78 ad2antlr ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{s}\in ℂ$
209 191 ad2antrr ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{t}\in ℂ$
210 simprl ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {Z}\left({i}\right)\in ℂ$
211 208 209 210 subdird ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{s}-\left(1-{t}\right)\right){Z}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)-\left(1-{t}\right){Z}\left({i}\right)$
212 207 211 eqtr3d ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({t}-{s}\right){Z}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)-\left(1-{t}\right){Z}\left({i}\right)$
213 simpll ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {t}\in ℂ$
214 simplr ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {s}\in ℂ$
215 simprr ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {U}\left({i}\right)\in ℂ$
216 213 214 215 subdird ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left({t}-{s}\right){U}\left({i}\right)={t}{U}\left({i}\right)-{s}{U}\left({i}\right)$
217 212 216 eqeq12d ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left({t}-{s}\right){Z}\left({i}\right)=\left({t}-{s}\right){U}\left({i}\right)↔\left(1-{s}\right){Z}\left({i}\right)-\left(1-{t}\right){Z}\left({i}\right)={t}{U}\left({i}\right)-{s}{U}\left({i}\right)\right)$
218 subcl ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\right)\to {t}-{s}\in ℂ$
219 218 adantr ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {t}-{s}\in ℂ$
220 mulcan1g ${⊢}\left({t}-{s}\in ℂ\wedge {Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\to \left(\left({t}-{s}\right){Z}\left({i}\right)=\left({t}-{s}\right){U}\left({i}\right)↔\left({t}-{s}=0\vee {Z}\left({i}\right)={U}\left({i}\right)\right)\right)$
221 219 210 215 220 syl3anc ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left({t}-{s}\right){Z}\left({i}\right)=\left({t}-{s}\right){U}\left({i}\right)↔\left({t}-{s}=0\vee {Z}\left({i}\right)={U}\left({i}\right)\right)\right)$
222 202 217 221 3bitr2d ${⊢}\left(\left({t}\in ℂ\wedge {s}\in ℂ\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)↔\left({t}-{s}=0\vee {Z}\left({i}\right)={U}\left({i}\right)\right)\right)$
223 182 185 189 222 syl12anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to \left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)↔\left({t}-{s}=0\vee {Z}\left({i}\right)={U}\left({i}\right)\right)\right)$
224 223 ralbidva ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({t}-{s}=0\vee {Z}\left({i}\right)={U}\left({i}\right)\right)\right)$
225 r19.32v ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({t}-{s}=0\vee {Z}\left({i}\right)={U}\left({i}\right)\right)↔\left({t}-{s}=0\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)$
226 simplr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to {Z}\ne {U}$
227 226 neneqd ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to ¬{Z}={U}$
228 simpll2 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to {Z}\in 𝔼\left({N}\right)$
229 simpll3 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to {U}\in 𝔼\left({N}\right)$
230 eqeefv ${⊢}\left({Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\to \left({Z}={U}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)$
231 228 229 230 syl2anc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to \left({Z}={U}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)$
232 227 231 mtbid ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to ¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)$
233 orel2 ${⊢}¬\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\to \left(\left({t}-{s}=0\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)\to {t}-{s}=0\right)$
234 232 233 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to \left(\left({t}-{s}=0\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)\to {t}-{s}=0\right)$
235 subeq0 ${⊢}\left({t}\in ℂ\wedge {s}\in ℂ\right)\to \left({t}-{s}=0↔{t}={s}\right)$
236 235 adantl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to \left({t}-{s}=0↔{t}={s}\right)$
237 234 236 sylibd ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to \left(\left({t}-{s}=0\vee \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}\left({i}\right)={U}\left({i}\right)\right)\to {t}={s}\right)$
238 225 237 syl5bi ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({t}-{s}=0\vee {Z}\left({i}\right)={U}\left({i}\right)\right)\to {t}={s}\right)$
239 224 238 sylbid ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in ℂ\wedge {s}\in ℂ\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\to {t}={s}\right)$
240 181 239 sylan2 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge {s}\in \left[0,\mathrm{+\infty }\right)\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\to {t}={s}\right)$
241 174 240 syl5 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge {s}\in \left[0,\mathrm{+\infty }\right)\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)\to {t}={s}\right)$
242 241 ralrimivva ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \forall {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)\to {t}={s}\right)$
243 242 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in {D}\right)\to \forall {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)\to {t}={s}\right)$
244 oveq2 ${⊢}{t}={s}\to 1-{t}=1-{s}$
245 244 oveq1d ${⊢}{t}={s}\to \left(1-{t}\right){Z}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)$
246 oveq1 ${⊢}{t}={s}\to {t}{U}\left({i}\right)={s}{U}\left({i}\right)$
247 245 246 oveq12d ${⊢}{t}={s}\to \left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)$
248 247 eqeq2d ${⊢}{t}={s}\to \left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)$
249 248 ralbidv ${⊢}{t}={s}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)$
250 249 reu4 ${⊢}\exists !{t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\left(\exists {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)\to {t}={s}\right)\right)$
251 170 243 250 sylanbrc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in {D}\right)\to \exists !{t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
252 df-reu ${⊢}\exists !{t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\exists !{t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
253 251 252 sylib ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {x}\in {D}\right)\to \exists !{t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
254 253 ralrimiva ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\exists !{t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
255 2 fnopabg ${⊢}\forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\exists !{t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)↔{F}Fn{D}$
256 254 255 sylib ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to {F}Fn{D}$
257 176 ad2antlr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {t}\in ℝ$
258 183 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
259 fveere ${⊢}\left({Z}\in 𝔼\left({N}\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {Z}\left({k}\right)\in ℝ$
260 258 259 sylancom ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {Z}\left({k}\right)\in ℝ$
261 186 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {U}\in 𝔼\left({N}\right)$
262 fveere ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {U}\left({k}\right)\in ℝ$
263 261 262 sylancom ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to {U}\left({k}\right)\in ℝ$
264 resubcl ${⊢}\left(1\in ℝ\wedge {t}\in ℝ\right)\to 1-{t}\in ℝ$
265 58 264 mpan ${⊢}{t}\in ℝ\to 1-{t}\in ℝ$
266 remulcl ${⊢}\left(1-{t}\in ℝ\wedge {Z}\left({k}\right)\in ℝ\right)\to \left(1-{t}\right){Z}\left({k}\right)\in ℝ$
267 265 266 sylan ${⊢}\left({t}\in ℝ\wedge {Z}\left({k}\right)\in ℝ\right)\to \left(1-{t}\right){Z}\left({k}\right)\in ℝ$
268 267 3adant3 ${⊢}\left({t}\in ℝ\wedge {Z}\left({k}\right)\in ℝ\wedge {U}\left({k}\right)\in ℝ\right)\to \left(1-{t}\right){Z}\left({k}\right)\in ℝ$
269 remulcl ${⊢}\left({t}\in ℝ\wedge {U}\left({k}\right)\in ℝ\right)\to {t}{U}\left({k}\right)\in ℝ$
270 269 3adant2 ${⊢}\left({t}\in ℝ\wedge {Z}\left({k}\right)\in ℝ\wedge {U}\left({k}\right)\in ℝ\right)\to {t}{U}\left({k}\right)\in ℝ$
271 268 270 readdcld ${⊢}\left({t}\in ℝ\wedge {Z}\left({k}\right)\in ℝ\wedge {U}\left({k}\right)\in ℝ\right)\to \left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\in ℝ$
272 257 260 263 271 syl3anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {k}\in \left(1\dots {N}\right)\right)\to \left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\in ℝ$
273 272 ralrimiva ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\in ℝ$
274 simpll1 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to {N}\in ℕ$
275 mptelee ${⊢}{N}\in ℕ\to \left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)↔\forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\in ℝ\right)$
276 274 275 syl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)↔\forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\in ℝ\right)$
277 273 276 mpbird ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)$
278 letric ${⊢}\left(1\in ℝ\wedge {t}\in ℝ\right)\to \left(1\le {t}\vee {t}\le 1\right)$
279 58 176 278 sylancr ${⊢}{t}\in \left[0,\mathrm{+\infty }\right)\to \left(1\le {t}\vee {t}\le 1\right)$
280 279 adantl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(1\le {t}\vee {t}\le 1\right)$
281 simpr ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to 1\le {t}$
282 176 adantr ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to {t}\in ℝ$
283 0red ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to 0\in ℝ$
284 1red ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to 1\in ℝ$
285 0lt1 ${⊢}0<1$
286 285 a1i ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to 0<1$
287 283 284 282 286 281 ltletrd ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to 0<{t}$
288 divelunit ${⊢}\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left({t}\in ℝ\wedge 0<{t}\right)\right)\to \left(\frac{1}{{t}}\in \left[0,1\right]↔1\le {t}\right)$
289 58 59 288 mpanl12 ${⊢}\left({t}\in ℝ\wedge 0<{t}\right)\to \left(\frac{1}{{t}}\in \left[0,1\right]↔1\le {t}\right)$
290 282 287 289 syl2anc ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to \left(\frac{1}{{t}}\in \left[0,1\right]↔1\le {t}\right)$
291 281 290 mpbird ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to \frac{1}{{t}}\in \left[0,1\right]$
292 291 adantll ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to \frac{1}{{t}}\in \left[0,1\right]$
293 176 ad3antlr ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in ℝ$
294 293 recnd ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\in ℂ$
295 287 gt0ne0d ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge 1\le {t}\right)\to {t}\ne 0$
296 295 adantll ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to {t}\ne 0$
297 296 adantr ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {t}\ne 0$
298 183 ad3antrrr ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\in 𝔼\left({N}\right)$
299 298 30 sylancom ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {Z}\left({i}\right)\in ℂ$
300 186 ad3antrrr ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\in 𝔼\left({N}\right)$
301 300 188 sylancom ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\left({i}\right)\in ℂ$
302 reccl ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \frac{1}{{t}}\in ℂ$
303 302 adantr ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \frac{1}{{t}}\in ℂ$
304 191 adantr ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to 1-{t}\in ℂ$
305 304 193 194 syl2an ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-{t}\right){Z}\left({i}\right)\in ℂ$
306 196 ad2ant2rl ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {t}{U}\left({i}\right)\in ℂ$
307 303 305 306 adddid ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)=\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right){t}{U}\left({i}\right)$
308 307 oveq2d ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right){t}{U}\left({i}\right)$
309 subcl ${⊢}\left(1\in ℂ\wedge \frac{1}{{t}}\in ℂ\right)\to 1-\left(\frac{1}{{t}}\right)\in ℂ$
310 72 302 309 sylancr ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to 1-\left(\frac{1}{{t}}\right)\in ℂ$
311 mulcl ${⊢}\left(1-\left(\frac{1}{{t}}\right)\in ℂ\wedge {Z}\left({i}\right)\in ℂ\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)\in ℂ$
312 310 193 311 syl2an ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)\in ℂ$
313 303 305 mulcld ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)\in ℂ$
314 recid2 ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{1}{{t}}\right){t}=1$
315 314 oveq1d ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{1}{{t}}\right){t}{U}\left({i}\right)=1{U}\left({i}\right)$
316 315 adantr ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right){t}{U}\left({i}\right)=1{U}\left({i}\right)$
317 simpll ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {t}\in ℂ$
318 simprr ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {U}\left({i}\right)\in ℂ$
319 303 317 318 mulassd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right){t}{U}\left({i}\right)=\left(\frac{1}{{t}}\right){t}{U}\left({i}\right)$
320 mulid2 ${⊢}{U}\left({i}\right)\in ℂ\to 1{U}\left({i}\right)={U}\left({i}\right)$
321 320 ad2antll ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1{U}\left({i}\right)={U}\left({i}\right)$
322 316 319 321 3eqtr3d ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right){t}{U}\left({i}\right)={U}\left({i}\right)$
323 322 318 eqeltrd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right){t}{U}\left({i}\right)\in ℂ$
324 312 313 323 addassd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right){t}{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right){t}{U}\left({i}\right)$
325 310 adantr ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-\left(\frac{1}{{t}}\right)\in ℂ$
326 302 304 mulcld ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right)\in ℂ$
327 326 adantr ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right)\in ℂ$
328 simprl ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {Z}\left({i}\right)\in ℂ$
329 325 327 328 adddird ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right)\right){Z}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)$
330 simpl ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to {t}\in ℂ$
331 subdi ${⊢}\left(\frac{1}{{t}}\in ℂ\wedge 1\in ℂ\wedge {t}\in ℂ\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right)=\left(\frac{1}{{t}}\right)\cdot 1-\left(\frac{1}{{t}}\right){t}$
332 72 331 mp3an2 ${⊢}\left(\frac{1}{{t}}\in ℂ\wedge {t}\in ℂ\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right)=\left(\frac{1}{{t}}\right)\cdot 1-\left(\frac{1}{{t}}\right){t}$
333 302 330 332 syl2anc ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right)=\left(\frac{1}{{t}}\right)\cdot 1-\left(\frac{1}{{t}}\right){t}$
334 302 mulid1d ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{1}{{t}}\right)\cdot 1=\frac{1}{{t}}$
335 334 314 oveq12d ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{1}{{t}}\right)\cdot 1-\left(\frac{1}{{t}}\right){t}=\left(\frac{1}{{t}}\right)-1$
336 333 335 eqtrd ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right)=\left(\frac{1}{{t}}\right)-1$
337 336 oveq2d ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to 1-\left(\frac{1}{{t}}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right)=\left(1-\left(\frac{1}{{t}}\right)\right)+\left(\frac{1}{{t}}\right)-1$
338 npncan2 ${⊢}\left(1\in ℂ\wedge \frac{1}{{t}}\in ℂ\right)\to \left(1-\left(\frac{1}{{t}}\right)\right)+\left(\frac{1}{{t}}\right)-1=0$
339 72 302 338 sylancr ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to \left(1-\left(\frac{1}{{t}}\right)\right)+\left(\frac{1}{{t}}\right)-1=0$
340 337 339 eqtrd ${⊢}\left({t}\in ℂ\wedge {t}\ne 0\right)\to 1-\left(\frac{1}{{t}}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right)=0$
341 340 adantr ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-\left(\frac{1}{{t}}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right)=0$
342 341 oveq1d ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right)\right){Z}\left({i}\right)=0\cdot {Z}\left({i}\right)$
343 109 ad2antrl ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 0\cdot {Z}\left({i}\right)=0$
344 342 343 eqtrd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right)\right){Z}\left({i}\right)=0$
345 191 ad2antrr ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 1-{t}\in ℂ$
346 303 345 328 mulassd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)=\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)$
347 346 oveq2d ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)$
348 329 344 347 3eqtr3rd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)=0$
349 348 322 oveq12d ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right){t}{U}\left({i}\right)=0+{U}\left({i}\right)$
350 addid2 ${⊢}{U}\left({i}\right)\in ℂ\to 0+{U}\left({i}\right)={U}\left({i}\right)$
351 350 ad2antll ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to 0+{U}\left({i}\right)={U}\left({i}\right)$
352 349 351 eqtrd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(1-{t}\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right){t}{U}\left({i}\right)={U}\left({i}\right)$
353 308 324 352 3eqtr2rd ${⊢}\left(\left({t}\in ℂ\wedge {t}\ne 0\right)\wedge \left({Z}\left({i}\right)\in ℂ\wedge {U}\left({i}\right)\in ℂ\right)\right)\to {U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
354 294 297 299 301 353 syl22anc ${⊢}\left(\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\wedge {i}\in \left(1\dots {N}\right)\right)\to {U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
355 354 ralrimiva ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
356 oveq2 ${⊢}{s}=\frac{1}{{t}}\to 1-{s}=1-\left(\frac{1}{{t}}\right)$
357 356 oveq1d ${⊢}{s}=\frac{1}{{t}}\to \left(1-{s}\right){Z}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)$
358 oveq1 ${⊢}{s}=\frac{1}{{t}}\to {s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)$
359 357 358 oveq12d ${⊢}{s}=\frac{1}{{t}}\to \left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)$
360 359 eqeq2d ${⊢}{s}=\frac{1}{{t}}\to \left({U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)↔{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)\right)$
361 360 ralbidv ${⊢}{s}=\frac{1}{{t}}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)\right)$
362 fveq2 ${⊢}{k}={i}\to {Z}\left({k}\right)={Z}\left({i}\right)$
363 362 oveq2d ${⊢}{k}={i}\to \left(1-{t}\right){Z}\left({k}\right)=\left(1-{t}\right){Z}\left({i}\right)$
364 fveq2 ${⊢}{k}={i}\to {U}\left({k}\right)={U}\left({i}\right)$
365 364 oveq2d ${⊢}{k}={i}\to {t}{U}\left({k}\right)={t}{U}\left({i}\right)$
366 363 365 oveq12d ${⊢}{k}={i}\to \left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
367 eqid ${⊢}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)$
368 ovex ${⊢}\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\in \mathrm{V}$
369 366 367 368 fvmpt ${⊢}{i}\in \left(1\dots {N}\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
370 369 oveq2d ${⊢}{i}\in \left(1\dots {N}\right)\to \left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
371 370 oveq2d ${⊢}{i}\in \left(1\dots {N}\right)\to \left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
372 371 eqeq2d ${⊢}{i}\in \left(1\dots {N}\right)\to \left({U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)↔{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)$
373 372 ralbiia ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
374 361 373 syl6bb ${⊢}{s}=\frac{1}{{t}}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)$
375 374 rspcev ${⊢}\left(\frac{1}{{t}}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-\left(\frac{1}{{t}}\right)\right){Z}\left({i}\right)+\left(\frac{1}{{t}}\right)\left(\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\to \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)$
376 292 355 375 syl2anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)$
377 186 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to {U}\in 𝔼\left({N}\right)$
378 183 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to {Z}\in 𝔼\left({N}\right)$
379 277 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)$
380 brbtwn ${⊢}\left({U}\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)\right)$
381 377 378 379 380 syl3anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to \left({U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{U}\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)\right)$
382 376 381 mpbird ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge 1\le {t}\right)\to {U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩$
383 382 ex ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(1\le {t}\to {U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩\right)$
384 simpll ${⊢}\left(\left({t}\in ℝ\wedge 0\le {t}\right)\wedge {t}\le 1\right)\to {t}\in ℝ$
385 simplr ${⊢}\left(\left({t}\in ℝ\wedge 0\le {t}\right)\wedge {t}\le 1\right)\to 0\le {t}$
386 simpr ${⊢}\left(\left({t}\in ℝ\wedge 0\le {t}\right)\wedge {t}\le 1\right)\to {t}\le 1$
387 384 385 386 3jca ${⊢}\left(\left({t}\in ℝ\wedge 0\le {t}\right)\wedge {t}\le 1\right)\to \left({t}\in ℝ\wedge 0\le {t}\wedge {t}\le 1\right)$
388 175 anbi1i ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge {t}\le 1\right)↔\left(\left({t}\in ℝ\wedge 0\le {t}\right)\wedge {t}\le 1\right)$
389 elicc01 ${⊢}{t}\in \left[0,1\right]↔\left({t}\in ℝ\wedge 0\le {t}\wedge {t}\le 1\right)$
390 387 388 389 3imtr4i ${⊢}\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge {t}\le 1\right)\to {t}\in \left[0,1\right]$
391 390 adantll ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {t}\le 1\right)\to {t}\in \left[0,1\right]$
392 369 rgen ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
393 oveq2 ${⊢}{s}={t}\to 1-{s}=1-{t}$
394 393 oveq1d ${⊢}{s}={t}\to \left(1-{s}\right){Z}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)$
395 oveq1 ${⊢}{s}={t}\to {s}{U}\left({i}\right)={t}{U}\left({i}\right)$
396 394 395 oveq12d ${⊢}{s}={t}\to \left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
397 396 eqeq2d ${⊢}{s}={t}\to \left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)↔\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
398 397 ralbidv ${⊢}{s}={t}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
399 398 rspcev ${⊢}\left({t}\in \left[0,1\right]\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)$
400 391 392 399 sylancl ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {t}\le 1\right)\to \exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)$
401 277 adantr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {t}\le 1\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)$
402 183 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {t}\le 1\right)\to {Z}\in 𝔼\left({N}\right)$
403 186 ad2antrr ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {t}\le 1\right)\to {U}\in 𝔼\left({N}\right)$
404 brbtwn ${⊢}\left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\to \left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)$
405 401 402 403 404 syl3anc ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {t}\le 1\right)\to \left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩↔\exists {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{s}\right){Z}\left({i}\right)+{s}{U}\left({i}\right)\right)$
406 400 405 mpbird ${⊢}\left(\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\wedge {t}\le 1\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩$
407 406 ex ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({t}\le 1\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩\right)$
408 383 407 orim12d ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left(\left(1\le {t}\vee {t}\le 1\right)\to \left({U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩\vee \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
409 280 408 mpd ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩\vee \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩\right)$
410 opeq2 ${⊢}{p}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\to ⟨{Z},{p}⟩=⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩$
411 410 breq2d ${⊢}{p}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\to \left({U}\mathrm{Btwn}⟨{Z},{p}⟩↔{U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩\right)$
412 breq1 ${⊢}{p}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\to \left({p}\mathrm{Btwn}⟨{Z},{U}⟩↔\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩\right)$
413 411 412 orbi12d ${⊢}{p}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\to \left(\left({U}\mathrm{Btwn}⟨{Z},{p}⟩\vee {p}\mathrm{Btwn}⟨{Z},{U}⟩\right)↔\left({U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩\vee \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
414 413 1 elrab2 ${⊢}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in {D}↔\left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in 𝔼\left({N}\right)\wedge \left({U}\mathrm{Btwn}⟨{Z},\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)⟩\vee \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\mathrm{Btwn}⟨{Z},{U}⟩\right)\right)$
415 277 409 414 sylanbrc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in {D}$
416 fveq1 ${⊢}{x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\to {x}\left({i}\right)=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)$
417 416 eqeq1d ${⊢}{x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\to \left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
418 417 ralbidv ${⊢}{x}=\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
419 418 rspcev ${⊢}\left(\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({k}\in \left(1\dots {N}\right)⟼\left(1-{t}\right){Z}\left({k}\right)+{t}{U}\left({k}\right)\right)\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to \exists {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
420 415 392 419 sylancl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \exists {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)$
421 7 simplbi ${⊢}{x}\in {D}\to {x}\in 𝔼\left({N}\right)$
422 1 ssrab3 ${⊢}{D}\subseteq 𝔼\left({N}\right)$
423 422 sseli ${⊢}{y}\in {D}\to {y}\in 𝔼\left({N}\right)$
424 421 423 anim12i ${⊢}\left({x}\in {D}\wedge {y}\in {D}\right)\to \left({x}\in 𝔼\left({N}\right)\wedge {y}\in 𝔼\left({N}\right)\right)$
425 r19.26 ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge {y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)↔\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
426 eqtr3 ${⊢}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge {y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to {x}\left({i}\right)={y}\left({i}\right)$
427 426 ralimi ${⊢}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge {y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)$
428 425 427 sylbir ${⊢}\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)$
429 eqeefv ${⊢}\left({x}\in 𝔼\left({N}\right)\wedge {y}\in 𝔼\left({N}\right)\right)\to \left({x}={y}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)$
430 429 adantl ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({x}\in 𝔼\left({N}\right)\wedge {y}\in 𝔼\left({N}\right)\right)\right)\to \left({x}={y}↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)={y}\left({i}\right)\right)$
431 428 430 syl5ibr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({x}\in 𝔼\left({N}\right)\wedge {y}\in 𝔼\left({N}\right)\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to {x}={y}\right)$
432 424 431 sylan2 ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge \left({x}\in {D}\wedge {y}\in {D}\right)\right)\to \left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to {x}={y}\right)$
433 432 ralrimivva ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to {x}={y}\right)$
434 433 adantr ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to {x}={y}\right)$
435 df-reu ${⊢}\exists !{x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
436 fveq1 ${⊢}{x}={y}\to {x}\left({i}\right)={y}\left({i}\right)$
437 436 eqeq1d ${⊢}{x}={y}\to \left({x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
438 437 ralbidv ${⊢}{x}={y}\to \left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
439 438 reu4 ${⊢}\exists !{x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)↔\left(\exists {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to {x}={y}\right)\right)$
440 435 439 bitr3i ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)↔\left(\exists {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\to {x}={y}\right)\right)$
441 420 434 440 sylanbrc ${⊢}\left(\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\wedge {t}\in \left[0,\mathrm{+\infty }\right)\right)\to \exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
442 441 ralrimiva ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to \forall {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)$
443 an12 ${⊢}\left({x}\in {D}\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)↔\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)$
444 443 opabbii ${⊢}\left\{⟨{x},{t}⟩|\left({x}\in {D}\wedge \left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}=\left\{⟨{x},{t}⟩|\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
445 2 444 eqtri ${⊢}{F}=\left\{⟨{x},{t}⟩|\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
446 445 cnveqi ${⊢}{{F}}^{-1}={\left\{⟨{x},{t}⟩|\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}}^{-1}$
447 cnvopab ${⊢}{\left\{⟨{x},{t}⟩|\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}}^{-1}=\left\{⟨{t},{x}⟩|\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
448 446 447 eqtri ${⊢}{{F}}^{-1}=\left\{⟨{t},{x}⟩|\left({t}\in \left[0,\mathrm{+\infty }\right)\wedge \left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)\right)\right\}$
449 448 fnopabg ${⊢}\forall {t}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {D}\wedge \forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){Z}\left({i}\right)+{t}{U}\left({i}\right)\right)↔{{F}}^{-1}Fn\left[0,\mathrm{+\infty }\right)$
450 442 449 sylib ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to {{F}}^{-1}Fn\left[0,\mathrm{+\infty }\right)$
451 dff1o4 ${⊢}{F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)↔\left({F}Fn{D}\wedge {{F}}^{-1}Fn\left[0,\mathrm{+\infty }\right)\right)$
452 256 450 451 sylanbrc ${⊢}\left(\left({N}\in ℕ\wedge {Z}\in 𝔼\left({N}\right)\wedge {U}\in 𝔼\left({N}\right)\right)\wedge {Z}\ne {U}\right)\to {F}:{D}\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right)$