axeuclidlem

Description: Lemma for axeuclid . Handle the algebraic aspects of the theorem. (Contributed by Scott Fenton, 9-Sep-2013)

		Ref	Expression
	Assertion	axeuclidlem	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$

Proof

Step	Hyp	Ref	Expression
1		simp21	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to P \in [0, 1]$
2		simp22	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to Q \in [0, 1]$
3		fveere	$⊢ (A \in 𝔼 (N) \land k \in (1 \dots N)) \to A (k) \in ℝ$
4	3	expcom	$⊢ k \in (1 \dots N) \to (A \in 𝔼 (N) \to A (k) \in ℝ)$
5		fveere	$⊢ (B \in 𝔼 (N) \land k \in (1 \dots N)) \to B (k) \in ℝ$
6	5	expcom	$⊢ k \in (1 \dots N) \to (B \in 𝔼 (N) \to B (k) \in ℝ)$
7	4 6	anim12d	$⊢ k \in (1 \dots N) \to ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (A (k) \in ℝ \land B (k) \in ℝ))$
8		fveere	$⊢ (C \in 𝔼 (N) \land k \in (1 \dots N)) \to C (k) \in ℝ$
9	8	expcom	$⊢ k \in (1 \dots N) \to (C \in 𝔼 (N) \to C (k) \in ℝ)$
10		fveere	$⊢ (T \in 𝔼 (N) \land k \in (1 \dots N)) \to T (k) \in ℝ$
11	10	expcom	$⊢ k \in (1 \dots N) \to (T \in 𝔼 (N) \to T (k) \in ℝ)$
12	9 11	anim12d	$⊢ k \in (1 \dots N) \to ((C \in 𝔼 (N) \land T \in 𝔼 (N)) \to (C (k) \in ℝ \land T (k) \in ℝ))$
13	7 12	anim12d	$⊢ k \in (1 \dots N) \to (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \to ((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)))$
14	13	impcom	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land k \in (1 \dots N)) \to ((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ))$
15		unitssre	$⊢ [0, 1] \subseteq ℝ$
16	15	sseli	$⊢ P \in [0, 1] \to P \in ℝ$
17	16	3ad2ant1	$⊢ (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \to P \in ℝ$
18	17	adantl	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P \in ℝ$
19		peano2rem	$⊢ P \in ℝ \to P - 1 \in ℝ$
20	18 19	syl	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P - 1 \in ℝ$
21		simplll	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to A (k) \in ℝ$
22	20 21	remulcld	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (P - 1) A (k) \in ℝ$
23		simpllr	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to B (k) \in ℝ$
24	22 23	readdcld	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (P - 1) A (k) + B (k) \in ℝ$
25		simpr3	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P \neq 0$
26	24 18 25	redivcld	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(P - 1) A (k) + B (k)}{P} \in ℝ$
27	14 26	sylan	$⊢ ((((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land k \in (1 \dots N)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(P - 1) A (k) + B (k)}{P} \in ℝ$
28	27	an32s	$⊢ ((((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \land k \in (1 \dots N)) \to \frac{(P - 1) A (k) + B (k)}{P} \in ℝ$
29	28	ralrimiva	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \forall k \in (1 \dots N) \frac{(P - 1) A (k) + B (k)}{P} \in ℝ$
30		eleenn	$⊢ A \in 𝔼 (N) \to N \in ℕ$
31	30	ad3antrrr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to N \in ℕ$
32		mptelee	$⊢ N \in ℕ \to ((k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) \frac{(P - 1) A (k) + B (k)}{P} \in ℝ)$
33	31 32	syl	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) \frac{(P - 1) A (k) + B (k)}{P} \in ℝ)$
34	29 33	mpbird	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \in 𝔼 (N)$
35	34	3adant3	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \in 𝔼 (N)$
36		simplrl	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to C (k) \in ℝ$
37	22 36	readdcld	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (P - 1) A (k) + C (k) \in ℝ$
38	37 18 25	redivcld	$⊢ (((A (k) \in ℝ \land B (k) \in ℝ) \land (C (k) \in ℝ \land T (k) \in ℝ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(P - 1) A (k) + C (k)}{P} \in ℝ$
39	14 38	sylan	$⊢ ((((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land k \in (1 \dots N)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(P - 1) A (k) + C (k)}{P} \in ℝ$
40	39	an32s	$⊢ ((((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \land k \in (1 \dots N)) \to \frac{(P - 1) A (k) + C (k)}{P} \in ℝ$
41	40	ralrimiva	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \forall k \in (1 \dots N) \frac{(P - 1) A (k) + C (k)}{P} \in ℝ$
42		mptelee	$⊢ N \in ℕ \to ((k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) \frac{(P - 1) A (k) + C (k)}{P} \in ℝ)$
43	31 42	syl	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) \frac{(P - 1) A (k) + C (k)}{P} \in ℝ)$
44	41 43	mpbird	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \in 𝔼 (N)$
45	44	3adant3	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \in 𝔼 (N)$
46		fveecn	$⊢ (A \in 𝔼 (N) \land i \in (1 \dots N)) \to A (i) \in ℂ$
47	46	expcom	$⊢ i \in (1 \dots N) \to (A \in 𝔼 (N) \to A (i) \in ℂ)$
48		fveecn	$⊢ (B \in 𝔼 (N) \land i \in (1 \dots N)) \to B (i) \in ℂ$
49	48	expcom	$⊢ i \in (1 \dots N) \to (B \in 𝔼 (N) \to B (i) \in ℂ)$
50	47 49	anim12d	$⊢ i \in (1 \dots N) \to ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (A (i) \in ℂ \land B (i) \in ℂ))$
51		fveecn	$⊢ (C \in 𝔼 (N) \land i \in (1 \dots N)) \to C (i) \in ℂ$
52	51	expcom	$⊢ i \in (1 \dots N) \to (C \in 𝔼 (N) \to C (i) \in ℂ)$
53		fveecn	$⊢ (T \in 𝔼 (N) \land i \in (1 \dots N)) \to T (i) \in ℂ$
54	53	expcom	$⊢ i \in (1 \dots N) \to (T \in 𝔼 (N) \to T (i) \in ℂ)$
55	52 54	anim12d	$⊢ i \in (1 \dots N) \to ((C \in 𝔼 (N) \land T \in 𝔼 (N)) \to (C (i) \in ℂ \land T (i) \in ℂ))$
56	50 55	anim12d	$⊢ i \in (1 \dots N) \to (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \to ((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)))$
57	56	impcom	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land i \in (1 \dots N)) \to ((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ))$
58		eqcom	$⊢ T (i) = \frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} \leftrightarrow \frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} = T (i)$
59		ax-1cn	$⊢ 1 \in ℂ$
60		simpr2	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to Q \in [0, 1]$
61	15	sseli	$⊢ Q \in [0, 1] \to Q \in ℝ$
62	61	recnd	$⊢ Q \in [0, 1] \to Q \in ℂ$
63	60 62	syl	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to Q \in ℂ$
64		subcl	$⊢ (1 \in ℂ \land Q \in ℂ) \to 1 - Q \in ℂ$
65	59 63 64	sylancr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to 1 - Q \in ℂ$
66		simpr1	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P \in [0, 1]$
67	16	recnd	$⊢ P \in [0, 1] \to P \in ℂ$
68	66 67	syl	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P \in ℂ$
69		subcl	$⊢ (P \in ℂ \land 1 \in ℂ) \to P - 1 \in ℂ$
70	68 59 69	sylancl	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P - 1 \in ℂ$
71		simplll	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to A (i) \in ℂ$
72	70 71	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (P - 1) A (i) \in ℂ$
73	65 72	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) (P - 1) A (i) \in ℂ$
74	63 72	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to Q (P - 1) A (i) \in ℂ$
75	73 74	addcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) \in ℂ$
76		simpllr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to B (i) \in ℂ$
77	65 76	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) B (i) \in ℂ$
78		simplrl	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to C (i) \in ℂ$
79	63 78	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to Q C (i) \in ℂ$
80	77 79	addcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) B (i) + Q C (i) \in ℂ$
81	75 80	addcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i) \in ℂ$
82		simplrr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to T (i) \in ℂ$
83		simpr3	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P \neq 0$
84	81 68 82 83	divmuld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (\frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} = T (i) \leftrightarrow P T (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i))$
85	58 84	bitrid	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (T (i) = \frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} \leftrightarrow P T (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i))$
86		negsubdi2	$⊢ (1 \in ℂ \land P \in ℂ) \to - (1 - P) = P - 1$
87	59 68 86	sylancr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to - (1 - P) = P - 1$
88	87	oveq1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (- (1 - P)) A (i) = (P - 1) A (i)$
89		subcl	$⊢ (1 \in ℂ \land P \in ℂ) \to 1 - P \in ℂ$
90	59 68 89	sylancr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to 1 - P \in ℂ$
91	90 71	mulneg1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (- (1 - P)) A (i) = - (1 - P) A (i)$
92		npcan	$⊢ (1 \in ℂ \land Q \in ℂ) \to 1 - Q + Q = 1$
93	59 63 92	sylancr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to 1 - Q + Q = 1$
94	93	oveq1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q + Q) (P - 1) A (i) = 1 (P - 1) A (i)$
95	65 63 72	adddird	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q + Q) (P - 1) A (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i)$
96	72	mullidd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to 1 (P - 1) A (i) = (P - 1) A (i)$
97	94 95 96	3eqtr3rd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (P - 1) A (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i)$
98	88 91 97	3eqtr3d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to - (1 - P) A (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i)$
99	98	oveq2d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) B (i) + Q C (i) + (- (1 - P) A (i)) = (1 - Q) B (i) + Q C (i) + (1 - Q) (P - 1) A (i) + Q (P - 1) A (i)$
100	90 71	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) \in ℂ$
101	80 100	negsubd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) B (i) + Q C (i) + (- (1 - P) A (i)) = (1 - Q) B (i) + Q C (i) - (1 - P) A (i)$
102	80 75	addcomd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) B (i) + Q C (i) + (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)$
103	99 101 102	3eqtr3d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) B (i) + Q C (i) - (1 - P) A (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)$
104	103	eqeq1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - Q) B (i) + Q C (i) - (1 - P) A (i) = P T (i) \leftrightarrow (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i) = P T (i))$
105		eqcom	$⊢ (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i) = P T (i) \leftrightarrow P T (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)$
106	104 105	bitrdi	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - Q) B (i) + Q C (i) - (1 - P) A (i) = P T (i) \leftrightarrow P T (i) = (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i))$
107	85 106	bitr4d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (T (i) = \frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} \leftrightarrow (1 - Q) B (i) + Q C (i) - (1 - P) A (i) = P T (i))$
108	73 74 77 79	add4d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i) = (1 - Q) (P - 1) A (i) + (1 - Q) B (i) + Q (P - 1) A (i) + Q C (i)$
109	65 72 76	adddid	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) ((P - 1) A (i) + B (i)) = (1 - Q) (P - 1) A (i) + (1 - Q) B (i)$
110	63 72 78	adddid	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to Q ((P - 1) A (i) + C (i)) = Q (P - 1) A (i) + Q C (i)$
111	109 110	oveq12d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) ((P - 1) A (i) + B (i)) + Q ((P - 1) A (i) + C (i)) = (1 - Q) (P - 1) A (i) + (1 - Q) B (i) + Q (P - 1) A (i) + Q C (i)$
112	108 111	eqtr4d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i) = (1 - Q) ((P - 1) A (i) + B (i)) + Q ((P - 1) A (i) + C (i))$
113	112	oveq1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} = \frac{(1 - Q) ((P - 1) A (i) + B (i)) + Q ((P - 1) A (i) + C (i))}{P}$
114	72 76	addcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (P - 1) A (i) + B (i) \in ℂ$
115	65 114	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - Q) ((P - 1) A (i) + B (i)) \in ℂ$
116	72 78	addcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (P - 1) A (i) + C (i) \in ℂ$
117	63 116	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to Q ((P - 1) A (i) + C (i)) \in ℂ$
118	115 117 68 83	divdird	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(1 - Q) ((P - 1) A (i) + B (i)) + Q ((P - 1) A (i) + C (i))}{P} = (\frac{(1 - Q) ((P - 1) A (i) + B (i))}{P}) + (\frac{Q ((P - 1) A (i) + C (i))}{P})$
119	65 114 68 83	divassd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(1 - Q) ((P - 1) A (i) + B (i))}{P} = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P})$
120	63 116 68 83	divassd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{Q ((P - 1) A (i) + C (i))}{P} = Q (\frac{(P - 1) A (i) + C (i)}{P})$
121	119 120	oveq12d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (\frac{(1 - Q) ((P - 1) A (i) + B (i))}{P}) + (\frac{Q ((P - 1) A (i) + C (i))}{P}) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})$
122	113 118 121	3eqtrd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to \frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})$
123	122	eqeq2d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (T (i) = \frac{(1 - Q) (P - 1) A (i) + Q (P - 1) A (i) + (1 - Q) B (i) + Q C (i)}{P} \leftrightarrow T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P}))$
124	68 82	mulcld	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P T (i) \in ℂ$
125	80 100 124	subaddd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - Q) B (i) + Q C (i) - (1 - P) A (i) = P T (i) \leftrightarrow (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i))$
126	107 123 125	3bitr3rd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i) \leftrightarrow T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P}))$
127	126	biimpd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i) \to T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P}))$
128		npncan2	$⊢ (1 \in ℂ \land P \in ℂ) \to (1 - P) + P - 1 = 0$
129	59 68 128	sylancr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) + P - 1 = 0$
130	129	oveq1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - P) + P - 1) A (i) = 0 \cdot A (i)$
131	90 70 71	adddird	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - P) + P - 1) A (i) = (1 - P) A (i) + (P - 1) A (i)$
132		mul02	$⊢ A (i) \in ℂ \to 0 \cdot A (i) = 0$
133	132	ad3antrrr	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to 0 \cdot A (i) = 0$
134	130 131 133	3eqtr3d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) + (P - 1) A (i) = 0$
135	134	oveq1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) + (P - 1) A (i) + B (i) = 0 + B (i)$
136	100 72 76	addassd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) + (P - 1) A (i) + B (i) = (1 - P) A (i) + (P - 1) A (i) + B (i)$
137	76	addlidd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to 0 + B (i) = B (i)$
138	135 136 137	3eqtr3rd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to B (i) = (1 - P) A (i) + (P - 1) A (i) + B (i)$
139	114 68 83	divcan2d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P (\frac{(P - 1) A (i) + B (i)}{P}) = (P - 1) A (i) + B (i)$
140	139	oveq2d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) = (1 - P) A (i) + (P - 1) A (i) + B (i)$
141	138 140	eqtr4d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P})$
142	134	oveq1d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) + (P - 1) A (i) + C (i) = 0 + C (i)$
143	100 72 78	addassd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) + (P - 1) A (i) + C (i) = (1 - P) A (i) + (P - 1) A (i) + C (i)$
144	78	addlidd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to 0 + C (i) = C (i)$
145	142 143 144	3eqtr3rd	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to C (i) = (1 - P) A (i) + (P - 1) A (i) + C (i)$
146	116 68 83	divcan2d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to P (\frac{(P - 1) A (i) + C (i)}{P}) = (P - 1) A (i) + C (i)$
147	146	oveq2d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) = (1 - P) A (i) + (P - 1) A (i) + C (i)$
148	145 147	eqtr4d	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P})$
149	141 148	jca	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}))$
150	127 149	jctild	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i) \to ((B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P})) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
151		df-3an	$⊢ (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})) \leftrightarrow ((B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P})) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P}))$
152	150 151	imbitrrdi	$⊢ (((A (i) \in ℂ \land B (i) \in ℂ) \land (C (i) \in ℂ \land T (i) \in ℂ)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i) \to (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
153	57 152	sylan	$⊢ ((((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land i \in (1 \dots N)) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to ((1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i) \to (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
154	153	an32s	$⊢ ((((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \land i \in (1 \dots N)) \to ((1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i) \to (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
155	154	ralimdva	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0)) \to (\forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i) \to \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
156	155	3impia	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P}))$
157		fveq1	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \to x (i) = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) (i)$
158		fveq2	$⊢ k = i \to A (k) = A (i)$
159	158	oveq2d	$⊢ k = i \to (P - 1) A (k) = (P - 1) A (i)$
160		fveq2	$⊢ k = i \to B (k) = B (i)$
161	159 160	oveq12d	$⊢ k = i \to (P - 1) A (k) + B (k) = (P - 1) A (i) + B (i)$
162	161	oveq1d	$⊢ k = i \to \frac{(P - 1) A (k) + B (k)}{P} = \frac{(P - 1) A (i) + B (i)}{P}$
163		eqid	$⊢ (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P})$
164		ovex	$⊢ \frac{(P - 1) A (i) + B (i)}{P} \in V$
165	162 163 164	fvmpt	$⊢ i \in (1 \dots N) \to (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) (i) = \frac{(P - 1) A (i) + B (i)}{P}$
166	157 165	sylan9eq	$⊢ (x = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \land i \in (1 \dots N)) \to x (i) = \frac{(P - 1) A (i) + B (i)}{P}$
167		oveq2	$⊢ x (i) = \frac{(P - 1) A (i) + B (i)}{P} \to P x (i) = P (\frac{(P - 1) A (i) + B (i)}{P})$
168	167	oveq2d	$⊢ x (i) = \frac{(P - 1) A (i) + B (i)}{P} \to (1 - P) A (i) + P x (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P})$
169	168	eqeq2d	$⊢ x (i) = \frac{(P - 1) A (i) + B (i)}{P} \to (B (i) = (1 - P) A (i) + P x (i) \leftrightarrow B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}))$
170		oveq2	$⊢ x (i) = \frac{(P - 1) A (i) + B (i)}{P} \to (1 - Q) x (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P})$
171	170	oveq1d	$⊢ x (i) = \frac{(P - 1) A (i) + B (i)}{P} \to (1 - Q) x (i) + Q y (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i)$
172	171	eqeq2d	$⊢ x (i) = \frac{(P - 1) A (i) + B (i)}{P} \to (T (i) = (1 - Q) x (i) + Q y (i) \leftrightarrow T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i))$
173	169 172	3anbi13d	$⊢ x (i) = \frac{(P - 1) A (i) + B (i)}{P} \to ((B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i)) \leftrightarrow (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i)))$
174	166 173	syl	$⊢ (x = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \land i \in (1 \dots N)) \to ((B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i)) \leftrightarrow (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i)))$
175	174	ralbidva	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \to (\forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i)) \leftrightarrow \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i)))$
176		fveq1	$⊢ y = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \to y (i) = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) (i)$
177		fveq2	$⊢ k = i \to C (k) = C (i)$
178	159 177	oveq12d	$⊢ k = i \to (P - 1) A (k) + C (k) = (P - 1) A (i) + C (i)$
179	178	oveq1d	$⊢ k = i \to \frac{(P - 1) A (k) + C (k)}{P} = \frac{(P - 1) A (i) + C (i)}{P}$
180		eqid	$⊢ (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P})$
181		ovex	$⊢ \frac{(P - 1) A (i) + C (i)}{P} \in V$
182	179 180 181	fvmpt	$⊢ i \in (1 \dots N) \to (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) (i) = \frac{(P - 1) A (i) + C (i)}{P}$
183	176 182	sylan9eq	$⊢ (y = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \land i \in (1 \dots N)) \to y (i) = \frac{(P - 1) A (i) + C (i)}{P}$
184		oveq2	$⊢ y (i) = \frac{(P - 1) A (i) + C (i)}{P} \to P y (i) = P (\frac{(P - 1) A (i) + C (i)}{P})$
185	184	oveq2d	$⊢ y (i) = \frac{(P - 1) A (i) + C (i)}{P} \to (1 - P) A (i) + P y (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P})$
186	185	eqeq2d	$⊢ y (i) = \frac{(P - 1) A (i) + C (i)}{P} \to (C (i) = (1 - P) A (i) + P y (i) \leftrightarrow C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}))$
187		oveq2	$⊢ y (i) = \frac{(P - 1) A (i) + C (i)}{P} \to Q y (i) = Q (\frac{(P - 1) A (i) + C (i)}{P})$
188	187	oveq2d	$⊢ y (i) = \frac{(P - 1) A (i) + C (i)}{P} \to (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})$
189	188	eqeq2d	$⊢ y (i) = \frac{(P - 1) A (i) + C (i)}{P} \to (T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i) \leftrightarrow T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P}))$
190	186 189	3anbi23d	$⊢ y (i) = \frac{(P - 1) A (i) + C (i)}{P} \to ((B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i)) \leftrightarrow (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
191	183 190	syl	$⊢ (y = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \land i \in (1 \dots N)) \to ((B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i)) \leftrightarrow (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
192	191	ralbidva	$⊢ y = (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \to (\forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q y (i)) \leftrightarrow \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P})))$
193	175 192	rspc2ev	$⊢ ((k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + B (k)}{P}) \in 𝔼 (N) \land (k \in (1 \dots N) ⟼ \frac{(P - 1) A (k) + C (k)}{P}) \in 𝔼 (N) \land \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + B (i)}{P}) \land C (i) = (1 - P) A (i) + P (\frac{(P - 1) A (i) + C (i)}{P}) \land T (i) = (1 - Q) (\frac{(P - 1) A (i) + B (i)}{P}) + Q (\frac{(P - 1) A (i) + C (i)}{P}))) \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i))$
194	35 45 156 193	syl3anc	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i))$
195		oveq2	$⊢ r = P \to 1 - r = 1 - P$
196	195	oveq1d	$⊢ r = P \to (1 - r) A (i) = (1 - P) A (i)$
197		oveq1	$⊢ r = P \to r x (i) = P x (i)$
198	196 197	oveq12d	$⊢ r = P \to (1 - r) A (i) + r x (i) = (1 - P) A (i) + P x (i)$
199	198	eqeq2d	$⊢ r = P \to (B (i) = (1 - r) A (i) + r x (i) \leftrightarrow B (i) = (1 - P) A (i) + P x (i))$
200	199	3anbi1d	$⊢ r = P \to ((B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)))$
201	200	ralbidv	$⊢ r = P \to (\forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)))$
202	201	2rexbidv	$⊢ r = P \to (\exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)))$
203		oveq2	$⊢ s = P \to 1 - s = 1 - P$
204	203	oveq1d	$⊢ s = P \to (1 - s) A (i) = (1 - P) A (i)$
205		oveq1	$⊢ s = P \to s y (i) = P y (i)$
206	204 205	oveq12d	$⊢ s = P \to (1 - s) A (i) + s y (i) = (1 - P) A (i) + P y (i)$
207	206	eqeq2d	$⊢ s = P \to (C (i) = (1 - s) A (i) + s y (i) \leftrightarrow C (i) = (1 - P) A (i) + P y (i))$
208	207	3anbi2d	$⊢ s = P \to ((B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - u) x (i) + u y (i)))$
209	208	ralbidv	$⊢ s = P \to (\forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - u) x (i) + u y (i)))$
210	209	2rexbidv	$⊢ s = P \to (\exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - u) x (i) + u y (i)))$
211		oveq2	$⊢ u = Q \to 1 - u = 1 - Q$
212	211	oveq1d	$⊢ u = Q \to (1 - u) x (i) = (1 - Q) x (i)$
213		oveq1	$⊢ u = Q \to u y (i) = Q y (i)$
214	212 213	oveq12d	$⊢ u = Q \to (1 - u) x (i) + u y (i) = (1 - Q) x (i) + Q y (i)$
215	214	eqeq2d	$⊢ u = Q \to (T (i) = (1 - u) x (i) + u y (i) \leftrightarrow T (i) = (1 - Q) x (i) + Q y (i))$
216	215	3anbi3d	$⊢ u = Q \to ((B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i)))$
217	216	ralbidv	$⊢ u = Q \to (\forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i)))$
218	217	2rexbidv	$⊢ u = Q \to (\exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i)))$
219	202 210 218	rspc3ev	$⊢ ((P \in [0, 1] \land P \in [0, 1] \land Q \in [0, 1]) \land \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - P) A (i) + P x (i) \land C (i) = (1 - P) A (i) + P y (i) \land T (i) = (1 - Q) x (i) + Q y (i))) \to \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
220	1 1 2 194 219	syl31anc	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
221		rexcom	$⊢ \exists u \in [0, 1] \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
222	221	rexbii	$⊢ \exists s \in [0, 1] \exists u \in [0, 1] \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists s \in [0, 1] \exists x \in 𝔼 (N) \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
223		rexcom	$⊢ \exists s \in [0, 1] \exists x \in 𝔼 (N) \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
224	222 223	bitri	$⊢ \exists s \in [0, 1] \exists u \in [0, 1] \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
225	224	rexbii	$⊢ \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists r \in [0, 1] \exists x \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
226		rexcom	$⊢ \exists r \in [0, 1] \exists x \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
227		rexcom	$⊢ \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists y \in 𝔼 (N) \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
228	227	rexbii	$⊢ \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists s \in [0, 1] \exists y \in 𝔼 (N) \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
229		rexcom	$⊢ \exists s \in [0, 1] \exists y \in 𝔼 (N) \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists y \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
230	228 229	bitri	$⊢ \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists y \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
231	230	rexbii	$⊢ \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists r \in [0, 1] \exists y \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
232		rexcom	$⊢ \exists r \in [0, 1] \exists y \in 𝔼 (N) \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists y \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
233	231 232	bitri	$⊢ \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists y \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
234	233	rexbii	$⊢ \exists x \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
235	225 226 234	3bitri	$⊢ \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i)) \leftrightarrow \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$
236	220 235	sylib	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land T \in 𝔼 (N))) \land (P \in [0, 1] \land Q \in [0, 1] \land P \neq 0) \land \forall i \in (1 \dots N) (1 - P) A (i) + P T (i) = (1 - Q) B (i) + Q C (i)) \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists r \in [0, 1] \exists s \in [0, 1] \exists u \in [0, 1] \forall i \in (1 \dots N) (B (i) = (1 - r) A (i) + r x (i) \land C (i) = (1 - s) A (i) + s y (i) \land T (i) = (1 - u) x (i) + u y (i))$

Metamath Proof Explorer

Theorem axeuclidlem

Proof