ballotlemsel1i

Description: The range ( 1 ... ( IC ) ) is invariant under ( SC ) . (Contributed by Thierry Arnoux, 28-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	ballotlemsel1i	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in (1 \dots I (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		ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
10		1zzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \in ℤ$
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		elfzelz	$⊢ 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 J \in (1 \dots I (C))) \to I (C) \in ℤ$
16		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
17	1 2 16	mp2an	$⊢ M + N \in ℕ$
18	17	nnzi	$⊢ M + N \in ℤ$
19	18	a1i	$⊢ C \in (O ∖ E) \to M + N \in ℤ$
20		elfzle2	$⊢ I (C) \in (1 \dots M + N) \to I (C) \leq M + N$
21	12 20	syl	$⊢ C \in (O ∖ E) \to I (C) \leq M + N$
22		eluz2	$⊢ M + N \in ℤ_{\geq I (C)} \leftrightarrow (I (C) \in ℤ \land M + N \in ℤ \land I (C) \leq M + N)$
23	14 19 21 22	syl3anbrc	$⊢ C \in (O ∖ E) \to M + N \in ℤ_{\geq I (C)}$
24		fzss2	$⊢ M + N \in ℤ_{\geq I (C)} \to (1 \dots I (C)) \subseteq (1 \dots M + N)$
25	23 24	syl	$⊢ C \in (O ∖ E) \to (1 \dots I (C)) \subseteq (1 \dots M + N)$
26	25	sselda	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in (1 \dots M + N)$
27	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)$
28	26 27	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in (1 \dots M + N)$
29		elfzelz	$⊢ S (C) (J) \in (1 \dots M + N) \to S (C) (J) \in ℤ$
30	28 29	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in ℤ$
31		elfzelz	$⊢ J \in (1 \dots I (C)) \to J \in ℤ$
32	31	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℤ$
33	32	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℝ$
34	15	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in ℝ$
35		1red	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \in ℝ$
36	34 35	readdcld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) + 1 \in ℝ$
37		elfzle2	$⊢ J \in (1 \dots I (C)) \to J \leq I (C)$
38	37	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \leq I (C)$
39	15	zcnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in ℂ$
40		1cnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \in ℂ$
41	39 40	pncand	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) + 1 - 1 = I (C)$
42	38 41	breqtrrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \leq I (C) + 1 - 1$
43	33 36 35 42	lesubd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \leq I (C) + 1 - J$
44	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)$
45	26 44	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) = if (J \leq I (C), I (C) + 1 - J, J)$
46	38	iftrued	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to if (J \leq I (C), I (C) + 1 - J, J) = I (C) + 1 - J$
47	45 46	eqtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) = I (C) + 1 - J$
48	43 47	breqtrrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \leq S (C) (J)$
49	14	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to I (C) \in ℤ$
50		elfznn	$⊢ J \in (1 \dots M + N) \to J \in ℕ$
51	50	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to J \in ℕ$
52	49 51	ltesubnnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to I (C) + 1 - J \leq I (C)$
53	26 52	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) + 1 - J \leq I (C)$
54	47 53	eqbrtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \leq I (C)$
55		elfz4	$⊢ ((1 \in ℤ \land I (C) \in ℤ \land S (C) (J) \in ℤ) \land (1 \leq S (C) (J) \land S (C) (J) \leq I (C))) \to S (C) (J) \in (1 \dots I (C))$
56	10 15 30 48 54 55	syl32anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in (1 \dots I (C))$

Metamath Proof Explorer

Theorem ballotlemsel1i

Proof