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 𝑀 ∈ ℕ
ballotth.n 𝑁 ∈ ℕ
ballotth.o 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
Assertion ballotlem1 ( ♯ ‘ 𝑂 ) = ( ( 𝑀 + 𝑁 ) C 𝑀 )

Proof

Step Hyp Ref Expression
1 ballotth.m 𝑀 ∈ ℕ
2 ballotth.n 𝑁 ∈ ℕ
3 ballotth.o 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 3 fveq2i ( ♯ ‘ 𝑂 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } )
5 fzfi ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
6 1 nnzi 𝑀 ∈ ℤ
7 hashbc ( ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ 𝑀 ∈ ℤ ) → ( ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) C 𝑀 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ) )
8 5 6 7 mp2an ( ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) C 𝑀 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } )
9 1 2 pm3.2i ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ )
10 nnaddcl ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
11 nnnn0 ( ( 𝑀 + 𝑁 ) ∈ ℕ → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
12 9 10 11 mp2b ( 𝑀 + 𝑁 ) ∈ ℕ0
13 hashfz1 ( ( 𝑀 + 𝑁 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) = ( 𝑀 + 𝑁 ) )
14 12 13 ax-mp ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) = ( 𝑀 + 𝑁 )
15 14 oveq1i ( ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) C 𝑀 ) = ( ( 𝑀 + 𝑁 ) C 𝑀 )
16 4 8 15 3eqtr2i ( ♯ ‘ 𝑂 ) = ( ( 𝑀 + 𝑁 ) C 𝑀 )