Metamath Proof Explorer

Theorem ballotlemfelz

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

Ref Expression
Hypotheses ballotth.m 
|- M e. NN
ballotth.n 
|- N e. NN
ballotth.o 
|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
ballotth.p 
|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
ballotth.f 
|- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
ballotlemfval.c 
|- ( ph -> C e. O )
ballotlemfval.j 
|- ( ph -> J e. ZZ )
Assertion ballotlemfelz 
|- ( ph -> ( ( F ` C ) ` J ) e. ZZ )

Proof

Step Hyp Ref Expression
1 ballotth.m 
 |-  M e. NN
2 ballotth.n 
 |-  N e. NN
3 ballotth.o 
 |-  O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4 ballotth.p 
 |-  P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
5 ballotth.f 
 |-  F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
6 ballotlemfval.c 
 |-  ( ph -> C e. O )
7 ballotlemfval.j 
 |-  ( ph -> J e. ZZ )
8 1 2 3 4 5 6 7 ballotlemfval 
 |-  ( ph -> ( ( F ` C ) ` J ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )
9 fzfi 
 |-  ( 1 ... J ) e. Fin
10 inss1 
 |-  ( ( 1 ... J ) i^i C ) C_ ( 1 ... J )
11 ssfi 
 |-  ( ( ( 1 ... J ) e. Fin /\ ( ( 1 ... J ) i^i C ) C_ ( 1 ... J ) ) -> ( ( 1 ... J ) i^i C ) e. Fin )
12 9 10 11 mp2an 
 |-  ( ( 1 ... J ) i^i C ) e. Fin
13 hashcl 
 |-  ( ( ( 1 ... J ) i^i C ) e. Fin -> ( # ` ( ( 1 ... J ) i^i C ) ) e. NN0 )
14 12 13 ax-mp 
 |-  ( # ` ( ( 1 ... J ) i^i C ) ) e. NN0
15 14 nn0zi 
 |-  ( # ` ( ( 1 ... J ) i^i C ) ) e. ZZ
16 difss 
 |-  ( ( 1 ... J ) \ C ) C_ ( 1 ... J )
17 ssfi 
 |-  ( ( ( 1 ... J ) e. Fin /\ ( ( 1 ... J ) \ C ) C_ ( 1 ... J ) ) -> ( ( 1 ... J ) \ C ) e. Fin )
18 9 16 17 mp2an 
 |-  ( ( 1 ... J ) \ C ) e. Fin
19 hashcl 
 |-  ( ( ( 1 ... J ) \ C ) e. Fin -> ( # ` ( ( 1 ... J ) \ C ) ) e. NN0 )
20 18 19 ax-mp 
 |-  ( # ` ( ( 1 ... J ) \ C ) ) e. NN0
21 20 nn0zi 
 |-  ( # ` ( ( 1 ... J ) \ C ) ) e. ZZ
22 zsubcl 
 |-  ( ( ( # ` ( ( 1 ... J ) i^i C ) ) e. ZZ /\ ( # ` ( ( 1 ... J ) \ C ) ) e. ZZ ) -> ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) e. ZZ )
23 15 21 22 mp2an 
 |-  ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) e. ZZ
24 8 23 eqeltrdi 
 |-  ( ph -> ( ( F ` C ) ` J ) e. ZZ )