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 𝑀 )