Metamath Proof Explorer

Theorem ballotlemfelz

Description: ( FC ) has values in ZZ . (Contributed by Thierry Arnoux, 23-Nov-2016)

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

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotlemfval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑂 )
7 ballotlemfval.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
8 1 2 3 4 5 6 7 ballotlemfval ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )
9 fzfi ⊢ ( 1 ... 𝐽 ) ∈ Fin
10 inss1 ⊢ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ⊆ ( 1 ... 𝐽 )
11 ssfi ⊢ ( ( ( 1 ... 𝐽 ) ∈ Fin ∧ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ⊆ ( 1 ... 𝐽 ) ) → ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ∈ Fin )
12 9 10 11 mp2an ⊢ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ∈ Fin
13 hashcl ⊢ ( ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ∈ Fin → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) ∈ ℕ0 )
14 12 13 ax-mp ⊢ ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) ∈ ℕ0
15 14 nn0zi ⊢ ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) ∈ ℤ
16 difss ⊢ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ⊆ ( 1 ... 𝐽 )
17 ssfi ⊢ ( ( ( 1 ... 𝐽 ) ∈ Fin ∧ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ⊆ ( 1 ... 𝐽 ) ) → ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ∈ Fin )
18 9 16 17 mp2an ⊢ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ∈ Fin
19 hashcl ⊢ ( ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ∈ Fin → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ∈ ℕ0 )
20 18 19 ax-mp ⊢ ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ∈ ℕ0
21 20 nn0zi ⊢ ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ∈ ℤ
22 zsubcl ⊢ ( ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) ∈ ℤ ∧ ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ∈ ℤ ) → ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) ∈ ℤ )
23 15 21 22 mp2an ⊢ ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) ∈ ℤ
24 8 23 eqeltrdi ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )