Metamath Proof Explorer

Theorem ballotlem1

Description: The size of the universe is a binomial coefficient. (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 }
Assertion ballotlem1 
|- ( # ` O ) = ( ( M + N ) _C M )

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 3 fveq2i 
 |-  ( # ` O ) = ( # ` { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } )
5 fzfi 
 |-  ( 1 ... ( M + N ) ) e. Fin
6 1 nnzi 
 |-  M e. ZZ
7 hashbc 
 |-  ( ( ( 1 ... ( M + N ) ) e. Fin /\ M e. ZZ ) -> ( ( # ` ( 1 ... ( M + N ) ) ) _C M ) = ( # ` { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } ) )
8 5 6 7 mp2an 
 |-  ( ( # ` ( 1 ... ( M + N ) ) ) _C M ) = ( # ` { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } )
9 1 2 pm3.2i 
 |-  ( M e. NN /\ N e. NN )
10 nnaddcl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M + N ) e. NN )
11 nnnn0 
 |-  ( ( M + N ) e. NN -> ( M + N ) e. NN0 )
12 9 10 11 mp2b 
 |-  ( M + N ) e. NN0
13 hashfz1 
 |-  ( ( M + N ) e. NN0 -> ( # ` ( 1 ... ( M + N ) ) ) = ( M + N ) )
14 12 13 ax-mp 
 |-  ( # ` ( 1 ... ( M + N ) ) ) = ( M + N )
15 14 oveq1i 
 |-  ( ( # ` ( 1 ... ( M + N ) ) ) _C M ) = ( ( M + N ) _C M )
16 4 8 15 3eqtr2i 
 |-  ( # ` O ) = ( ( M + N ) _C M )