ballotlemfrceq

Description: Value of F for a reverse counting ( RC ) . (Contributed by Thierry Arnoux, 27-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) ⟼ inf (\{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	ballotlemfrceq	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) = - F (R (C)) (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) ⟼ inf (\{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 9	ballotlemsel1i	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in (1 \dots I (C))$
13		1zzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \in ℤ$
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	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (I (C) \in (1 \dots M + N) \land F (C) (I (C)) = 0)$
16	15	simpld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in (1 \dots M + N)$
17	16	elfzelzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in ℤ$
18		elfzuz3	$⊢ I (C) \in (1 \dots M + N) \to M + N \in ℤ_{\geq I (C)}$
19		fzss2	$⊢ M + N \in ℤ_{\geq I (C)} \to (1 \dots I (C)) \subseteq (1 \dots M + N)$
20	16 18 19	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots I (C)) \subseteq (1 \dots M + N)$
21		simpr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in (1 \dots I (C))$
22	20 21	sseldd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in (1 \dots M + N)$
23	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)$
24	22 23	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in (1 \dots M + N)$
25	24	elfzelzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in ℤ$
26		fzsubel	$⊢ ((1 \in ℤ \land I (C) \in ℤ) \land (S (C) (J) \in ℤ \land 1 \in ℤ)) \to (S (C) (J) \in (1 \dots I (C)) \leftrightarrow S (C) (J) - 1 \in (1 - 1 \dots I (C) - 1))$
27	13 17 25 13 26	syl22anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (S (C) (J) \in (1 \dots I (C)) \leftrightarrow S (C) (J) - 1 \in (1 - 1 \dots I (C) - 1))$
28	12 27	mpbid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) - 1 \in (1 - 1 \dots I (C) - 1)$
29		1m1e0	$⊢ 1 - 1 = 0$
30	29	oveq1i	$⊢ (1 - 1 \dots I (C) - 1) = (0 \dots I (C) - 1)$
31	28 30	eleqtrdi	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) - 1 \in (0 \dots I (C) - 1)$
32	14	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
33	32	elfzelzd	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
34		1zzd	$⊢ C \in (O ∖ E) \to 1 \in ℤ$
35	33 34	zsubcld	$⊢ C \in (O ∖ E) \to I (C) - 1 \in ℤ$
36		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
37	1 2 36	mp2an	$⊢ M + N \in ℕ$
38	37	nnzi	$⊢ M + N \in ℤ$
39	38	a1i	$⊢ C \in (O ∖ E) \to M + N \in ℤ$
40		elfzle2	$⊢ I (C) \in (1 \dots M + N) \to I (C) \leq M + N$
41	32 40	syl	$⊢ C \in (O ∖ E) \to I (C) \leq M + N$
42		zlem1lt	$⊢ (I (C) \in ℤ \land M + N \in ℤ) \to (I (C) \leq M + N \leftrightarrow I (C) - 1 < M + N)$
43	33 39 42	syl2anc	$⊢ C \in (O ∖ E) \to (I (C) \leq M + N \leftrightarrow I (C) - 1 < M + N)$
44	35	zred	$⊢ C \in (O ∖ E) \to I (C) - 1 \in ℝ$
45	39	zred	$⊢ C \in (O ∖ E) \to M + N \in ℝ$
46		ltle	$⊢ (I (C) - 1 \in ℝ \land M + N \in ℝ) \to (I (C) - 1 < M + N \to I (C) - 1 \leq M + N)$
47	44 45 46	syl2anc	$⊢ C \in (O ∖ E) \to (I (C) - 1 < M + N \to I (C) - 1 \leq M + N)$
48	43 47	sylbid	$⊢ C \in (O ∖ E) \to (I (C) \leq M + N \to I (C) - 1 \leq M + N)$
49	41 48	mpd	$⊢ C \in (O ∖ E) \to I (C) - 1 \leq M + N$
50		eluz2	$⊢ M + N \in ℤ_{\geq (I (C) - 1)} \leftrightarrow (I (C) - 1 \in ℤ \land M + N \in ℤ \land I (C) - 1 \leq M + N)$
51	35 39 49 50	syl3anbrc	$⊢ C \in (O ∖ E) \to M + N \in ℤ_{\geq (I (C) - 1)}$
52		fzss2	$⊢ M + N \in ℤ_{\geq (I (C) - 1)} \to (0 \dots I (C) - 1) \subseteq (0 \dots M + N)$
53	51 52	syl	$⊢ C \in (O ∖ E) \to (0 \dots I (C) - 1) \subseteq (0 \dots M + N)$
54	53	sselda	$⊢ (C \in (O ∖ E) \land S (C) (J) - 1 \in (0 \dots I (C) - 1)) \to S (C) (J) - 1 \in (0 \dots M + N)$
55	31 54	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) - 1 \in (0 \dots M + N)$
56	1 2 3 4 5 6 7 8 9 10 11	ballotlemfg	$⊢ (C \in (O ∖ E) \land S (C) (J) - 1 \in (0 \dots M + N)) \to F (C) (S (C) (J) - 1) = C \underset{˙}{\times} (1 \dots S (C) (J) - 1)$
57	55 56	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) = C \underset{˙}{\times} (1 \dots S (C) (J) - 1)$
58	1 2 3 4 5 6 7 8 9 10 11	ballotlemfrc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) = C \underset{˙}{\times} (S (C) (J) \dots I (C))$
59	57 58	oveq12d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) + F (R (C)) (J) = (C \underset{˙}{\times} (1 \dots S (C) (J) - 1)) + (C \underset{˙}{\times} (S (C) (J) \dots I (C)))$
60		fzsplit3	$⊢ S (C) (J) \in (1 \dots I (C)) \to (1 \dots I (C)) = (1 \dots S (C) (J) - 1) \cup (S (C) (J) \dots I (C))$
61	12 60	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots I (C)) = (1 \dots S (C) (J) - 1) \cup (S (C) (J) \dots I (C))$
62	61	oveq2d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \underset{˙}{\times} (1 \dots I (C)) = C \underset{˙}{\times} ((1 \dots S (C) (J) - 1) \cup (S (C) (J) \dots I (C)))$
63		fz1ssfz0	$⊢ (1 \dots M + N) \subseteq (0 \dots M + N)$
64	63	sseli	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in (0 \dots M + N)$
65	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))$
66	64 65	sylan2	$⊢ (C \in (O ∖ E) \land I (C) \in (1 \dots M + N)) \to F (C) (I (C)) = C \underset{˙}{\times} (1 \dots I (C))$
67	16 66	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (I (C)) = C \underset{˙}{\times} (1 \dots I (C))$
68	15	simprd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (I (C)) = 0$
69	67 68	eqtr3d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \underset{˙}{\times} (1 \dots I (C)) = 0$
70		fzfi	$⊢ (1 \dots M + N) \in Fin$
71		eldifi	$⊢ C \in (O ∖ E) \to C \in O$
72	1 2 3	ballotlemelo	$⊢ C \in O \leftrightarrow (C \subseteq (1 \dots M + N) \land \|C\| = M)$
73	72	simplbi	$⊢ C \in O \to C \subseteq (1 \dots M + N)$
74	71 73	syl	$⊢ C \in (O ∖ E) \to C \subseteq (1 \dots M + N)$
75		ssfi	$⊢ ((1 \dots M + N) \in Fin \land C \subseteq (1 \dots M + N)) \to C \in Fin$
76	70 74 75	sylancr	$⊢ C \in (O ∖ E) \to C \in Fin$
77	76	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \in Fin$
78		fzfid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots S (C) (J) - 1) \in Fin$
79		fzfid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (S (C) (J) \dots I (C)) \in Fin$
80	25	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) \in ℝ$
81		ltm1	$⊢ S (C) (J) \in ℝ \to S (C) (J) - 1 < S (C) (J)$
82		fzdisj	$⊢ S (C) (J) - 1 < S (C) (J) \to (1 \dots S (C) (J) - 1) \cap (S (C) (J) \dots I (C)) = \emptyset$
83	80 81 82	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots S (C) (J) - 1) \cap (S (C) (J) \dots I (C)) = \emptyset$
84	1 2 3 4 5 6 7 8 9 10 11 77 78 79 83	ballotlemgun	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \underset{˙}{\times} ((1 \dots S (C) (J) - 1) \cup (S (C) (J) \dots I (C))) = (C \underset{˙}{\times} (1 \dots S (C) (J) - 1)) + (C \underset{˙}{\times} (S (C) (J) \dots I (C)))$
85	62 69 84	3eqtr3rd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (C \underset{˙}{\times} (1 \dots S (C) (J) - 1)) + (C \underset{˙}{\times} (S (C) (J) \dots I (C))) = 0$
86	59 85	eqtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) + F (R (C)) (J) = 0$
87	71	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to C \in O$
88	25 13	zsubcld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) - 1 \in ℤ$
89	1 2 3 4 5 87 88	ballotlemfelz	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) \in ℤ$
90	89	zcnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) \in ℂ$
91	1 2 3 4 5 6 7 8 9 10	ballotlemro	$⊢ C \in (O ∖ E) \to R (C) \in O$
92	91	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to R (C) \in O$
93	21	elfzelzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℤ$
94	1 2 3 4 5 92 93	ballotlemfelz	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) \in ℤ$
95	94	zcnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (R (C)) (J) \in ℂ$
96		addeq0	$⊢ (F (C) (S (C) (J) - 1) \in ℂ \land F (R (C)) (J) \in ℂ) \to (F (C) (S (C) (J) - 1) + F (R (C)) (J) = 0 \leftrightarrow F (C) (S (C) (J) - 1) = - F (R (C)) (J))$
97	90 95 96	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (F (C) (S (C) (J) - 1) + F (R (C)) (J) = 0 \leftrightarrow F (C) (S (C) (J) - 1) = - F (R (C)) (J))$
98	86 97	mpbid	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to F (C) (S (C) (J) - 1) = - F (R (C)) (J)$

Metamath Proof Explorer

Theorem ballotlemfrceq

Proof