ballotlemsv

Description: Value of S evaluated at J 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	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)$

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	ballotlemsval	$⊢ C \in (O ∖ E) \to S (C) = (i \in (1 \dots M + N) ⟼ if (i \leq I (C), I (C) + 1 - i, i))$
11		breq1	$⊢ i = j \to (i \leq I (C) \leftrightarrow j \leq I (C))$
12		oveq2	$⊢ i = j \to I (C) + 1 - i = I (C) + 1 - j$
13		id	$⊢ i = j \to i = j$
14	11 12 13	ifbieq12d	$⊢ i = j \to if (i \leq I (C), I (C) + 1 - i, i) = if (j \leq I (C), I (C) + 1 - j, j)$
15	14	cbvmptv	$⊢ (i \in (1 \dots M + N) ⟼ if (i \leq I (C), I (C) + 1 - i, i)) = (j \in (1 \dots M + N) ⟼ if (j \leq I (C), I (C) + 1 - j, j))$
16	10 15	eqtrdi	$⊢ C \in (O ∖ E) \to S (C) = (j \in (1 \dots M + N) ⟼ if (j \leq I (C), I (C) + 1 - j, j))$
17	16	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) = (j \in (1 \dots M + N) ⟼ if (j \leq I (C), I (C) + 1 - j, j))$
18		simpr	$⊢ (C \in (O ∖ E) \land j = J) \to j = J$
19	18	breq1d	$⊢ (C \in (O ∖ E) \land j = J) \to (j \leq I (C) \leftrightarrow J \leq I (C))$
20	18	oveq2d	$⊢ (C \in (O ∖ E) \land j = J) \to I (C) + 1 - j = I (C) + 1 - J$
21	19 20 18	ifbieq12d	$⊢ (C \in (O ∖ E) \land j = J) \to if (j \leq I (C), I (C) + 1 - j, j) = if (J \leq I (C), I (C) + 1 - J, J)$
22	21	adantlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land j = J) \to if (j \leq I (C), I (C) + 1 - j, j) = if (J \leq I (C), I (C) + 1 - J, J)$
23		simpr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to J \in (1 \dots M + N)$
24		ovexd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land J \leq I (C)) \to I (C) + 1 - J \in V$
25		elex	$⊢ J \in (1 \dots M + N) \to J \in V$
26	25	ad2antlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots M + N)) \land \neg J \leq I (C)) \to J \in V$
27	24 26	ifclda	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to if (J \leq I (C), I (C) + 1 - J, J) \in V$
28	17 22 23 27	fvmptd	$⊢ (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)$

Metamath Proof Explorer

Theorem ballotlemsv

Proof