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) ⟼ sup (\{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) ⟼ sup (\{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		elfzelz	$⊢ S (C) (J) \in (1 \dots M + N) \to S (C) (J) \in ℤ$
18	16 17	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) \in ℤ$
19	18	3adant3	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) \in ℤ$
20	19 11	zsubcld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \in ℤ$
21	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)$
22		zltlem1	$⊢ (1 \in ℤ \land S (C) (J) \in ℤ) \to (1 < S (C) (J) \leftrightarrow 1 \leq S (C) (J) - 1)$
23	22	biimpa	$⊢ ((1 \in ℤ \land S (C) (J) \in ℤ) \land 1 < S (C) (J)) \to 1 \leq S (C) (J) - 1$
24	11 19 21 23	syl21anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \leq S (C) (J) - 1$
25	19	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) \in ℝ$
26		1red	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \in ℝ$
27	25 26	resubcld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \in ℝ$
28		simp1	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to C \in (O ∖ E)$
29	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)$
30	29	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
31		elfzelz	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in ℤ$
32	28 30 31	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \in ℤ$
33	32	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \in ℝ$
34	15	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to M + N \in ℝ$
35		elfzelz	$⊢ J \in (1 \dots M + N) \to J \in ℤ$
36	35	3ad2ant2	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in ℤ$
37		elfzle1	$⊢ J \in (1 \dots M + N) \to 1 \leq J$
38	37	3ad2ant2	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \leq J$
39	36	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in ℝ$
40		simp3	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J < I (C)$
41	39 33 40	ltled	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \leq I (C)$
42		elfz4	$⊢ ((1 \in ℤ \land I (C) \in ℤ \land J \in ℤ) \land (1 \leq J \land J \leq I (C))) \to J \in (1 \dots I (C))$
43	11 32 36 38 41 42	syl32anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in (1 \dots I (C))$
44	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))$
45	28 43 44	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))$
46		elfzle2	$⊢ S (C) (J) \in (1 \dots I (C)) \to S (C) (J) \leq I (C)$
47	45 46	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) \leq I (C)$
48		zlem1lt	$⊢ (S (C) (J) \in ℤ \land I (C) \in ℤ) \to (S (C) (J) \leq I (C) \leftrightarrow S (C) (J) - 1 < I (C))$
49	19 32 48	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))$
50	47 49	mpbid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 < I (C)$
51	27 33 50	ltled	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \leq I (C)$
52		elfzle2	$⊢ I (C) \in (1 \dots M + N) \to I (C) \leq M + N$
53	28 30 52	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \leq M + N$
54	27 33 34 51 53	letrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 \leq M + N$
55		elfz4	$⊢ ((1 \in ℤ \land M + N \in ℤ \land S (C) (J) - 1 \in ℤ) \land (1 \leq S (C) (J) - 1 \land S (C) (J) - 1 \leq M + N)) \to S (C) (J) - 1 \in (1 \dots M + N)$
56	11 15 20 24 54 55	syl32anc	$⊢ (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)$
57		biid	$⊢ S (C) (J) - 1 < I (C) \leftrightarrow S (C) (J) - 1 < I (C)$
58	50 57	sylibr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 < I (C)$
59	1 2 3 4 5 6 7 8	ballotlemi	$⊢ C \in (O ∖ E) \to I (C) = sup (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <)$
60	59	breq2d	$⊢ C \in (O ∖ E) \to (S (C) (J) - 1 < I (C) \leftrightarrow S (C) (J) - 1 < sup (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
61	60	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 < sup (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
62	58 61	mpbid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) - 1 < sup (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <)$
63		ltso	$⊢ < Or ℝ$
64	63	a1i	$⊢ C \in (O ∖ E) \to < Or ℝ$
65	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))$
66	64 65	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 < sup (\{k \in (1 \dots M + N) \| F (C) (k) = 0\} ℝ <))$
67	66	con2d	$⊢ C \in (O ∖ E) \to (S (C) (J) - 1 < sup (\{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\})$
68	28 62 67	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\}$
69		fveqeq2	$⊢ k = S (C) (J) - 1 \to (F (C) (k) = 0 \leftrightarrow F (C) (S (C) (J) - 1) = 0)$
70	69	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)$
71	68 70	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)$
72		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)$
73	71 72	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)$
74	56 73	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$
75	74	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$
76	1 2 3 4 5 6 7 8 9 10	ballotlemro	$⊢ C \in (O ∖ E) \to R (C) \in O$
77	76	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to R (C) \in O$
78		elfzelz	$⊢ J \in (1 \dots I (C)) \to J \in ℤ$
79	78	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℤ$
80	1 2 3 4 5 77 79	ballotlemfelz	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) \in ℤ$
81	80	zcnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) \in ℂ$
82	81	negeq0d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (F (R (C)) (J) = 0 \leftrightarrow - F (R (C)) (J) = 0)$
83		eqid	$⊢ (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|) = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
84	1 2 3 4 5 6 7 8 9 10 83	ballotlemfrceq	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) = - F (R (C)) (J)$
85	84	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)$
86	82 85	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)$
87	86	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)$
88	28 43 87	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)$
89	75 88	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