ballotlemimin

Description: ( IC ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016) (Revised by AV, 6-Oct-2020)

	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) ⟼ inf (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
Assertion	ballotlemimin	$⊢ C \in (O ∖ E) \to \neg \exists k \in (1 \dots I (C) - 1) F (C) (k) = 0$

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) ⟼ inf (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
9		elfzle2	$⊢ k \in (1 \dots I (C) - 1) \to k \leq I (C) - 1$
10	9	adantl	$⊢ (C \in (O ∖ E) \land k \in (1 \dots I (C) - 1)) \to k \leq I (C) - 1$
11		elfzelz	$⊢ k \in (1 \dots I (C) - 1) \to k \in ℤ$
12	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)$
13	12	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
14	13	elfzelzd	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
15		zltlem1	$⊢ (k \in ℤ \land I (C) \in ℤ) \to (k < I (C) \leftrightarrow k \leq I (C) - 1)$
16	11 14 15	syl2anr	$⊢ (C \in (O ∖ E) \land k \in (1 \dots I (C) - 1)) \to (k < I (C) \leftrightarrow k \leq I (C) - 1)$
17	10 16	mpbird	$⊢ (C \in (O ∖ E) \land k \in (1 \dots I (C) - 1)) \to k < I (C)$
18	17	adantr	$⊢ ((C \in (O ∖ E) \land k \in (1 \dots I (C) - 1)) \land F (C) (k) = 0) \to k < I (C)$
19		1zzd	$⊢ C \in (O ∖ E) \to 1 \in ℤ$
20	14 19	zsubcld	$⊢ C \in (O ∖ E) \to I (C) - 1 \in ℤ$
21	20	zred	$⊢ C \in (O ∖ E) \to I (C) - 1 \in ℝ$
22		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
23	1 2 22	mp2an	$⊢ M + N \in ℕ$
24	23	a1i	$⊢ C \in (O ∖ E) \to M + N \in ℕ$
25	24	nnred	$⊢ C \in (O ∖ E) \to M + N \in ℝ$
26		elfzle2	$⊢ I (C) \in (1 \dots M + N) \to I (C) \leq M + N$
27	13 26	syl	$⊢ C \in (O ∖ E) \to I (C) \leq M + N$
28	24	nnzd	$⊢ C \in (O ∖ E) \to M + N \in ℤ$
29		zlem1lt	$⊢ (I (C) \in ℤ \land M + N \in ℤ) \to (I (C) \leq M + N \leftrightarrow I (C) - 1 < M + N)$
30	14 28 29	syl2anc	$⊢ C \in (O ∖ E) \to (I (C) \leq M + N \leftrightarrow I (C) - 1 < M + N)$
31	27 30	mpbid	$⊢ C \in (O ∖ E) \to I (C) - 1 < M + N$
32	21 25 31	ltled	$⊢ C \in (O ∖ E) \to I (C) - 1 \leq M + N$
33		eluz	$⊢ (I (C) - 1 \in ℤ \land M + N \in ℤ) \to (M + N \in ℤ_{\geq (I (C) - 1)} \leftrightarrow I (C) - 1 \leq M + N)$
34	20 28 33	syl2anc	$⊢ C \in (O ∖ E) \to (M + N \in ℤ_{\geq (I (C) - 1)} \leftrightarrow I (C) - 1 \leq M + N)$
35	32 34	mpbird	$⊢ C \in (O ∖ E) \to M + N \in ℤ_{\geq (I (C) - 1)}$
36		fzss2	$⊢ M + N \in ℤ_{\geq (I (C) - 1)} \to (1 \dots I (C) - 1) \subseteq (1 \dots M + N)$
37	35 36	syl	$⊢ C \in (O ∖ E) \to (1 \dots I (C) - 1) \subseteq (1 \dots M + N)$
38	37	sseld	$⊢ C \in (O ∖ E) \to (k \in (1 \dots I (C) - 1) \to k \in (1 \dots M + N))$
39		rabid	$⊢ k \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \leftrightarrow (k \in (1 \dots M + N) \land F (C) (k) = 0)$
40	1 2 3 4 5 6 7 8	ballotlemsup	$⊢ C \in (O ∖ E) \to \exists z \in ℝ (\forall w \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \neg w < z \land \forall w \in ℝ (z < w \to \exists y \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} y < w))$
41		ltso	$⊢ < Or ℝ$
42	41	a1i	$⊢ \exists z \in ℝ (\forall w \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \neg w < z \land \forall w \in ℝ (z < w \to \exists y \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} y < w)) \to < Or ℝ$
43		id	$⊢ \exists z \in ℝ (\forall w \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \neg w < z \land \forall w \in ℝ (z < w \to \exists y \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} y < w)) \to \exists z \in ℝ (\forall w \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \neg w < z \land \forall w \in ℝ (z < w \to \exists y \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} y < w))$
44	42 43	inflb	$⊢ \exists z \in ℝ (\forall w \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \neg w < z \land \forall w \in ℝ (z < w \to \exists y \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} y < w)) \to (k \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \to \neg k < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
45	40 44	syl	$⊢ C \in (O ∖ E) \to (k \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \to \neg k < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
46	1 2 3 4 5 6 7 8	ballotlemi	$⊢ C \in (O ∖ E) \to I (C) = inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <)$
47	46	breq2d	$⊢ C \in (O ∖ E) \to (k < I (C) \leftrightarrow k < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
48	47	notbid	$⊢ C \in (O ∖ E) \to (\neg k < I (C) \leftrightarrow \neg k < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
49	45 48	sylibrd	$⊢ C \in (O ∖ E) \to (k \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \to \neg k < I (C))$
50	39 49	biimtrrid	$⊢ C \in (O ∖ E) \to ((k \in (1 \dots M + N) \land F (C) (k) = 0) \to \neg k < I (C))$
51	38 50	syland	$⊢ C \in (O ∖ E) \to ((k \in (1 \dots I (C) - 1) \land F (C) (k) = 0) \to \neg k < I (C))$
52	51	imp	$⊢ (C \in (O ∖ E) \land (k \in (1 \dots I (C) - 1) \land F (C) (k) = 0)) \to \neg k < I (C)$
53		biid	$⊢ k < I (C) \leftrightarrow k < I (C)$
54	52 53	sylnib	$⊢ (C \in (O ∖ E) \land (k \in (1 \dots I (C) - 1) \land F (C) (k) = 0)) \to \neg k < I (C)$
55	54	anassrs	$⊢ ((C \in (O ∖ E) \land k \in (1 \dots I (C) - 1)) \land F (C) (k) = 0) \to \neg k < I (C)$
56	18 55	pm2.65da	$⊢ (C \in (O ∖ E) \land k \in (1 \dots I (C) - 1)) \to \neg F (C) (k) = 0$
57	56	nrexdv	$⊢ C \in (O ∖ E) \to \neg \exists k \in (1 \dots I (C) - 1) F (C) (k) = 0$

Metamath Proof Explorer

Theorem ballotlemimin

Proof