ballotlemsdom

Description: Domain of S for a given counting C . (Contributed by Thierry Arnoux, 12-Apr-2017)

	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)))$
Assertion	ballotlemsdom	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) \in (1 \dots M + N)$

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	1 2 3 4 5 6 7 8 9	ballotlemsv	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) = if (J \leq I (C), I (C) + 1 - J, J)$
11		fzssuz	$⊢ (1 \dots M + N) \subseteq ℤ_{\geq 1}$
12		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
13	11 12	sstri	$⊢ (1 \dots M + N) \subseteq ℤ$
14	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)$
15	14	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
16	13 15	sseldi	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
17	16	ad2antrr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to I (C) \in ℤ$
18		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
19	1 2 18	mp2an	$⊢ M + N \in ℕ$
20	19	nnzi	$⊢ M + N \in ℤ$
21	20	a1i	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to M + N \in ℤ$
22	15	ad2antrr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to I (C) \in (1 \dots M + N)$
23		elfzle2	$⊢ I (C) \in (1 \dots M + N) \to I (C) \leq M + N$
24	22 23	syl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to I (C) \leq M + N$
25		eluz2	$⊢ M + N \in ℤ_{\geq I (C)} \leftrightarrow (I (C) \in ℤ \land M + N \in ℤ \land I (C) \leq M + N)$
26		fzss2	$⊢ M + N \in ℤ_{\geq I (C)} \to (1 \dots I (C)) \subseteq (1 \dots M + N)$
27	25 26	sylbir	$⊢ (I (C) \in ℤ \land M + N \in ℤ \land I (C) \leq M + N) \to (1 \dots I (C)) \subseteq (1 \dots M + N)$
28	17 21 24 27	syl3anc	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to (1 \dots I (C)) \subseteq (1 \dots M + N)$
29		1zzd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to 1 \in ℤ$
30		simplr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to J \in (1 \dots M + N)$
31	13 30	sseldi	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to J \in ℤ$
32		elfzle1	$⊢ J \in (1 \dots M + N) \to 1 \leq J$
33	30 32	syl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to 1 \leq J$
34		simpr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to J \leq I (C)$
35		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))$
36	29 17 31 33 34 35	syl32anc	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to J \in (1 \dots I (C))$
37		fzrev3i	$⊢ J \in (1 \dots I (C)) \to 1 + I (C) - J \in (1 \dots I (C))$
38	36 37	syl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to 1 + I (C) - J \in (1 \dots I (C))$
39		1cnd	$⊢ C \in (O ∖ E) \to 1 \in ℂ$
40	16	zcnd	$⊢ C \in (O ∖ E) \to I (C) \in ℂ$
41	39 40	addcomd	$⊢ C \in (O ∖ E) \to 1 + I (C) = I (C) + 1$
42	41	oveq1d	$⊢ C \in (O ∖ E) \to 1 + I (C) - J = I (C) + 1 - J$
43	42	eleq1d	$⊢ C \in (O ∖ E) \to (1 + I (C) - J \in (1 \dots I (C)) \leftrightarrow I (C) + 1 - J \in (1 \dots I (C)))$
44	43	ad2antrr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to (1 + I (C) - J \in (1 \dots I (C)) \leftrightarrow I (C) + 1 - J \in (1 \dots I (C)))$
45	38 44	mpbid	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to I (C) + 1 - J \in (1 \dots I (C))$
46	28 45	sseldd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to I (C) + 1 - J \in (1 \dots M + N)$
47		simplr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land \neg J \leq I (C)) \to J \in (1 \dots M + N)$
48	46 47	ifclda	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to if (J \leq I (C), I (C) + 1 - J, J) \in (1 \dots M + N)$
49	10 48	eqeltrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) \in (1 \dots M + N)$

Metamath Proof Explorer

Theorem ballotlemsdom

Proof