ballotlemfrcn0

Description: Value of F for a reversed counting ( RC ) , before the first tie, cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2017) (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\} ℝ <))$
	ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
	ballotth.r	$⊢ R = (c \in (O ∖ E) ⟼ S (c) [c])$
Assertion	ballotlemfrcn0	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to F (R (C)) (J) \neq 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		ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
10		ballotth.r	$⊢ R = (c \in (O ∖ E) ⟼ S (c) [c])$
11		1zzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \in ℤ$
12		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
13	1 2 12	mp2an	$⊢ M + N \in ℕ$
14	13	nnzi	$⊢ M + N \in ℤ$
15	14	a1i	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to M + N \in ℤ$
16	1 2 3 4 5 6 7 8 9	ballotlemsdom	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) \in (1 \dots M + N)$
17	16	elfzelzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) \in ℤ$
18	17	3adant3	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) \in ℤ$
19	18 11	zsubcld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \in ℤ$
20	1 2 3 4 5 6 7 8 9	ballotlemsgt1	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 < S (C) (J)$
21		zltlem1	$⊢ (1 \in ℤ \land S (C) (J) \in ℤ) \to (1 < S (C) (J) \leftrightarrow 1 \leq S (C) (J) - 1)$
22	21	biimpa	$⊢ ((1 \in ℤ \land S (C) (J) \in ℤ) \land 1 < S (C) (J)) \to 1 \leq S (C) (J) - 1$
23	11 18 20 22	syl21anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \leq S (C) (J) - 1$
24	18	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) \in ℝ$
25		1red	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \in ℝ$
26	24 25	resubcld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \in ℝ$
27		simp1	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to C \in (O ∖ E)$
28	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)$
29	28	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
30		elfzelz	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in ℤ$
31	27 29 30	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \in ℤ$
32	31	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \in ℝ$
33	15	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to M + N \in ℝ$
34		elfzelz	$⊢ J \in (1 \dots M + N) \to J \in ℤ$
35	34	3ad2ant2	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in ℤ$
36		elfzle1	$⊢ J \in (1 \dots M + N) \to 1 \leq J$
37	36	3ad2ant2	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \leq J$
38	35	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in ℝ$
39		simp3	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J < I (C)$
40	38 32 39	ltled	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \leq I (C)$
41	11 31 35 37 40	elfzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in (1 \dots I (C))$
42	1 2 3 4 5 6 7 8 9	ballotlemsel1i	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in (1 \dots I (C))$
43	27 41 42	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) \in (1 \dots I (C))$
44		elfzle2	$⊢ S (C) (J) \in (1 \dots I (C)) \to S (C) (J) \leq I (C)$
45	43 44	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) \leq I (C)$
46		zlem1lt	$⊢ (S (C) (J) \in ℤ \land I (C) \in ℤ) \to (S (C) (J) \leq I (C) \leftrightarrow S (C) (J) - 1 < I (C))$
47	18 31 46	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to (S (C) (J) \leq I (C) \leftrightarrow S (C) (J) - 1 < I (C))$
48	45 47	mpbid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 < I (C)$
49	26 32 48	ltled	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \leq I (C)$
50		elfzle2	$⊢ I (C) \in (1 \dots M + N) \to I (C) \leq M + N$
51	27 29 50	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \leq M + N$
52	26 32 33 49 51	letrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \leq M + N$
53	11 15 19 23 52	elfzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \in (1 \dots M + N)$
54		biid	$⊢ S (C) (J) - 1 < I (C) \leftrightarrow S (C) (J) - 1 < I (C)$
55	48 54	sylibr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 < I (C)$
56	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\} ℝ <)$
57	56	breq2d	$⊢ C \in (O ∖ E) \to (S (C) (J) - 1 < I (C) \leftrightarrow S (C) (J) - 1 < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
58	57	3ad2ant1	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to (S (C) (J) - 1 < I (C) \leftrightarrow S (C) (J) - 1 < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
59	55 58	mpbid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <)$
60		ltso	$⊢ < Or ℝ$
61	60	a1i	$⊢ C \in (O ∖ E) \to < Or ℝ$
62	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))$
63	61 62	inflb	$⊢ C \in (O ∖ E) \to (S (C) (J) - 1 \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \to \neg S (C) (J) - 1 < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
64	63	con2d	$⊢ C \in (O ∖ E) \to (S (C) (J) - 1 < inf (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <) \to \neg S (C) (J) - 1 \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\})$
65	27 59 64	sylc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to \neg S (C) (J) - 1 \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\}$
66		fveqeq2	$⊢ k = S (C) (J) - 1 \to (F (C) (k) = 0 \leftrightarrow F (C) (S (C) (J) - 1) = 0)$
67	66	elrab	$⊢ S (C) (J) - 1 \in \{k \in (1 \dots M + N) \| F (C) (k) = 0\} \leftrightarrow (S (C) (J) - 1 \in (1 \dots M + N) \land F (C) (S (C) (J) - 1) = 0)$
68	65 67	sylnib	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to \neg (S (C) (J) - 1 \in (1 \dots M + N) \land F (C) (S (C) (J) - 1) = 0)$
69		imnan	$⊢ (S (C) (J) - 1 \in (1 \dots M + N) \to \neg F (C) (S (C) (J) - 1) = 0) \leftrightarrow \neg (S (C) (J) - 1 \in (1 \dots M + N) \land F (C) (S (C) (J) - 1) = 0)$
70	68 69	sylibr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to (S (C) (J) - 1 \in (1 \dots M + N) \to \neg F (C) (S (C) (J) - 1) = 0)$
71	53 70	mpd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to \neg F (C) (S (C) (J) - 1) = 0$
72	71	neqned	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to F (C) (S (C) (J) - 1) \neq 0$
73	1 2 3 4 5 6 7 8 9 10	ballotlemro	$⊢ C \in (O ∖ E) \to R (C) \in O$
74	73	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to R (C) \in O$
75		elfzelz	$⊢ J \in (1 \dots I (C)) \to J \in ℤ$
76	75	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℤ$
77	1 2 3 4 5 74 76	ballotlemfelz	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) \in ℤ$
78	77	zcnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) \in ℂ$
79	78	negeq0d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (F (R (C)) (J) = 0 \leftrightarrow - F (R (C)) (J) = 0)$
80		eqid	$⊢ (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|) = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
81	1 2 3 4 5 6 7 8 9 10 80	ballotlemfrceq	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) = - F (R (C)) (J)$
82	81	eqeq1d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (F (C) (S (C) (J) - 1) = 0 \leftrightarrow - F (R (C)) (J) = 0)$
83	79 82	bitr4d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (F (R (C)) (J) = 0 \leftrightarrow F (C) (S (C) (J) - 1) = 0)$
84	83	necon3bid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (F (R (C)) (J) \neq 0 \leftrightarrow F (C) (S (C) (J) - 1) \neq 0)$
85	27 41 84	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to (F (R (C)) (J) \neq 0 \leftrightarrow F (C) (S (C) (J) - 1) \neq 0)$
86	72 85	mpbird	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to F (R (C)) (J) \neq 0$

Metamath Proof Explorer

Theorem ballotlemfrcn0

Proof