axcontlem7

Description: Lemma for axcont . Given two points in D , one preceeds the other iff its scaling constant is less than the other point's. (Contributed by Scott Fenton, 18-Jun-2013)

	Ref	Expression
Hypotheses	axcontlem7.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
	axcontlem7.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	axcontlem7	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D)) \to (P Btwn ⟨Z, Q⟩ \leftrightarrow F (P) \leq F (Q))$

Proof

Step	Hyp	Ref	Expression
1		axcontlem7.1	$⊢ D = \{p \in 𝔼 (N) \| (U Btwn ⟨Z, p⟩ \lor p Btwn ⟨Z, U⟩)\}$
2		axcontlem7.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	ssrab3	$⊢ D \subseteq 𝔼 (N)$
4	3	sseli	$⊢ P \in D \to P \in 𝔼 (N)$
5	4	ad2antrl	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D)) \to P \in 𝔼 (N)$
6		simpll2	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D)) \to Z \in 𝔼 (N)$
7	3	sseli	$⊢ Q \in D \to Q \in 𝔼 (N)$
8	7	ad2antll	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D)) \to Q \in 𝔼 (N)$
9		brbtwn	$⊢ (P \in 𝔼 (N) \land Z \in 𝔼 (N) \land Q \in 𝔼 (N)) \to (P Btwn ⟨Z, Q⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i))$
10	5 6 8 9	syl3anc	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D)) \to (P Btwn ⟨Z, Q⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i))$
11	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))$
12	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))$
13	11 12	anim12dan	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \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)))$
14		an4	$⊢ ((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))) \leftrightarrow ((F (P) \in [0, +∞) \land F (Q) \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)))$
15		r19.26	$⊢ \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)) \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))$
16	15	anbi2i	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land \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))) \leftrightarrow ((F (P) \in [0, +∞) \land F (Q) \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)))$
17	14 16	bitr4i	$⊢ ((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))) \leftrightarrow ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land \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)))$
18		id	$⊢ P (i) = (1 - F (P)) Z (i) + F (P) U (i) \to P (i) = (1 - F (P)) Z (i) + F (P) U (i)$
19		oveq2	$⊢ Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \to t Q (i) = t ((1 - F (Q)) Z (i) + F (Q) U (i))$
20	19	oveq2d	$⊢ Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i) \to (1 - t) Z (i) + t Q (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i))$
21	18 20	eqeqan12d	$⊢ (P (i) = (1 - F (P)) Z (i) + F (P) U (i) \land Q (i) = (1 - F (Q)) Z (i) + F (Q) U (i)) \to (P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)))$
22	21	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)) \to \forall i \in (1 \dots N) (P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)))$
23		ralbi	$⊢ \forall i \in (1 \dots N) (P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i))) \to (\forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow \forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)))$
24	22 23	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)) \to (\forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow \forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)))$
25	24	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)) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)))$
26		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 t \in [0, 1])) \to Z \in 𝔼 (N)$
27		fveecn	$⊢ (Z \in 𝔼 (N) \land i \in (1 \dots N)) \to Z (i) \in ℂ$
28	26 27	sylan	$⊢ ((((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 t \in [0, 1])) \land i \in (1 \dots N)) \to Z (i) \in ℂ$
29		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 t \in [0, 1])) \to U \in 𝔼 (N)$
30		fveecn	$⊢ (U \in 𝔼 (N) \land i \in (1 \dots N)) \to U (i) \in ℂ$
31	29 30	sylan	$⊢ ((((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 t \in [0, 1])) \land i \in (1 \dots N)) \to U (i) \in ℂ$
32		elicc01	$⊢ t \in [0, 1] \leftrightarrow (t \in ℝ \land 0 \leq t \land t \leq 1)$
33	32	simp1bi	$⊢ t \in [0, 1] \to t \in ℝ$
34	33	recnd	$⊢ t \in [0, 1] \to t \in ℂ$
35	34	ad2antll	$⊢ (((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 t \in [0, 1])) \to t \in ℂ$
36	35	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 t \in [0, 1])) \land i \in (1 \dots N)) \to t \in ℂ$
37		elrege0	$⊢ F (P) \in [0, +∞) \leftrightarrow (F (P) \in ℝ \land 0 \leq F (P))$
38	37	simplbi	$⊢ F (P) \in [0, +∞) \to F (P) \in ℝ$
39	38	recnd	$⊢ F (P) \in [0, +∞) \to F (P) \in ℂ$
40	39	adantr	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to F (P) \in ℂ$
41	40	ad2antrl	$⊢ (((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 t \in [0, 1])) \to F (P) \in ℂ$
42	41	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 t \in [0, 1])) \land i \in (1 \dots N)) \to F (P) \in ℂ$
43		elrege0	$⊢ F (Q) \in [0, +∞) \leftrightarrow (F (Q) \in ℝ \land 0 \leq F (Q))$
44	43	simplbi	$⊢ F (Q) \in [0, +∞) \to F (Q) \in ℝ$
45	44	recnd	$⊢ F (Q) \in [0, +∞) \to F (Q) \in ℂ$
46	45	adantl	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to F (Q) \in ℂ$
47	46	ad2antrl	$⊢ (((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 t \in [0, 1])) \to F (Q) \in ℂ$
48	47	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 t \in [0, 1])) \land i \in (1 \dots N)) \to F (Q) \in ℂ$
49		ax-1cn	$⊢ 1 \in ℂ$
50		simpr1	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t \in ℂ$
51		simpr3	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to F (Q) \in ℂ$
52	50 51	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t F (Q) \in ℂ$
53		subcl	$⊢ (1 \in ℂ \land t F (Q) \in ℂ) \to 1 - t F (Q) \in ℂ$
54	49 52 53	sylancr	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to 1 - t F (Q) \in ℂ$
55		subcl	$⊢ (1 \in ℂ \land F (P) \in ℂ) \to 1 - F (P) \in ℂ$
56	49 55	mpan	$⊢ F (P) \in ℂ \to 1 - F (P) \in ℂ$
57	56	3ad2ant2	$⊢ (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ) \to 1 - F (P) \in ℂ$
58	57	adantl	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to 1 - F (P) \in ℂ$
59		simpll	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to Z (i) \in ℂ$
60	54 58 59	subdird	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t F (Q) - (1 - F (P))) Z (i) = (1 - t F (Q)) Z (i) - (1 - F (P)) Z (i)$
61		simpr2	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to F (P) \in ℂ$
62		nnncan1	$⊢ (1 \in ℂ \land t F (Q) \in ℂ \land F (P) \in ℂ) \to 1 - t F (Q) - (1 - F (P)) = F (P) - t F (Q)$
63	49 52 61 62	mp3an2i	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to 1 - t F (Q) - (1 - F (P)) = F (P) - t F (Q)$
64	63	oveq1d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t F (Q) - (1 - F (P))) Z (i) = (F (P) - t F (Q)) Z (i)$
65		subdi	$⊢ (t \in ℂ \land 1 \in ℂ \land F (Q) \in ℂ) \to t (1 - F (Q)) = t \cdot 1 - t F (Q)$
66	49 65	mp3an2	$⊢ (t \in ℂ \land F (Q) \in ℂ) \to t (1 - F (Q)) = t \cdot 1 - t F (Q)$
67		mulid1	$⊢ t \in ℂ \to t \cdot 1 = t$
68	67	adantr	$⊢ (t \in ℂ \land F (Q) \in ℂ) \to t \cdot 1 = t$
69	68	oveq1d	$⊢ (t \in ℂ \land F (Q) \in ℂ) \to t \cdot 1 - t F (Q) = t - t F (Q)$
70	66 69	eqtrd	$⊢ (t \in ℂ \land F (Q) \in ℂ) \to t (1 - F (Q)) = t - t F (Q)$
71	50 51 70	syl2anc	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t (1 - F (Q)) = t - t F (Q)$
72	71	oveq2d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to 1 - t + t (1 - F (Q)) = (1 - t) + t - t F (Q)$
73		npncan	$⊢ (1 \in ℂ \land t \in ℂ \land t F (Q) \in ℂ) \to (1 - t) + t - t F (Q) = 1 - t F (Q)$
74	49 50 52 73	mp3an2i	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t) + t - t F (Q) = 1 - t F (Q)$
75	72 74	eqtr2d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to 1 - t F (Q) = 1 - t + t (1 - F (Q))$
76	75	oveq1d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t F (Q)) Z (i) = (1 - t + t (1 - F (Q))) Z (i)$
77		subcl	$⊢ (1 \in ℂ \land t \in ℂ) \to 1 - t \in ℂ$
78	49 77	mpan	$⊢ t \in ℂ \to 1 - t \in ℂ$
79	78	3ad2ant1	$⊢ (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ) \to 1 - t \in ℂ$
80	79	adantl	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to 1 - t \in ℂ$
81		subcl	$⊢ (1 \in ℂ \land F (Q) \in ℂ) \to 1 - F (Q) \in ℂ$
82	49 81	mpan	$⊢ F (Q) \in ℂ \to 1 - F (Q) \in ℂ$
83	82	3ad2ant3	$⊢ (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ) \to 1 - F (Q) \in ℂ$
84	83	adantl	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to 1 - F (Q) \in ℂ$
85	50 84	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t (1 - F (Q)) \in ℂ$
86	80 85 59	adddird	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t + t (1 - F (Q))) Z (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i)$
87	50 84 59	mulassd	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t (1 - F (Q)) Z (i) = t (1 - F (Q)) Z (i)$
88	87	oveq2d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t) Z (i) + t (1 - F (Q)) Z (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i)$
89	76 86 88	3eqtrd	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t F (Q)) Z (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i)$
90	89	oveq1d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t F (Q)) Z (i) - (1 - F (P)) Z (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i) - (1 - F (P)) Z (i)$
91	60 64 90	3eqtr3d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (F (P) - t F (Q)) Z (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i) - (1 - F (P)) Z (i)$
92		simplr	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to U (i) \in ℂ$
93	61 52 92	subdird	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (F (P) - t F (Q)) U (i) = F (P) U (i) - t F (Q) U (i)$
94	50 51 92	mulassd	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t F (Q) U (i) = t F (Q) U (i)$
95	94	oveq2d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to F (P) U (i) - t F (Q) U (i) = F (P) U (i) - t F (Q) U (i)$
96	93 95	eqtrd	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (F (P) - t F (Q)) U (i) = F (P) U (i) - t F (Q) U (i)$
97	91 96	eqeq12d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to ((F (P) - t F (Q)) Z (i) = (F (P) - t F (Q)) U (i) \leftrightarrow (1 - t) Z (i) + t (1 - F (Q)) Z (i) - (1 - F (P)) Z (i) = F (P) U (i) - t F (Q) U (i))$
98	58 59	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - F (P)) Z (i) \in ℂ$
99	61 92	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to F (P) U (i) \in ℂ$
100	80 59	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t) Z (i) \in ℂ$
101	84 59	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - F (Q)) Z (i) \in ℂ$
102	50 101	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t (1 - F (Q)) Z (i) \in ℂ$
103	100 102	addcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t) Z (i) + t (1 - F (Q)) Z (i) \in ℂ$
104	51 92	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to F (Q) U (i) \in ℂ$
105	50 104	mulcld	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t F (Q) U (i) \in ℂ$
106	98 99 103 105	addsubeq4d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to ((1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i) + t F (Q) U (i) \leftrightarrow (1 - t) Z (i) + t (1 - F (Q)) Z (i) - (1 - F (P)) Z (i) = F (P) U (i) - t F (Q) U (i))$
107	100 102 105	addassd	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t) Z (i) + t (1 - F (Q)) Z (i) + t F (Q) U (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i) + t F (Q) U (i)$
108	50 101 104	adddid	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to t ((1 - F (Q)) Z (i) + F (Q) U (i)) = t (1 - F (Q)) Z (i) + t F (Q) U (i)$
109	108	oveq2d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) = (1 - t) Z (i) + t (1 - F (Q)) Z (i) + t F (Q) U (i)$
110	107 109	eqtr4d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to (1 - t) Z (i) + t (1 - F (Q)) Z (i) + t F (Q) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i))$
111	110	eqeq2d	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to ((1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t (1 - F (Q)) Z (i) + t F (Q) U (i) \leftrightarrow (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)))$
112	97 106 111	3bitr2rd	$⊢ ((Z (i) \in ℂ \land U (i) \in ℂ) \land (t \in ℂ \land F (P) \in ℂ \land F (Q) \in ℂ)) \to ((1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) \leftrightarrow (F (P) - t F (Q)) Z (i) = (F (P) - t F (Q)) U (i))$
113	28 31 36 42 48 112	syl23anc	$⊢ ((((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 t \in [0, 1])) \land i \in (1 \dots N)) \to ((1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) \leftrightarrow (F (P) - t F (Q)) Z (i) = (F (P) - t F (Q)) U (i))$
114	113	ralbidva	$⊢ (((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 t \in [0, 1])) \to (\forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) \leftrightarrow \forall i \in (1 \dots N) (F (P) - t F (Q)) Z (i) = (F (P) - t F (Q)) U (i))$
115	36 48	mulcld	$⊢ ((((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 t \in [0, 1])) \land i \in (1 \dots N)) \to t F (Q) \in ℂ$
116	42 115	subcld	$⊢ ((((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 t \in [0, 1])) \land i \in (1 \dots N)) \to F (P) - t F (Q) \in ℂ$
117		mulcan1g	$⊢ (F (P) - t F (Q) \in ℂ \land Z (i) \in ℂ \land U (i) \in ℂ) \to ((F (P) - t F (Q)) Z (i) = (F (P) - t F (Q)) U (i) \leftrightarrow (F (P) - t F (Q) = 0 \lor Z (i) = U (i)))$
118	116 28 31 117	syl3anc	$⊢ ((((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 t \in [0, 1])) \land i \in (1 \dots N)) \to ((F (P) - t F (Q)) Z (i) = (F (P) - t F (Q)) U (i) \leftrightarrow (F (P) - t F (Q) = 0 \lor Z (i) = U (i)))$
119	118	ralbidva	$⊢ (((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 t \in [0, 1])) \to (\forall i \in (1 \dots N) (F (P) - t F (Q)) Z (i) = (F (P) - t F (Q)) U (i) \leftrightarrow \forall i \in (1 \dots N) (F (P) - t F (Q) = 0 \lor Z (i) = U (i)))$
120		r19.32v	$⊢ \forall i \in (1 \dots N) (F (P) - t F (Q) = 0 \lor Z (i) = U (i)) \leftrightarrow (F (P) - t F (Q) = 0 \lor \forall i \in (1 \dots N) Z (i) = U (i))$
121		simplr	$⊢ (((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 t \in [0, 1])) \to Z \neq U$
122	121	neneqd	$⊢ (((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 t \in [0, 1])) \to \neg Z = U$
123		biorf	$⊢ \neg Z = U \to (F (P) - t F (Q) = 0 \leftrightarrow (Z = U \lor F (P) - t F (Q) = 0))$
124		orcom	$⊢ (Z = U \lor F (P) - t F (Q) = 0) \leftrightarrow (F (P) - t F (Q) = 0 \lor Z = U)$
125	123 124	bitrdi	$⊢ \neg Z = U \to (F (P) - t F (Q) = 0 \leftrightarrow (F (P) - t F (Q) = 0 \lor Z = U))$
126	122 125	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 t \in [0, 1])) \to (F (P) - t F (Q) = 0 \leftrightarrow (F (P) - t F (Q) = 0 \lor Z = U))$
127	35 47	mulcld	$⊢ (((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 t \in [0, 1])) \to t F (Q) \in ℂ$
128	41 127	subeq0ad	$⊢ (((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 t \in [0, 1])) \to (F (P) - t F (Q) = 0 \leftrightarrow F (P) = t F (Q))$
129		eqeefv	$⊢ (Z \in 𝔼 (N) \land U \in 𝔼 (N)) \to (Z = U \leftrightarrow \forall i \in (1 \dots N) Z (i) = U (i))$
130	129	3adant1	$⊢ (N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \to (Z = U \leftrightarrow \forall i \in (1 \dots N) Z (i) = U (i))$
131	130	adantr	$⊢ ((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \to (Z = U \leftrightarrow \forall i \in (1 \dots N) Z (i) = U (i))$
132	131	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 t \in [0, 1])) \to (Z = U \leftrightarrow \forall i \in (1 \dots N) Z (i) = U (i))$
133	132	orbi2d	$⊢ (((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 t \in [0, 1])) \to ((F (P) - t F (Q) = 0 \lor Z = U) \leftrightarrow (F (P) - t F (Q) = 0 \lor \forall i \in (1 \dots N) Z (i) = U (i)))$
134	126 128 133	3bitr3rd	$⊢ (((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 t \in [0, 1])) \to ((F (P) - t F (Q) = 0 \lor \forall i \in (1 \dots N) Z (i) = U (i)) \leftrightarrow F (P) = t F (Q))$
135	120 134	syl5bb	$⊢ (((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 t \in [0, 1])) \to (\forall i \in (1 \dots N) (F (P) - t F (Q) = 0 \lor Z (i) = U (i)) \leftrightarrow F (P) = t F (Q))$
136	114 119 135	3bitrd	$⊢ (((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 t \in [0, 1])) \to (\forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) \leftrightarrow F (P) = t F (Q))$
137	136	anassrs	$⊢ ((((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 t \in [0, 1]) \to (\forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) \leftrightarrow F (P) = t F (Q))$
138	137	rexbidva	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞))) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) \leftrightarrow \exists t \in [0, 1] F (P) = t F (Q))$
139	33	adantl	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to t \in ℝ$
140		1red	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to 1 \in ℝ$
141	43	biimpi	$⊢ F (Q) \in [0, +∞) \to (F (Q) \in ℝ \land 0 \leq F (Q))$
142	141	ad2antlr	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to (F (Q) \in ℝ \land 0 \leq F (Q))$
143	32	simp3bi	$⊢ t \in [0, 1] \to t \leq 1$
144	143	adantl	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to t \leq 1$
145		lemul1a	$⊢ ((t \in ℝ \land 1 \in ℝ \land (F (Q) \in ℝ \land 0 \leq F (Q))) \land t \leq 1) \to t F (Q) \leq 1 F (Q)$
146	139 140 142 144 145	syl31anc	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to t F (Q) \leq 1 F (Q)$
147	45	ad2antlr	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to F (Q) \in ℂ$
148	147	mulid2d	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to 1 F (Q) = F (Q)$
149	146 148	breqtrd	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to t F (Q) \leq F (Q)$
150		breq1	$⊢ F (P) = t F (Q) \to (F (P) \leq F (Q) \leftrightarrow t F (Q) \leq F (Q))$
151	149 150	syl5ibrcom	$⊢ ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land t \in [0, 1]) \to (F (P) = t F (Q) \to F (P) \leq F (Q))$
152	151	rexlimdva	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to (\exists t \in [0, 1] F (P) = t F (Q) \to F (P) \leq F (Q))$
153		0elunit	$⊢ 0 \in [0, 1]$
154		simpl	$⊢ (F (P) = 0 \land F (Q) \in [0, +∞)) \to F (P) = 0$
155	45	mul02d	$⊢ F (Q) \in [0, +∞) \to 0 \cdot F (Q) = 0$
156	155	adantl	$⊢ (F (P) = 0 \land F (Q) \in [0, +∞)) \to 0 \cdot F (Q) = 0$
157	154 156	eqtr4d	$⊢ (F (P) = 0 \land F (Q) \in [0, +∞)) \to F (P) = 0 \cdot F (Q)$
158		oveq1	$⊢ t = 0 \to t F (Q) = 0 \cdot F (Q)$
159	158	rspceeqv	$⊢ (0 \in [0, 1] \land F (P) = 0 \cdot F (Q)) \to \exists t \in [0, 1] F (P) = t F (Q)$
160	153 157 159	sylancr	$⊢ (F (P) = 0 \land F (Q) \in [0, +∞)) \to \exists t \in [0, 1] F (P) = t F (Q)$
161	160	adantrl	$⊢ (F (P) = 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞))) \to \exists t \in [0, 1] F (P) = t F (Q)$
162	161	a1d	$⊢ (F (P) = 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞))) \to (F (P) \leq F (Q) \to \exists t \in [0, 1] F (P) = t F (Q))$
163	162	ex	$⊢ F (P) = 0 \to ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to (F (P) \leq F (Q) \to \exists t \in [0, 1] F (P) = t F (Q)))$
164		simp3	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (P) \leq F (Q)$
165	38	adantr	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to F (P) \in ℝ$
166	165	3ad2ant2	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (P) \in ℝ$
167	37	simprbi	$⊢ F (P) \in [0, +∞) \to 0 \leq F (P)$
168	167	adantr	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to 0 \leq F (P)$
169	168	3ad2ant2	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to 0 \leq F (P)$
170	44	adantl	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to F (Q) \in ℝ$
171	170	3ad2ant2	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (Q) \in ℝ$
172		0red	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to 0 \in ℝ$
173		simp1	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (P) \neq 0$
174	166 169 173	ne0gt0d	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to 0 < F (P)$
175	172 166 171 174 164	ltletrd	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to 0 < F (Q)$
176		divelunit	$⊢ ((F (P) \in ℝ \land 0 \leq F (P)) \land (F (Q) \in ℝ \land 0 < F (Q))) \to (\frac{F (P)}{F (Q)} \in [0, 1] \leftrightarrow F (P) \leq F (Q))$
177	166 169 171 175 176	syl22anc	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to (\frac{F (P)}{F (Q)} \in [0, 1] \leftrightarrow F (P) \leq F (Q))$
178	164 177	mpbird	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to \frac{F (P)}{F (Q)} \in [0, 1]$
179	40	3ad2ant2	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (P) \in ℂ$
180	46	3ad2ant2	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (Q) \in ℂ$
181	175	gt0ne0d	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (Q) \neq 0$
182	179 180 181	divcan1d	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to (\frac{F (P)}{F (Q)}) F (Q) = F (P)$
183	182	eqcomd	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to F (P) = (\frac{F (P)}{F (Q)}) F (Q)$
184		oveq1	$⊢ t = \frac{F (P)}{F (Q)} \to t F (Q) = (\frac{F (P)}{F (Q)}) F (Q)$
185	184	rspceeqv	$⊢ (\frac{F (P)}{F (Q)} \in [0, 1] \land F (P) = (\frac{F (P)}{F (Q)}) F (Q)) \to \exists t \in [0, 1] F (P) = t F (Q)$
186	178 183 185	syl2anc	$⊢ (F (P) \neq 0 \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \land F (P) \leq F (Q)) \to \exists t \in [0, 1] F (P) = t F (Q)$
187	186	3exp	$⊢ F (P) \neq 0 \to ((F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to (F (P) \leq F (Q) \to \exists t \in [0, 1] F (P) = t F (Q)))$
188	163 187	pm2.61ine	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to (F (P) \leq F (Q) \to \exists t \in [0, 1] F (P) = t F (Q))$
189	152 188	impbid	$⊢ (F (P) \in [0, +∞) \land F (Q) \in [0, +∞)) \to (\exists t \in [0, 1] F (P) = t F (Q) \leftrightarrow F (P) \leq F (Q))$
190	189	adantl	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞))) \to (\exists t \in [0, 1] F (P) = t F (Q) \leftrightarrow F (P) \leq F (Q))$
191	138 190	bitrd	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (F (P) \in [0, +∞) \land F (Q) \in [0, +∞))) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) (1 - F (P)) Z (i) + F (P) U (i) = (1 - t) Z (i) + t ((1 - F (Q)) Z (i) + F (Q) U (i)) \leftrightarrow F (P) \leq F (Q))$
192	25 191	sylan9bbr	$⊢ ((((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 \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))) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow F (P) \leq F (Q))$
193	192	anasss	$⊢ (((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 \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)))) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow F (P) \leq F (Q))$
194	17 193	sylan2b	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land ((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)))) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow F (P) \leq F (Q))$
195	13 194	syldan	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D)) \to (\exists t \in [0, 1] \forall i \in (1 \dots N) P (i) = (1 - t) Z (i) + t Q (i) \leftrightarrow F (P) \leq F (Q))$
196	10 195	bitrd	$⊢ (((N \in ℕ \land Z \in 𝔼 (N) \land U \in 𝔼 (N)) \land Z \neq U) \land (P \in D \land Q \in D)) \to (P Btwn ⟨Z, Q⟩ \leftrightarrow F (P) \leq F (Q))$

Metamath Proof Explorer

Theorem axcontlem7

Proof