axcontlem4

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

		Ref	Expression
	Hypothesis	axcontlem4.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	Assertion	axcontlem4	$⊢ ((N \in ℕ \land (A \subseteq 𝔼 (N) \land B \subseteq 𝔼 (N) \land \forall x \in A \forall y \in B x Btwn ⟨Z, y⟩)) \land ((Z \in 𝔼 (N) \land U \in A \land B \neq \emptyset) \land Z \neq U)) \to A \subseteq D$

Proof

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

Metamath Proof Explorer

Theorem axcontlem4

Proof