Metamath Proof Explorer


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 )