Theorem ballotlemfelz

Description: ( FC ) has values in ZZ . (Contributed by Thierry Arnoux, 23-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)$$
	ballotlemfval.c	$$⊢\phi \to C\in O$$
	ballotlemfval.j	$$⊢\phi \to J\in \mathbb{Z}$$
Assertion	ballotlemfelz	$$⊢\phi \to F\left(C\right)\left(J\right)\in \mathbb{Z}$$

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		ballotlemfval.c	$$⊢\phi \to C\in O$$
7		ballotlemfval.j	$$⊢\phi \to J\in \mathbb{Z}$$
8	1 2 3 4 5 6 7	ballotlemfval	$$⊢\phi \to F\left(C\right)\left(J\right)=\left|\left(1\dots J\right)\cap C\right|-\left|\left(1\dots J\right)\setminus C\right|$$
9		fzfi	$$⊢\left(1\dots J\right)\in \mathrm{Fin}$$
10		inss1	$$⊢\left(1\dots J\right)\cap C\subseteq \left(1\dots J\right)$$
11		ssfi	$$⊢\left(\left(1\dots J\right)\in \mathrm{Fin}\wedge \left(1\dots J\right)\cap C\subseteq \left(1\dots J\right)\right)\to \left(1\dots J\right)\cap C\in \mathrm{Fin}$$
12	9 10 11	mp2an	$$⊢\left(1\dots J\right)\cap C\in \mathrm{Fin}$$
13		hashcl	$$⊢\left(1\dots J\right)\cap C\in \mathrm{Fin}\to \left|\left(1\dots J\right)\cap C\right|\in {\mathbb{N}}_0$$
14	12 13	ax-mp	$$⊢\left|\left(1\dots J\right)\cap C\right|\in {\mathbb{N}}_0$$
15	14	nn0zi	$$⊢\left|\left(1\dots J\right)\cap C\right|\in \mathbb{Z}$$
16		difss	$$⊢\left(1\dots J\right)\setminus C\subseteq \left(1\dots J\right)$$
17		ssfi	$$⊢\left(\left(1\dots J\right)\in \mathrm{Fin}\wedge \left(1\dots J\right)\setminus C\subseteq \left(1\dots J\right)\right)\to \left(1\dots J\right)\setminus C\in \mathrm{Fin}$$
18	9 16 17	mp2an	$$⊢\left(1\dots J\right)\setminus C\in \mathrm{Fin}$$
19		hashcl	$$⊢\left(1\dots J\right)\setminus C\in \mathrm{Fin}\to \left|\left(1\dots J\right)\setminus C\right|\in {\mathbb{N}}_0$$
20	18 19	ax-mp	$$⊢\left|\left(1\dots J\right)\setminus C\right|\in {\mathbb{N}}_0$$
21	20	nn0zi	$$⊢\left|\left(1\dots J\right)\setminus C\right|\in \mathbb{Z}$$
22		zsubcl	$$⊢\left(\left|\left(1\dots J\right)\cap C\right|\in \mathbb{Z}\wedge \left|\left(1\dots J\right)\setminus C\right|\in \mathbb{Z}\right)\to \left|\left(1\dots J\right)\cap C\right|-\left|\left(1\dots J\right)\setminus C\right|\in \mathbb{Z}$$
23	15 21 22	mp2an	$$⊢\left|\left(1\dots J\right)\cap C\right|-\left|\left(1\dots J\right)\setminus C\right|\in \mathbb{Z}$$
24	8 23	eqeltrdi	$$⊢\phi \to F\left(C\right)\left(J\right)\in \mathbb{Z}$$