ballotlemic

Description: If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016)

	Ref	Expression
Hypotheses	ballotth.m	$⊢ M \in ℕ$
	ballotth.n	$⊢ N \in ℕ$
	ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
	ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
	ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
	ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
	ballotth.mgtn	$⊢ N < M$
	ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ sup (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
Assertion	ballotlemic	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to I (C) \in C$

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	$⊢ M \in ℕ$
2		ballotth.n	$⊢ N \in ℕ$
3		ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
4		ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
5		ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
6		ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
7		ballotth.mgtn	$⊢ N < M$
8		ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ sup (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
9		eldifi	$⊢ C \in (O ∖ E) \to C \in O$
10	9	ad2antrr	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to C \in O$
11	1 2 3 4 5 6 7 8	ballotlemiex	$⊢ C \in (O ∖ E) \to (I (C) \in (1 \dots M + N) \land F (C) (I (C)) = 0)$
12	11	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
13		elfznn	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in ℕ$
14	12 13	syl	$⊢ C \in (O ∖ E) \to I (C) \in ℕ$
15	14	adantr	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to I (C) \in ℕ$
16	1 2 3 4 5 6 7 8	ballotlemi1	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to I (C) \neq 1$
17		eluz2b3	$⊢ I (C) \in ℤ_{\geq 2} \leftrightarrow (I (C) \in ℕ \land I (C) \neq 1)$
18	15 16 17	sylanbrc	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to I (C) \in ℤ_{\geq 2}$
19		uz2m1nn	$⊢ I (C) \in ℤ_{\geq 2} \to I (C) - 1 \in ℕ$
20	18 19	syl	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to I (C) - 1 \in ℕ$
21	20	adantr	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to I (C) - 1 \in ℕ$
22		elnnuz	$⊢ I (C) - 1 \in ℕ \leftrightarrow I (C) - 1 \in ℤ_{\geq 1}$
23	22	biimpi	$⊢ I (C) - 1 \in ℕ \to I (C) - 1 \in ℤ_{\geq 1}$
24		eluzfz1	$⊢ I (C) - 1 \in ℤ_{\geq 1} \to 1 \in (1 \dots I (C) - 1)$
25	20 23 24	3syl	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to 1 \in (1 \dots I (C) - 1)$
26	25	adantr	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to 1 \in (1 \dots I (C) - 1)$
27		1nn	$⊢ 1 \in ℕ$
28	27	a1i	$⊢ C \in (O ∖ E) \to 1 \in ℕ$
29	1 2 3 4 5 9 28	ballotlemfp1	$⊢ C \in (O ∖ E) \to ((\neg 1 \in C \to F (C) (1) = F (C) (1 - 1) - 1) \land (1 \in C \to F (C) (1) = F (C) (1 - 1) + 1))$
30	29	simpld	$⊢ C \in (O ∖ E) \to (\neg 1 \in C \to F (C) (1) = F (C) (1 - 1) - 1)$
31	30	imp	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to F (C) (1) = F (C) (1 - 1) - 1$
32		1m1e0	$⊢ 1 - 1 = 0$
33	32	fveq2i	$⊢ F (C) (1 - 1) = F (C) (0)$
34	33	oveq1i	$⊢ F (C) (1 - 1) - 1 = F (C) (0) - 1$
35	34	a1i	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to F (C) (1 - 1) - 1 = F (C) (0) - 1$
36	1 2 3 4 5	ballotlemfval0	$⊢ C \in O \to F (C) (0) = 0$
37	9 36	syl	$⊢ C \in (O ∖ E) \to F (C) (0) = 0$
38	37	adantr	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to F (C) (0) = 0$
39	38	oveq1d	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to F (C) (0) - 1 = 0 - 1$
40	31 35 39	3eqtrrd	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to 0 - 1 = F (C) (1)$
41		0le1	$⊢ 0 \leq 1$
42		0re	$⊢ 0 \in ℝ$
43		1re	$⊢ 1 \in ℝ$
44		suble0	$⊢ (0 \in ℝ \land 1 \in ℝ) \to (0 - 1 \leq 0 \leftrightarrow 0 \leq 1)$
45	42 43 44	mp2an	$⊢ 0 - 1 \leq 0 \leftrightarrow 0 \leq 1$
46	41 45	mpbir	$⊢ 0 - 1 \leq 0$
47	40 46	eqbrtrrdi	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to F (C) (1) \leq 0$
48	47	adantr	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to F (C) (1) \leq 0$
49		fveq2	$⊢ i = 1 \to F (C) (i) = F (C) (1)$
50	49	breq1d	$⊢ i = 1 \to (F (C) (i) \leq 0 \leftrightarrow F (C) (1) \leq 0)$
51	50	rspcev	$⊢ (1 \in (1 \dots I (C) - 1) \land F (C) (1) \leq 0) \to \exists i \in (1 \dots I (C) - 1) F (C) (i) \leq 0$
52	26 48 51	syl2anc	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to \exists i \in (1 \dots I (C) - 1) F (C) (i) \leq 0$
53		0lt1	$⊢ 0 < 1$
54		1p0e1	$⊢ 1 + 0 = 1$
55	1 2 3 4 5 9 14	ballotlemfp1	$⊢ C \in (O ∖ E) \to ((\neg I (C) \in C \to F (C) (I (C)) = F (C) (I (C) - 1) - 1) \land (I (C) \in C \to F (C) (I (C)) = F (C) (I (C) - 1) + 1))$
56	55	simpld	$⊢ C \in (O ∖ E) \to (\neg I (C) \in C \to F (C) (I (C)) = F (C) (I (C) - 1) - 1)$
57	56	imp	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to F (C) (I (C)) = F (C) (I (C) - 1) - 1$
58	11	simprd	$⊢ C \in (O ∖ E) \to F (C) (I (C)) = 0$
59	58	adantr	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to F (C) (I (C)) = 0$
60	57 59	eqtr3d	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to F (C) (I (C) - 1) - 1 = 0$
61	9	adantr	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to C \in O$
62	14	nnzd	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
63	62	adantr	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to I (C) \in ℤ$
64		1zzd	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to 1 \in ℤ$
65	63 64	zsubcld	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to I (C) - 1 \in ℤ$
66	1 2 3 4 5 61 65	ballotlemfelz	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to F (C) (I (C) - 1) \in ℤ$
67	66	zcnd	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to F (C) (I (C) - 1) \in ℂ$
68		1cnd	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to 1 \in ℂ$
69		0cnd	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to 0 \in ℂ$
70	67 68 69	subaddd	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to (F (C) (I (C) - 1) - 1 = 0 \leftrightarrow 1 + 0 = F (C) (I (C) - 1))$
71	60 70	mpbid	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to 1 + 0 = F (C) (I (C) - 1)$
72	54 71	syl5eqr	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to 1 = F (C) (I (C) - 1)$
73	53 72	breqtrid	$⊢ (C \in (O ∖ E) \land \neg I (C) \in C) \to 0 < F (C) (I (C) - 1)$
74	73	adantlr	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to 0 < F (C) (I (C) - 1)$
75	1 2 3 4 5 10 21 52 74	ballotlemfc0	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to \exists k \in (1 \dots I (C) - 1) F (C) (k) = 0$
76	1 2 3 4 5 6 7 8	ballotlemimin	$⊢ C \in (O ∖ E) \to \neg \exists k \in (1 \dots I (C) - 1) F (C) (k) = 0$
77	76	ad2antrr	$⊢ ((C \in (O ∖ E) \land \neg 1 \in C) \land \neg I (C) \in C) \to \neg \exists k \in (1 \dots I (C) - 1) F (C) (k) = 0$
78	75 77	condan	$⊢ (C \in (O ∖ E) \land \neg 1 \in C) \to I (C) \in C$

Metamath Proof Explorer

Theorem ballotlemic

Proof