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