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 = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	axcontlem2.2	$⊢ F = \{⟨x, t⟩ \| (x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)))\}$
Assertion	axcontlem2	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to F : D \underset{1-1 onto}{⟶} [0, +∞)$

Proof

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

Metamath Proof Explorer

Theorem axcontlem2

Proof