Theorem ballotlemfmpn

Description: ( FC ) finishes counting at ( M - N ) . (Contributed by Thierry Arnoux, 25-Nov-2016)

	Ref	Expression
Hypotheses	ballotth.m	$$⊢M\in \mathbb{N}$$
	ballotth.n	$$⊢N\in \mathbb{N}$$
	ballotth.o	$$⊢O=\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}$$
	ballotth.p	$$⊢P=\left(x\in 𝒫O⟼\frac{\left|x\right|}{\left|O\right|}\right)$$
	ballotth.f	$$⊢F=\left(c\in O⟼\left(i\in \mathbb{Z}⟼\left|\left(1\dots i\right)\cap c\right|-\left|\left(1\dots i\right)\setminus c\right|\right)\right)$$
Assertion	ballotlemfmpn	$$⊢C\in O\to F\left(C\right)\left(M+N\right)=M-N$$

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	$$⊢M\in \mathbb{N}$$
2		ballotth.n	$$⊢N\in \mathbb{N}$$
3		ballotth.o	$$⊢O=\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}$$
4		ballotth.p	$$⊢P=\left(x\in 𝒫O⟼\frac{\left|x\right|}{\left|O\right|}\right)$$
5		ballotth.f	$$⊢F=\left(c\in O⟼\left(i\in \mathbb{Z}⟼\left|\left(1\dots i\right)\cap c\right|-\left|\left(1\dots i\right)\setminus c\right|\right)\right)$$
6		id	$$⊢C\in O\to C\in O$$
7		nnaddcl	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to M+N\in \mathbb{N}$$
8	1 2 7	mp2an	$$⊢M+N\in \mathbb{N}$$
9	8	nnzi	$$⊢M+N\in \mathbb{Z}$$
10	9	a1i	$$⊢C\in O\to M+N\in \mathbb{Z}$$
11	1 2 3 4 5 6 10	ballotlemfval	$$⊢C\in O\to F\left(C\right)\left(M+N\right)=\left|\left(1\dots M+N\right)\cap C\right|-\left|\left(1\dots M+N\right)\setminus C\right|$$
12		ssrab2	$$⊢\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}\subseteq 𝒫\left(1\dots M+N\right)$$
13	3 12	eqsstri	$$⊢O\subseteq 𝒫\left(1\dots M+N\right)$$
14	13	sseli	$$⊢C\in O\to C\in 𝒫\left(1\dots M+N\right)$$
15	14	elpwid	$$⊢C\in O\to C\subseteq \left(1\dots M+N\right)$$
16		sseqin2	$$⊢C\subseteq \left(1\dots M+N\right)\leftrightarrow \left(1\dots M+N\right)\cap C=C$$
17	15 16	sylib	$$⊢C\in O\to \left(1\dots M+N\right)\cap C=C$$
18	17	fveq2d	$$⊢C\in O\to \left|\left(1\dots M+N\right)\cap C\right|=\left|C\right|$$
19		rabssab	$$⊢\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}\subseteq \left\{c|\left|c\right|=M\right\}$$
20	19	sseli	$$⊢C\in \left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}\to C\in \left\{c|\left|c\right|=M\right\}$$
21	20 3	eleq2s	$$⊢C\in O\to C\in \left\{c|\left|c\right|=M\right\}$$
22		fveqeq2	$$⊢b=C\to \left(\left|b\right|=M\leftrightarrow \left|C\right|=M\right)$$
23		fveqeq2	$$⊢c=b\to \left(\left|c\right|=M\leftrightarrow \left|b\right|=M\right)$$
24	23	cbvabv	$$⊢\left\{c|\left|c\right|=M\right\}=\left\{b|\left|b\right|=M\right\}$$
25	22 24	elab2g	$$⊢C\in O\to \left(C\in \left\{c|\left|c\right|=M\right\}\leftrightarrow \left|C\right|=M\right)$$
26	21 25	mpbid	$$⊢C\in O\to \left|C\right|=M$$
27	18 26	eqtrd	$$⊢C\in O\to \left|\left(1\dots M+N\right)\cap C\right|=M$$
28		fzfi	$$⊢\left(1\dots M+N\right)\in \mathrm{Fin}$$
29		hashssdif	$$⊢\left(\left(1\dots M+N\right)\in \mathrm{Fin}\wedge C\subseteq \left(1\dots M+N\right)\right)\to \left|\left(1\dots M+N\right)\setminus C\right|=\left|\left(1\dots M+N\right)\right|-\left|C\right|$$
30	28 15 29	sylancr	$$⊢C\in O\to \left|\left(1\dots M+N\right)\setminus C\right|=\left|\left(1\dots M+N\right)\right|-\left|C\right|$$
31	8	nnnn0i	$$⊢M+N\in {\mathbb{N}}_0$$
32		hashfz1	$$⊢M+N\in {\mathbb{N}}_0\to \left|\left(1\dots M+N\right)\right|=M+N$$
33	31 32	mp1i	$$⊢C\in O\to \left|\left(1\dots M+N\right)\right|=M+N$$
34	33 26	oveq12d	$$⊢C\in O\to \left|\left(1\dots M+N\right)\right|-\left|C\right|=M+N-M$$
35	1	nncni	$$⊢M\in ℂ$$
36	2	nncni	$$⊢N\in ℂ$$
37		pncan2	$$⊢\left(M\in ℂ\wedge N\in ℂ\right)\to M+N-M=N$$
38	35 36 37	mp2an	$$⊢M+N-M=N$$
39	38	a1i	$$⊢C\in O\to M+N-M=N$$
40	30 34 39	3eqtrd	$$⊢C\in O\to \left|\left(1\dots M+N\right)\setminus C\right|=N$$
41	27 40	oveq12d	$$⊢C\in O\to \left|\left(1\dots M+N\right)\cap C\right|-\left|\left(1\dots M+N\right)\setminus C\right|=M-N$$
42	11 41	eqtrd	$$⊢C\in O\to F\left(C\right)\left(M+N\right)=M-N$$