ballotlemfrci

Description: Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-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)))$
	ballotth.r	$⊢ R = (c \in (O ∖ E) ⟼ S (c) [c])$
	ballotlemg	$⊢ \underset{˙}{\times} = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
Assertion	ballotlemfrci	$⊢ C \in (O ∖ E) \to F (R (C)) (I (C)) = 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		ballotlemg	$⊢ \underset{˙}{\times} = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
12	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)$
13	12	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
14		elfzuz	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in ℤ_{\geq 1}$
15		eluzfz2	$⊢ I (C) \in ℤ_{\geq 1} \to I (C) \in (1 \dots I (C))$
16	13 14 15	3syl	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots I (C))$
17	1 2 3 4 5 6 7 8 9 10 11	ballotlemfrc	$⊢ (C \in (O ∖ E) \land I (C) \in (1 \dots I (C))) \to F (R (C)) (I (C)) = C \underset{˙}{\times} (S (C) (I (C)) \dots I (C))$
18	16 17	mpdan	$⊢ C \in (O ∖ E) \to F (R (C)) (I (C)) = C \underset{˙}{\times} (S (C) (I (C)) \dots I (C))$
19	1 2 3 4 5 6 7 8 9	ballotlemsi	$⊢ C \in (O ∖ E) \to S (C) (I (C)) = 1$
20	19	oveq1d	$⊢ C \in (O ∖ E) \to (S (C) (I (C)) \dots I (C)) = (1 \dots I (C))$
21	20	oveq2d	$⊢ C \in (O ∖ E) \to C \underset{˙}{\times} (S (C) (I (C)) \dots I (C)) = C \underset{˙}{\times} (1 \dots I (C))$
22	18 21	eqtrd	$⊢ C \in (O ∖ E) \to F (R (C)) (I (C)) = C \underset{˙}{\times} (1 \dots I (C))$
23		fz1ssfz0	$⊢ (1 \dots M + N) \subseteq (0 \dots M + N)$
24	23 13	sselid	$⊢ C \in (O ∖ E) \to I (C) \in (0 \dots M + N)$
25	1 2 3 4 5 6 7 8 9 10 11	ballotlemfg	$⊢ (C \in (O ∖ E) \land I (C) \in (0 \dots M + N)) \to F (C) (I (C)) = C \underset{˙}{\times} (1 \dots I (C))$
26	24 25	mpdan	$⊢ C \in (O ∖ E) \to F (C) (I (C)) = C \underset{˙}{\times} (1 \dots I (C))$
27	12	simprd	$⊢ C \in (O ∖ E) \to F (C) (I (C)) = 0$
28	22 26 27	3eqtr2d	$⊢ C \in (O ∖ E) \to F (R (C)) (I (C)) = 0$

Metamath Proof Explorer

Theorem ballotlemfrci

Proof