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 ∈ ℕ
ballotth.n ⊢ N ∈ ℕ
ballotth.o ⊢ O = c ∈ 𝒫 1 … M + N | c = M
Assertion ballotlem1 ⊢ O = ( M + N M)

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ M ∈ ℕ
2 ballotth.n ⊢ N ∈ ℕ
3 ballotth.o ⊢ O = c ∈ 𝒫 1 … M + N | c = M
4 3 fveq2i ⊢ O = c ∈ 𝒫 1 … M + N | c = M
5 fzfi ⊢ 1 … M + N ∈ Fin
6 1 nnzi ⊢ M ∈ ℤ
7 hashbc ⊢ 1 … M + N ∈ Fin ∧ M ∈ ℤ → ( 1 … M + N M) = c ∈ 𝒫 1 … M + N | c = M
8 5 6 7 mp2an ⊢ ( 1 … M + N M) = c ∈ 𝒫 1 … M + N | c = M
9 1 2 pm3.2i ⊢ M ∈ ℕ ∧ N ∈ ℕ
10 nnaddcl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M + N ∈ ℕ
11 nnnn0 ⊢ M + N ∈ ℕ → M + N ∈ ℕ 0
12 9 10 11 mp2b ⊢ M + N ∈ ℕ 0
13 hashfz1 ⊢ M + N ∈ ℕ 0 → 1 … M + N = M + N
14 12 13 ax-mp ⊢ 1 … M + N = M + N
15 14 oveq1i ⊢ ( 1 … M + N M) = ( M + N M)
16 4 8 15 3eqtr2i ⊢ O = ( M + N M)