axpasch

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

		Ref	Expression
	Assertion	axpasch	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to ((D Btwn ⟨A, C⟩ \land E Btwn ⟨B, C⟩) \to \exists x \in 𝔼 (N) (x Btwn ⟨D, B⟩ \land x Btwn ⟨E, A⟩))$

Proof

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

Metamath Proof Explorer

Theorem axpasch

Proof