Metamath Proof Explorer

Theorem ballotlemfmpn

Description: ( FC ) finishes counting at ( M - N ) . (Contributed by Thierry Arnoux, 25-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 ) ) ) ) )
Assertion ballotlemfmpn 
|- ( C e. O -> ( ( F ` C ) ` ( M + N ) ) = ( M - N ) )

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 id 
 |-  ( C e. O -> C e. O )
7 nnaddcl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M + N ) e. NN )
8 1 2 7 mp2an 
 |-  ( M + N ) e. NN
9 8 nnzi 
 |-  ( M + N ) e. ZZ
10 9 a1i 
 |-  ( C e. O -> ( M + N ) e. ZZ )
11 1 2 3 4 5 6 10 ballotlemfval 
 |-  ( C e. O -> ( ( F ` C ) ` ( M + N ) ) = ( ( # ` ( ( 1 ... ( M + N ) ) i^i C ) ) - ( # ` ( ( 1 ... ( M + N ) ) \ C ) ) ) )
12 ssrab2 
 |-  { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } C_ ~P ( 1 ... ( M + N ) )
13 3 12 eqsstri 
 |-  O C_ ~P ( 1 ... ( M + N ) )
14 13 sseli 
 |-  ( C e. O -> C e. ~P ( 1 ... ( M + N ) ) )
15 14 elpwid 
 |-  ( C e. O -> C C_ ( 1 ... ( M + N ) ) )
16 sseqin2 
 |-  ( C C_ ( 1 ... ( M + N ) ) <-> ( ( 1 ... ( M + N ) ) i^i C ) = C )
17 15 16 sylib 
 |-  ( C e. O -> ( ( 1 ... ( M + N ) ) i^i C ) = C )
18 17 fveq2d 
 |-  ( C e. O -> ( # ` ( ( 1 ... ( M + N ) ) i^i C ) ) = ( # ` C ) )
19 rabssab 
 |-  { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } C_ { c | ( # ` c ) = M }
20 19 sseli 
 |-  ( C e. { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } -> C e. { c | ( # ` c ) = M } )
21 20 3 eleq2s 
 |-  ( C e. O -> C e. { c | ( # ` c ) = M } )
22 fveqeq2 
 |-  ( b = C -> ( ( # ` b ) = M <-> ( # ` C ) = M ) )
23 fveqeq2 
 |-  ( c = b -> ( ( # ` c ) = M <-> ( # ` b ) = M ) )
24 23 cbvabv 
 |-  { c | ( # ` c ) = M } = { b | ( # ` b ) = M }
25 22 24 elab2g 
 |-  ( C e. O -> ( C e. { c | ( # ` c ) = M } <-> ( # ` C ) = M ) )
26 21 25 mpbid 
 |-  ( C e. O -> ( # ` C ) = M )
27 18 26 eqtrd 
 |-  ( C e. O -> ( # ` ( ( 1 ... ( M + N ) ) i^i C ) ) = M )
28 fzfi 
 |-  ( 1 ... ( M + N ) ) e. Fin
29 hashssdif 
 |-  ( ( ( 1 ... ( M + N ) ) e. Fin /\ C C_ ( 1 ... ( M + N ) ) ) -> ( # ` ( ( 1 ... ( M + N ) ) \ C ) ) = ( ( # ` ( 1 ... ( M + N ) ) ) - ( # ` C ) ) )
30 28 15 29 sylancr 
 |-  ( C e. O -> ( # ` ( ( 1 ... ( M + N ) ) \ C ) ) = ( ( # ` ( 1 ... ( M + N ) ) ) - ( # ` C ) ) )
31 8 nnnn0i 
 |-  ( M + N ) e. NN0
32 hashfz1 
 |-  ( ( M + N ) e. NN0 -> ( # ` ( 1 ... ( M + N ) ) ) = ( M + N ) )
33 31 32 mp1i 
 |-  ( C e. O -> ( # ` ( 1 ... ( M + N ) ) ) = ( M + N ) )
34 33 26 oveq12d 
 |-  ( C e. O -> ( ( # ` ( 1 ... ( M + N ) ) ) - ( # ` C ) ) = ( ( M + N ) - M ) )
35 1 nncni 
 |-  M e. CC
36 2 nncni 
 |-  N e. CC
37 pncan2 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - M ) = N )
38 35 36 37 mp2an 
 |-  ( ( M + N ) - M ) = N
39 38 a1i 
 |-  ( C e. O -> ( ( M + N ) - M ) = N )
40 30 34 39 3eqtrd 
 |-  ( C e. O -> ( # ` ( ( 1 ... ( M + N ) ) \ C ) ) = N )
41 27 40 oveq12d 
 |-  ( C e. O -> ( ( # ` ( ( 1 ... ( M + N ) ) i^i C ) ) - ( # ` ( ( 1 ... ( M + N ) ) \ C ) ) ) = ( M - N ) )
42 11 41 eqtrd 
 |-  ( C e. O -> ( ( F ` C ) ` ( M + N ) ) = ( M - N ) )