Metamath Proof Explorer

Theorem ballotlemfmpn

Description: ( FC ) finishes counting at ( M - N ) . (Contributed by Thierry Arnoux, 25-Nov-2016)

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
Assertion ballotlemfmpn ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑀 + 𝑁 ) ) = ( 𝑀 − 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 id ⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ∈ 𝑂 )
7 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
8 1 2 7 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ
9 8 nnzi ⊢ ( 𝑀 + 𝑁 ) ∈ ℤ
10 9 a1i ⊢ ( 𝐶 ∈ 𝑂 → ( 𝑀 + 𝑁 ) ∈ ℤ )
11 1 2 3 4 5 6 10 ballotlemfval ⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∖ 𝐶 ) ) ) )
12 ssrab2 ⊢ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) )
13 3 12 eqsstri ⊢ 𝑂 ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) )
14 13 sseli ⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) )
15 14 elpwid ⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
16 sseqin2 ⊢ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ↔ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ 𝐶 ) = 𝐶 )
17 15 16 sylib ⊢ ( 𝐶 ∈ 𝑂 → ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ 𝐶 ) = 𝐶 )
18 17 fveq2d ⊢ ( 𝐶 ∈ 𝑂 → ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ 𝐶 ) ) = ( ♯ ‘ 𝐶 ) )
19 rabssab ⊢ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ⊆ { 𝑐 ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
20 19 sseli ⊢ ( 𝐶 ∈ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } → 𝐶 ∈ { 𝑐 ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } )
21 20 3 eleq2s ⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ∈ { 𝑐 ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } )
22 fveqeq2 ⊢ ( 𝑏 = 𝐶 → ( ( ♯ ‘ 𝑏 ) = 𝑀 ↔ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
23 fveqeq2 ⊢ ( 𝑐 = 𝑏 → ( ( ♯ ‘ 𝑐 ) = 𝑀 ↔ ( ♯ ‘ 𝑏 ) = 𝑀 ) )
24 23 cbvabv ⊢ { 𝑐 ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } = { 𝑏 ∣ ( ♯ ‘ 𝑏 ) = 𝑀 }
25 22 24 elab2g ⊢ ( 𝐶 ∈ 𝑂 → ( 𝐶 ∈ { 𝑐 ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ↔ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
26 21 25 mpbid ⊢ ( 𝐶 ∈ 𝑂 → ( ♯ ‘ 𝐶 ) = 𝑀 )
27 18 26 eqtrd ⊢ ( 𝐶 ∈ 𝑂 → ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ 𝐶 ) ) = 𝑀 )
28 fzfi ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
29 hashssdif ⊢ ( ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∖ 𝐶 ) ) = ( ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) − ( ♯ ‘ 𝐶 ) ) )
30 28 15 29 sylancr ⊢ ( 𝐶 ∈ 𝑂 → ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∖ 𝐶 ) ) = ( ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) − ( ♯ ‘ 𝐶 ) ) )
31 8 nnnn0i ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ0
32 hashfz1 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) = ( 𝑀 + 𝑁 ) )
33 31 32 mp1i ⊢ ( 𝐶 ∈ 𝑂 → ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) = ( 𝑀 + 𝑁 ) )
34 33 26 oveq12d ⊢ ( 𝐶 ∈ 𝑂 → ( ( ♯ ‘ ( 1 ... ( 𝑀 + 𝑁 ) ) ) − ( ♯ ‘ 𝐶 ) ) = ( ( 𝑀 + 𝑁 ) − 𝑀 ) )
35 1 nncni ⊢ 𝑀 ∈ ℂ
36 2 nncni ⊢ 𝑁 ∈ ℂ
37 pncan2 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
38 35 36 37 mp2an ⊢ ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁
39 38 a1i ⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
40 30 34 39 3eqtrd ⊢ ( 𝐶 ∈ 𝑂 → ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∖ 𝐶 ) ) = 𝑁 )
41 27 40 oveq12d ⊢ ( 𝐶 ∈ 𝑂 → ( ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∖ 𝐶 ) ) ) = ( 𝑀 − 𝑁 ) )
42 11 41 eqtrd ⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑀 + 𝑁 ) ) = ( 𝑀 − 𝑁 ) )