Theorem ballotlemfval0

Description: ( FC ) always starts counting at 0 . (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	ballotlemfval0	$$⊢C\in O\to F\left(C\right)\left(0\right)=0$$

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		0zd	$$⊢C\in O\to 0\in \mathbb{Z}$$
8	1 2 3 4 5 6 7	ballotlemfval	$$⊢C\in O\to F\left(C\right)\left(0\right)=\left|\left(1\dots 0\right)\cap C\right|-\left|\left(1\dots 0\right)\setminus C\right|$$
9		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
10	9	ineq1i	$$⊢\left(1\dots 0\right)\cap C=\varnothing \cap C$$
11		incom	$$⊢C\cap \varnothing =\varnothing \cap C$$
12		in0	$$⊢C\cap \varnothing =\varnothing$$
13	10 11 12	3eqtr2i	$$⊢\left(1\dots 0\right)\cap C=\varnothing$$
14	13	fveq2i	$$⊢\left|\left(1\dots 0\right)\cap C\right|=\left|\varnothing \right|$$
15		hash0	$$⊢\left|\varnothing \right|=0$$
16	14 15	eqtri	$$⊢\left|\left(1\dots 0\right)\cap C\right|=0$$
17	9	difeq1i	$$⊢\left(1\dots 0\right)\setminus C=\varnothing \setminus C$$
18		0dif	$$⊢\varnothing \setminus C=\varnothing$$
19	17 18	eqtri	$$⊢\left(1\dots 0\right)\setminus C=\varnothing$$
20	19	fveq2i	$$⊢\left|\left(1\dots 0\right)\setminus C\right|=\left|\varnothing \right|$$
21	20 15	eqtri	$$⊢\left|\left(1\dots 0\right)\setminus C\right|=0$$
22	16 21	oveq12i	$$⊢\left|\left(1\dots 0\right)\cap C\right|-\left|\left(1\dots 0\right)\setminus C\right|=0-0$$
23		0m0e0	$$⊢0-0=0$$
24	22 23	eqtri	$$⊢\left|\left(1\dots 0\right)\cap C\right|-\left|\left(1\dots 0\right)\setminus C\right|=0$$
25	8 24	eqtrdi	$$⊢C\in O\to F\left(C\right)\left(0\right)=0$$