Theorem ballotlemfval0

Description: ( FC ) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016)

	Ref	Expression
Hypotheses	ballotth.m	⊢ 𝑀 ∈ ℕ
	ballotth.n	⊢ 𝑁 ∈ ℕ
	ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
	ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
	ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
Assertion	ballotlemfval0	⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	⊢ 𝑀 ∈ ℕ
2		ballotth.n	⊢ 𝑁 ∈ ℕ
3		ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4		ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5		ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6		id	⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ∈ 𝑂 )
7		0zd	⊢ ( 𝐶 ∈ 𝑂 → 0 ∈ ℤ )
8	1 2 3 4 5 6 7	ballotlemfval	⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = ( ( ♯ ‘ ( ( 1 ... 0 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 0 ) ∖ 𝐶 ) ) ) )
9		fz10	⊢ ( 1 ... 0 ) = ∅
10	9	ineq1i	⊢ ( ( 1 ... 0 ) ∩ 𝐶 ) = ( ∅ ∩ 𝐶 )
11		incom	⊢ ( 𝐶 ∩ ∅ ) = ( ∅ ∩ 𝐶 )
12		in0	⊢ ( 𝐶 ∩ ∅ ) = ∅
13	10 11 12	3eqtr2i	⊢ ( ( 1 ... 0 ) ∩ 𝐶 ) = ∅
14	13	fveq2i	⊢ ( ♯ ‘ ( ( 1 ... 0 ) ∩ 𝐶 ) ) = ( ♯ ‘ ∅ )
15		hash0	⊢ ( ♯ ‘ ∅ ) = 0
16	14 15	eqtri	⊢ ( ♯ ‘ ( ( 1 ... 0 ) ∩ 𝐶 ) ) = 0
17	9	difeq1i	⊢ ( ( 1 ... 0 ) ∖ 𝐶 ) = ( ∅ ∖ 𝐶 )
18		0dif	⊢ ( ∅ ∖ 𝐶 ) = ∅
19	17 18	eqtri	⊢ ( ( 1 ... 0 ) ∖ 𝐶 ) = ∅
20	19	fveq2i	⊢ ( ♯ ‘ ( ( 1 ... 0 ) ∖ 𝐶 ) ) = ( ♯ ‘ ∅ )
21	20 15	eqtri	⊢ ( ♯ ‘ ( ( 1 ... 0 ) ∖ 𝐶 ) ) = 0
22	16 21	oveq12i	⊢ ( ( ♯ ‘ ( ( 1 ... 0 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 0 ) ∖ 𝐶 ) ) ) = ( 0 − 0 )
23		0m0e0	⊢ ( 0 − 0 ) = 0
24	22 23	eqtri	⊢ ( ( ♯ ‘ ( ( 1 ... 0 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 0 ) ∖ 𝐶 ) ) ) = 0
25	8 24	eqtrdi	⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )