axcontlem8

Description: Lemma for axcont . A point in D is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013)

	Ref	Expression
Hypotheses	axcontlem8.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	axcontlem8.2	$⊢ F = \{⟨x, t⟩ \| (x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)))\}$
Assertion	axcontlem8	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \to ((F (P) \leq F (Q) \land F (Q) \leq F (R)) \to Q Btwn ⟨P, R⟩)$

Proof

Step	Hyp	Ref	Expression
1		axcontlem8.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
2		axcontlem8.2	$⊢ F = \{⟨x, t⟩ \| (x \in D \land (t \in [0, +∞) \land \forall i \in (1 \dots N) x (i) = (1 - t) Z (i) + t U (i)))\}$
3	1 2	axcontlem6	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land P \in D) \to (F (P) \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i))$
4	3	ex	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to (P \in D \to (F (P) \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i)))$
5	1 2	axcontlem6	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land Q \in D) \to (F (Q) \in [0, +∞) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i))$
6	5	ex	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to (Q \in D \to (F (Q) \in [0, +∞) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)))$
7	1 2	axcontlem6	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land R \in D) \to (F (R) \in [0, +∞) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i))$
8	7	ex	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to (R \in D \to (F (R) \in [0, +∞) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i)))$
9	4 6 8	3anim123d	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to ((P \in D \land Q \in D \land R \in D) \to ((F (P) \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i)) \land (F (Q) \in [0, +∞) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)) \land (F (R) \in [0, +∞) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i))))$
10	9	imp	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \to ((F (P) \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i)) \land (F (Q) \in [0, +∞) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)) \land (F (R) \in [0, +∞) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i)))$
11	10	adantr	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to ((F (P) \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i)) \land (F (Q) \in [0, +∞) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)) \land (F (R) \in [0, +∞) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i)))$
12		3an6	$⊢ ((F (P) \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i)) \land (F (Q) \in [0, +∞) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)) \land (F (R) \in [0, +∞) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i))) \leftrightarrow ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞)) \land (\forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i)))$
13		0elunit	$⊢ 0 \in [0, 1]$
14		simplr1	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to F (P) \in [0, +∞)$
15	14	ad2antlr	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) \in [0, +∞)$
16		elrege0	$⊢ F (P) \in [0, +∞) \leftrightarrow (F (P) \in ℝ \land 0 \leq F (P))$
17	16	simplbi	$⊢ F (P) \in [0, +∞) \to F (P) \in ℝ$
18	15 17	syl	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) \in ℝ$
19	18	recnd	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) \in ℂ$
20		simprrl	$⊢ (F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) \leq F (Q)$
21	20	adantr	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) \leq F (Q)$
22		simprrr	$⊢ (F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (Q) \leq F (R)$
23		simpl	$⊢ (F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) = F (R)$
24	22 23	breqtrrd	$⊢ (F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (Q) \leq F (P)$
25	24	adantr	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (Q) \leq F (P)$
26		simplr2	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to F (Q) \in [0, +∞)$
27	26	ad2antlr	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (Q) \in [0, +∞)$
28		elrege0	$⊢ F (Q) \in [0, +∞) \leftrightarrow (F (Q) \in ℝ \land 0 \leq F (Q))$
29	28	simplbi	$⊢ F (Q) \in [0, +∞) \to F (Q) \in ℝ$
30	27 29	syl	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (Q) \in ℝ$
31	18 30	letri3d	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to (F (P) = F (Q) \leftrightarrow (F (P) \leq F (Q) \land F (Q) \leq F (P)))$
32	21 25 31	mpbir2and	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) = F (Q)$
33		simpll	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) = F (R)$
34		simpll2	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \to Z \in 𝔼 (N)$
35	34	adantr	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to Z \in 𝔼 (N)$
36	35	ad2antlr	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to Z \in 𝔼 (N)$
37		fveecn	$⊢ (Z \in 𝔼 (N) \land i \in (1 \dots N)) \to Z (i) \in ℂ$
38	36 37	sylancom	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to Z (i) \in ℂ$
39		simpll3	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \to U \in 𝔼 (N)$
40	39	adantr	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to U \in 𝔼 (N)$
41	40	ad2antlr	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to U \in 𝔼 (N)$
42		fveecn	$⊢ (U \in 𝔼 (N) \land i \in (1 \dots N)) \to U (i) \in ℂ$
43	41 42	sylancom	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to U (i) \in ℂ$
44		ax-1cn	$⊢ 1 \in ℂ$
45		simpl	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (P) \in ℂ$
46		subcl	$⊢ (1 \in ℂ \land F (P) \in ℂ) \to 1 - F (P) \in ℂ$
47	44 45 46	sylancr	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 - F (P) \in ℂ$
48		simprl	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to Z (i) \in ℂ$
49	47 48	mulcld	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (P)) Z (i) \in ℂ$
50		mulcl	$⊢ (F (P) \in ℂ \land U (i) \in ℂ) \to F (P) U (i) \in ℂ$
51	50	adantrl	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (P) U (i) \in ℂ$
52	49 51	addcld	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (P)) Z (i) + F (P) U (i) \in ℂ$
53	52	mulid2d	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 ((1 - F (P)) Z (i) + F (P) U (i)) = (1 - F (P)) Z (i) + F (P) U (i)$
54	52	mul02d	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i)) = 0$
55	53 54	oveq12d	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i)) = (1 - F (P)) Z (i) + F (P) U (i) + 0$
56	52	addid1d	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (P)) Z (i) + F (P) U (i) + 0 = (1 - F (P)) Z (i) + F (P) U (i)$
57	55 56	eqtr2d	$⊢ (F (P) \in ℂ \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (P)) Z (i) + F (P) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i))$
58	57	3adant2	$⊢ (F (P) \in ℂ \land (F (P) = F (Q) \land F (P) = F (R)) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (P)) Z (i) + F (P) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i))$
59		oveq2	$⊢ F (P) = F (Q) \to 1 - F (P) = 1 - F (Q)$
60	59	oveq1d	$⊢ F (P) = F (Q) \to (1 - F (P)) Z (i) = (1 - F (Q)) Z (i)$
61		oveq1	$⊢ F (P) = F (Q) \to F (P) U (i) = F (Q) U (i)$
62	60 61	oveq12d	$⊢ F (P) = F (Q) \to (1 - F (P)) Z (i) + F (P) U (i) = (1 - F (Q)) Z (i) + F (Q) U (i)$
63		oveq2	$⊢ F (P) = F (R) \to 1 - F (P) = 1 - F (R)$
64	63	oveq1d	$⊢ F (P) = F (R) \to (1 - F (P)) Z (i) = (1 - F (R)) Z (i)$
65		oveq1	$⊢ F (P) = F (R) \to F (P) U (i) = F (R) U (i)$
66	64 65	oveq12d	$⊢ F (P) = F (R) \to (1 - F (P)) Z (i) + F (P) U (i) = (1 - F (R)) Z (i) + F (R) U (i)$
67	66	oveq2d	$⊢ F (P) = F (R) \to 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i)) = 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))$
68	67	oveq2d	$⊢ F (P) = F (R) \to 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i)) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))$
69	62 68	eqeqan12d	$⊢ (F (P) = F (Q) \land F (P) = F (R)) \to ((1 - F (P)) Z (i) + F (P) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i)) \leftrightarrow (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i)))$
70	69	3ad2ant2	$⊢ (F (P) \in ℂ \land (F (P) = F (Q) \land F (P) = F (R)) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to ((1 - F (P)) Z (i) + F (P) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (P)) Z (i) + F (P) U (i)) \leftrightarrow (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i)))$
71	58 70	mpbid	$⊢ (F (P) \in ℂ \land (F (P) = F (Q) \land F (P) = F (R)) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))$
72	19 32 33 38 43 71	syl122anc	$⊢ ((F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))$
73	72	ralrimiva	$⊢ (F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))$
74		oveq2	$⊢ t = 0 \to 1 - t = 1 - 0$
75		1m0e1	$⊢ 1 - 0 = 1$
76	74 75	eqtrdi	$⊢ t = 0 \to 1 - t = 1$
77	76	oveq1d	$⊢ t = 0 \to (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) = 1 ((1 - F (P)) Z (i) + F (P) U (i))$
78		oveq1	$⊢ t = 0 \to t ((1 - F (R)) Z (i) + F (R) U (i)) = 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))$
79	77 78	oveq12d	$⊢ t = 0 \to (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))$
80	79	eqeq2d	$⊢ t = 0 \to ((1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) \leftrightarrow (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i)))$
81	80	ralbidv	$⊢ t = 0 \to (\forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) \leftrightarrow \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i)))$
82	81	rspcev	$⊢ (0 \in [0, 1] \land \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = 1 ((1 - F (P)) Z (i) + F (P) U (i)) + 0 \cdot ((1 - F (R)) Z (i) + F (R) U (i))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))$
83	13 73 82	sylancr	$⊢ (F (P) = F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))$
84	83	ex	$⊢ F (P) = F (R) \to (((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)))$
85	26	adantl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (Q) \in [0, +∞)$
86	85 29	syl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (Q) \in ℝ$
87		simplr3	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to F (R) \in [0, +∞)$
88	87	adantl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (R) \in [0, +∞)$
89		elrege0	$⊢ F (R) \in [0, +∞) \leftrightarrow (F (R) \in ℝ \land 0 \leq F (R))$
90	89	simplbi	$⊢ F (R) \in [0, +∞) \to F (R) \in ℝ$
91	88 90	syl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (R) \in ℝ$
92	14	adantl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) \in [0, +∞)$
93	92 17	syl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) \in ℝ$
94		simprrr	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (Q) \leq F (R)$
95	86 91 93 94	lesub1dd	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (Q) - F (P) \leq F (R) - F (P)$
96	86 93	resubcld	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (Q) - F (P) \in ℝ$
97		simprrl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) \leq F (Q)$
98	86 93	subge0d	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to (0 \leq F (Q) - F (P) \leftrightarrow F (P) \leq F (Q))$
99	97 98	mpbird	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to 0 \leq F (Q) - F (P)$
100	91 93	resubcld	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (R) - F (P) \in ℝ$
101	93 86 91 97 94	letrd	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) \leq F (R)$
102		simpl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) \neq F (R)$
103	102	necomd	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (R) \neq F (P)$
104	93 91 101 103	leneltd	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to F (P) < F (R)$
105	93 91	posdifd	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to (F (P) < F (R) \leftrightarrow 0 < F (R) - F (P))$
106	104 105	mpbid	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to 0 < F (R) - F (P)$
107		divelunit	$⊢ ((F (Q) - F (P) \in ℝ \land 0 \leq F (Q) - F (P)) \land (F (R) - F (P) \in ℝ \land 0 < F (R) - F (P))) \to (\frac{F (Q) - F (P)}{F (R) - F (P)} \in [0, 1] \leftrightarrow F (Q) - F (P) \leq F (R) - F (P))$
108	96 99 100 106 107	syl22anc	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to (\frac{F (Q) - F (P)}{F (R) - F (P)} \in [0, 1] \leftrightarrow F (Q) - F (P) \leq F (R) - F (P))$
109	95 108	mpbird	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to \frac{F (Q) - F (P)}{F (R) - F (P)} \in [0, 1]$
110	14	ad2antlr	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) \in [0, +∞)$
111	17	recnd	$⊢ F (P) \in [0, +∞) \to F (P) \in ℂ$
112	110 111	syl	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) \in ℂ$
113		simpll	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (P) \neq F (R)$
114	26	ad2antlr	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (Q) \in [0, +∞)$
115	29	recnd	$⊢ F (Q) \in [0, +∞) \to F (Q) \in ℂ$
116	114 115	syl	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (Q) \in ℂ$
117	87	ad2antlr	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (R) \in [0, +∞)$
118	90	recnd	$⊢ F (R) \in [0, +∞) \to F (R) \in ℂ$
119	117 118	syl	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to F (R) \in ℂ$
120	34	ad2antrl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to Z \in 𝔼 (N)$
121	120 37	sylan	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to Z (i) \in ℂ$
122	39	ad2antrl	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to U \in 𝔼 (N)$
123	122 42	sylan	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to U (i) \in ℂ$
124		simp2r	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) \in ℂ$
125		simp2l	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) \in ℂ$
126	124 125	subcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) - F (Q) \in ℂ$
127		simp1l	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (P) \in ℂ$
128	44 127 46	sylancr	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 - F (P) \in ℂ$
129	126 128	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) (1 - F (P)) \in ℂ$
130	125 127	subcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) - F (P) \in ℂ$
131		subcl	$⊢ (1 \in ℂ \land F (R) \in ℂ) \to 1 - F (R) \in ℂ$
132	44 124 131	sylancr	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 - F (R) \in ℂ$
133	130 132	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (Q) - F (P)) (1 - F (R)) \in ℂ$
134	124 127	subcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) - F (P) \in ℂ$
135		simp1r	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (P) \neq F (R)$
136	135	necomd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) \neq F (P)$
137	124 127 136	subne0d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) - F (P) \neq 0$
138	129 133 134 137	divdird	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R))}{F (R) - F (P)} = (\frac{(F (R) - F (Q)) (1 - F (P))}{F (R) - F (P)}) + (\frac{(F (Q) - F (P)) (1 - F (R))}{F (R) - F (P)})$
139	134	mulid1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (P)) \cdot 1 = F (R) - F (P)$
140	134 125	mulcomd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (P)) F (Q) = F (Q) (F (R) - F (P))$
141	125 124 127	subdid	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) (F (R) - F (P)) = F (Q) F (R) - F (Q) F (P)$
142	140 141	eqtrd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (P)) F (Q) = F (Q) F (R) - F (Q) F (P)$
143	139 142	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (P)) \cdot 1 - (F (R) - F (P)) F (Q) = F (R) - F (P) - (F (Q) F (R) - F (Q) F (P))$
144		subdi	$⊢ (F (R) - F (P) \in ℂ \land 1 \in ℂ \land F (Q) \in ℂ) \to (F (R) - F (P)) (1 - F (Q)) = (F (R) - F (P)) \cdot 1 - (F (R) - F (P)) F (Q)$
145	44 144	mp3an2	$⊢ (F (R) - F (P) \in ℂ \land F (Q) \in ℂ) \to (F (R) - F (P)) (1 - F (Q)) = (F (R) - F (P)) \cdot 1 - (F (R) - F (P)) F (Q)$
146	134 125 145	syl2anc	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (P)) (1 - F (Q)) = (F (R) - F (P)) \cdot 1 - (F (R) - F (P)) F (Q)$
147		subdi	$⊢ (F (R) - F (Q) \in ℂ \land 1 \in ℂ \land F (P) \in ℂ) \to (F (R) - F (Q)) (1 - F (P)) = (F (R) - F (Q)) \cdot 1 - (F (R) - F (Q)) F (P)$
148	44 147	mp3an2	$⊢ (F (R) - F (Q) \in ℂ \land F (P) \in ℂ) \to (F (R) - F (Q)) (1 - F (P)) = (F (R) - F (Q)) \cdot 1 - (F (R) - F (Q)) F (P)$
149	126 127 148	syl2anc	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) (1 - F (P)) = (F (R) - F (Q)) \cdot 1 - (F (R) - F (Q)) F (P)$
150	126	mulid1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) \cdot 1 = F (R) - F (Q)$
151	124 125 127	subdird	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) F (P) = F (R) F (P) - F (Q) F (P)$
152	124 127	mulcomd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) F (P) = F (P) F (R)$
153	152	oveq1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) F (P) - F (Q) F (P) = F (P) F (R) - F (Q) F (P)$
154	151 153	eqtrd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) F (P) = F (P) F (R) - F (Q) F (P)$
155	150 154	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) \cdot 1 - (F (R) - F (Q)) F (P) = F (R) - F (Q) - (F (P) F (R) - F (Q) F (P))$
156	149 155	eqtrd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) (1 - F (P)) = F (R) - F (Q) - (F (P) F (R) - F (Q) F (P))$
157		subdi	$⊢ (F (Q) - F (P) \in ℂ \land 1 \in ℂ \land F (R) \in ℂ) \to (F (Q) - F (P)) (1 - F (R)) = (F (Q) - F (P)) \cdot 1 - (F (Q) - F (P)) F (R)$
158	44 157	mp3an2	$⊢ (F (Q) - F (P) \in ℂ \land F (R) \in ℂ) \to (F (Q) - F (P)) (1 - F (R)) = (F (Q) - F (P)) \cdot 1 - (F (Q) - F (P)) F (R)$
159	130 124 158	syl2anc	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (Q) - F (P)) (1 - F (R)) = (F (Q) - F (P)) \cdot 1 - (F (Q) - F (P)) F (R)$
160	130	mulid1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (Q) - F (P)) \cdot 1 = F (Q) - F (P)$
161	125 127 124	subdird	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (Q) - F (P)) F (R) = F (Q) F (R) - F (P) F (R)$
162	160 161	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (Q) - F (P)) \cdot 1 - (F (Q) - F (P)) F (R) = F (Q) - F (P) - (F (Q) F (R) - F (P) F (R))$
163	159 162	eqtrd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (Q) - F (P)) (1 - F (R)) = F (Q) - F (P) - (F (Q) F (R) - F (P) F (R))$
164	156 163	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R)) = (F (R) - F (Q) - (F (P) F (R) - F (Q) F (P))) + (F (Q) - F (P)) - (F (Q) F (R) - F (P) F (R))$
165	127 124	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (P) F (R) \in ℂ$
166	125 127	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) F (P) \in ℂ$
167	165 166	subcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (P) F (R) - F (Q) F (P) \in ℂ$
168		mulcl	$⊢ (F (Q) \in ℂ \land F (R) \in ℂ) \to F (Q) F (R) \in ℂ$
169	168	3ad2ant2	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) F (R) \in ℂ$
170	169 165	subcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) F (R) - F (P) F (R) \in ℂ$
171	126 130 167 170	addsub4d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) + (F (Q) - F (P)) - ((F (P) F (R) - F (Q) F (P)) + F (Q) F (R) - F (P) F (R)) = (F (R) - F (Q) - (F (P) F (R) - F (Q) F (P))) + (F (Q) - F (P)) - (F (Q) F (R) - F (P) F (R))$
172	124 125 127	npncand	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) + F (Q) - F (P) = F (R) - F (P)$
173	165 166 169	npncan3d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (P) F (R) - F (Q) F (P)) + F (Q) F (R) - F (P) F (R) = F (Q) F (R) - F (Q) F (P)$
174	172 173	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) + (F (Q) - F (P)) - ((F (P) F (R) - F (Q) F (P)) + F (Q) F (R) - F (P) F (R)) = F (R) - F (P) - (F (Q) F (R) - F (Q) F (P))$
175	164 171 174	3eqtr2d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R)) = F (R) - F (P) - (F (Q) F (R) - F (Q) F (P))$
176	143 146 175	3eqtr4d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (P)) (1 - F (Q)) = (F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R))$
177	129 133	addcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R)) \in ℂ$
178		subcl	$⊢ (1 \in ℂ \land F (Q) \in ℂ) \to 1 - F (Q) \in ℂ$
179	44 125 178	sylancr	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 - F (Q) \in ℂ$
180	177 134 179 137	divmuld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{(F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R))}{F (R) - F (P)} = 1 - F (Q) \leftrightarrow (F (R) - F (P)) (1 - F (Q)) = (F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R)))$
181	176 180	mpbird	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) (1 - F (P)) + (F (Q) - F (P)) (1 - F (R))}{F (R) - F (P)} = 1 - F (Q)$
182	126 128 134 137	div23d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) (1 - F (P))}{F (R) - F (P)} = (\frac{F (R) - F (Q)}{F (R) - F (P)}) (1 - F (P))$
183	134 130 134 137	divsubdird	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{F (R) - F (P) - (F (Q) - F (P))}{F (R) - F (P)} = (\frac{F (R) - F (P)}{F (R) - F (P)}) - (\frac{F (Q) - F (P)}{F (R) - F (P)})$
184	124 125 127	nnncan2d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) - F (P) - (F (Q) - F (P)) = F (R) - F (Q)$
185	184	oveq1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{F (R) - F (P) - (F (Q) - F (P))}{F (R) - F (P)} = \frac{F (R) - F (Q)}{F (R) - F (P)}$
186	134 137	dividd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{F (R) - F (P)}{F (R) - F (P)} = 1$
187	186	oveq1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (R) - F (P)}{F (R) - F (P)}) - (\frac{F (Q) - F (P)}{F (R) - F (P)}) = 1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})$
188	183 185 187	3eqtr3d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{F (R) - F (Q)}{F (R) - F (P)} = 1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})$
189	188	oveq1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (R) - F (Q)}{F (R) - F (P)}) (1 - F (P)) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P))$
190	182 189	eqtrd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) (1 - F (P))}{F (R) - F (P)} = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P))$
191	130 132 134 137	div23d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (Q) - F (P)) (1 - F (R))}{F (R) - F (P)} = (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))$
192	190 191	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{(F (R) - F (Q)) (1 - F (P))}{F (R) - F (P)}) + (\frac{(F (Q) - F (P)) (1 - F (R))}{F (R) - F (P)}) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))$
193	138 181 192	3eqtr3d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 - F (Q) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))$
194	193	oveq1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (Q)) Z (i) = ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))) Z (i)$
195	126 127	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) F (P) \in ℂ$
196	130 124	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (Q) - F (P)) F (R) \in ℂ$
197	195 196 134 137	divdird	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) F (P) + (F (Q) - F (P)) F (R)}{F (R) - F (P)} = (\frac{(F (R) - F (Q)) F (P)}{F (R) - F (P)}) + (\frac{(F (Q) - F (P)) F (R)}{F (R) - F (P)})$
198	154 161	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) F (P) + (F (Q) - F (P)) F (R) = (F (P) F (R) - F (Q) F (P)) + F (Q) F (R) - F (P) F (R)$
199	173 198 142	3eqtr4rd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (P)) F (Q) = (F (R) - F (Q)) F (P) + (F (Q) - F (P)) F (R)$
200	195 196	addcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (F (R) - F (Q)) F (P) + (F (Q) - F (P)) F (R) \in ℂ$
201	200 134 125 137	divmuld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{(F (R) - F (Q)) F (P) + (F (Q) - F (P)) F (R)}{F (R) - F (P)} = F (Q) \leftrightarrow (F (R) - F (P)) F (Q) = (F (R) - F (Q)) F (P) + (F (Q) - F (P)) F (R))$
202	199 201	mpbird	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) F (P) + (F (Q) - F (P)) F (R)}{F (R) - F (P)} = F (Q)$
203	126 127 134 137	div23d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) F (P)}{F (R) - F (P)} = (\frac{F (R) - F (Q)}{F (R) - F (P)}) F (P)$
204	188	oveq1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (R) - F (Q)}{F (R) - F (P)}) F (P) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P)$
205	203 204	eqtrd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (R) - F (Q)) F (P)}{F (R) - F (P)} = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P)$
206	130 124 134 137	div23d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{(F (Q) - F (P)) F (R)}{F (R) - F (P)} = (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)$
207	205 206	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{(F (R) - F (Q)) F (P)}{F (R) - F (P)}) + (\frac{(F (Q) - F (P)) F (R)}{F (R) - F (P)}) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)$
208	197 202 207	3eqtr3d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)$
209	208	oveq1d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (Q) U (i) = ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)) U (i)$
210	194 209	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (Q)) Z (i) + F (Q) U (i) = ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))) Z (i) + ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)) U (i)$
211	130 134 137	divcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to \frac{F (Q) - F (P)}{F (R) - F (P)} \in ℂ$
212		subcl	$⊢ (1 \in ℂ \land \frac{F (Q) - F (P)}{F (R) - F (P)} \in ℂ) \to 1 - (\frac{F (Q) - F (P)}{F (R) - F (P)}) \in ℂ$
213	44 211 212	sylancr	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to 1 - (\frac{F (Q) - F (P)}{F (R) - F (P)}) \in ℂ$
214		simp3l	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to Z (i) \in ℂ$
215	128 214	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (P)) Z (i) \in ℂ$
216	213 215	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) \in ℂ$
217	132 214	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (R)) Z (i) \in ℂ$
218	211 217	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) \in ℂ$
219		simp3r	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to U (i) \in ℂ$
220	127 219	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (P) U (i) \in ℂ$
221	213 220	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) \in ℂ$
222	124 219	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to F (R) U (i) \in ℂ$
223	211 222	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i) \in ℂ$
224	216 218 221 223	add4d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) + (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i)$
225	213 128	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) \in ℂ$
226	211 132	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) \in ℂ$
227	213 128 214	mulassd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i)$
228	211 132 214	mulassd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) = (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i)$
229	227 228	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i)$
230	225 214 226 229	joinlmuladdmuld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))) Z (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i)$
231	213 127	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) \in ℂ$
232	211 124	mulcld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) \in ℂ$
233	213 127 219	mulassd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i)$
234	211 124 219	mulassd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i) = (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i)$
235	233 234	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i)$
236	231 219 232 235	joinlmuladdmuld	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i)$
237	230 236	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))) Z (i) + ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) + (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i)$
238	213 215 220	adddid	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i)$
239	211 217 222	adddid	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i)) = (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i)$
240	238 239	oveq12d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i)) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) Z (i) + (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) U (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R)) Z (i) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R) U (i)$
241	224 237 240	3eqtr4rd	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i)) = ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) (1 - F (P)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) (1 - F (R))) Z (i) + ((1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) F (P) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) F (R)) U (i)$
242	210 241	eqtr4d	$⊢ ((F (P) \in ℂ \land F (P) \neq F (R)) \land (F (Q) \in ℂ \land F (R) \in ℂ) \land (Z (i) \in ℂ \land U (i) \in ℂ)) \to (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i))$
243	112 113 116 119 121 123 242	syl222anc	$⊢ ((F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \land i \in (1 \dots N)) \to (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i))$
244	243	ralrimiva	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i))$
245		oveq2	$⊢ t = \frac{F (Q) - F (P)}{F (R) - F (P)} \to 1 - t = 1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})$
246	245	oveq1d	$⊢ t = \frac{F (Q) - F (P)}{F (R) - F (P)} \to (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i))$
247		oveq1	$⊢ t = \frac{F (Q) - F (P)}{F (R) - F (P)} \to t ((1 - F (R)) Z (i) + F (R) U (i)) = (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i))$
248	246 247	oveq12d	$⊢ t = \frac{F (Q) - F (P)}{F (R) - F (P)} \to (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i))$
249	248	eqeq2d	$⊢ t = \frac{F (Q) - F (P)}{F (R) - F (P)} \to ((1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) \leftrightarrow (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i)))$
250	249	ralbidv	$⊢ t = \frac{F (Q) - F (P)}{F (R) - F (P)} \to (\forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) \leftrightarrow \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i)))$
251	250	rspcev	$⊢ (\frac{F (Q) - F (P)}{F (R) - F (P)} \in [0, 1] \land \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - (\frac{F (Q) - F (P)}{F (R) - F (P)})) ((1 - F (P)) Z (i) + F (P) U (i)) + (\frac{F (Q) - F (P)}{F (R) - F (P)}) ((1 - F (R)) Z (i) + F (R) U (i))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))$
252	109 244 251	syl2anc	$⊢ (F (P) \neq F (R) \land ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R)))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))$
253	252	ex	$⊢ F (P) \neq F (R) \to (((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)))$
254	84 253	pm2.61ine	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))$
255		r19.26-3	$⊢ \forall i \in (1 \dots N) (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \leftrightarrow (\forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i))$
256		simp2	$⊢ (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)$
257		oveq2	$⊢ P (i) = (1 - F (P)) Z (i) + F (P) U (i) \to (1 - t) P (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i))$
258		oveq2	$⊢ R (i) = (1 - F (R)) Z (i) + F (R) U (i) \to t R (i) = t ((1 - F (R)) Z (i) + F (R) U (i))$
259	257 258	oveqan12d	$⊢ (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to (1 - t) P (i) + t R (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))$
260	259	3adant2	$⊢ (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to (1 - t) P (i) + t R (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))$
261	256 260	eqeq12d	$⊢ (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to (Q (i) = (1 - t) P (i) + t R (i) \leftrightarrow (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)))$
262	261	ralimi	$⊢ \forall i \in (1 \dots N) (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to \forall i \in (1 \dots N) (Q (i) = (1 - t) P (i) + t R (i) \leftrightarrow (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)))$
263		ralbi	$⊢ \forall i \in (1 \dots N) (Q (i) = (1 - t) P (i) + t R (i) \leftrightarrow (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i))) \to (\forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i) \leftrightarrow \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)))$
264	262 263	syl	$⊢ \forall i \in (1 \dots N) (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to (\forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i) \leftrightarrow \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)))$
265	264	rexbidv	$⊢ \forall i \in (1 \dots N) (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i) \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)))$
266	265	biimprcd	$⊢ \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) \to (\forall i \in (1 \dots N) (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
267	255 266	syl5bir	$⊢ \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (Q)) Z (i) + F (Q) U (i) = (1 - t) ((1 - F (P)) Z (i) + F (P) U (i)) + t ((1 - F (R)) Z (i) + F (R) U (i)) \to ((\forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
268	254 267	syl	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to ((\forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
269	268	an32s	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞))) \to ((\forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i)) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
270	269	expimpd	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to (((F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞)) \land (\forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
271	270	adantlr	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to (((F (P) \in [0, +∞) \land F (Q) \in [0, +∞) \land F (R) \in [0, +∞)) \land (\forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
272	12 271	syl5bi	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to (((F (P) \in [0, +∞) \land \forall i \in (1 \dots N) P (i) = (1 - F (P)) Z (i) + F (P) U (i)) \land (F (Q) \in [0, +∞) \land \forall i \in (1 \dots N) Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)) \land (F (R) \in [0, +∞) \land \forall i \in (1 \dots N) R (i) = (1 - F (R)) Z (i) + F (R) U (i))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
273	11 272	mpd	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i)$
274		simpl1	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to N \in ℕ$
275	1	ssrab3	$⊢ D \subseteq 𝔼 (N)$
276	275	sseli	$⊢ Q \in D \to Q \in 𝔼 (N)$
277	275	sseli	$⊢ P \in D \to P \in 𝔼 (N)$
278	275	sseli	$⊢ R \in D \to R \in 𝔼 (N)$
279	276 277 278	3anim123i	$⊢ (Q \in D \land P \in D \land R \in D) \to (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land R \in 𝔼 (N))$
280	279	3com12	$⊢ (P \in D \land Q \in D \land R \in D) \to (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land R \in 𝔼 (N))$
281		brbtwn	$⊢ (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land R \in 𝔼 (N)) \to (Q Btwn ⟨P, R⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
282	281	adantl	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land R \in 𝔼 (N))) \to (Q Btwn ⟨P, R⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
283	274 280 282	syl2an	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \to (Q Btwn ⟨P, R⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
284	283	adantr	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to (Q Btwn ⟨P, R⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) Q (i) = (1 - t) P (i) + t R (i))$
285	273 284	mpbird	$⊢ ((((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \land (F (P) \leq F (Q) \land F (Q) \leq F (R))) \to Q Btwn ⟨P, R⟩$
286	285	ex	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D \land R \in D)) \to ((F (P) \leq F (Q) \land F (Q) \leq F (R)) \to Q Btwn ⟨P, R⟩)$

Metamath Proof Explorer

Theorem axcontlem8

Proof