Metamath Proof Explorer

Theorem ballotlem8

Description: There are as many countings with ties starting with a ballot for A as there are starting with a ballot for B . (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Hypotheses ballotth.m ⊢M∈ℕ
ballotth.n ⊢N∈ℕ
ballotth.o ⊢O=c∈𝒫1…M+N|c=M
ballotth.p ⊢P=x∈𝒫O⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
ballotth.r ⊢R=c∈O∖E⟼S⁡cc
Assertion ballotlem8 ⊢c∈O∖E|1∈c=c∈O∖E|¬1∈c

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢M∈ℕ
2 ballotth.n ⊢N∈ℕ
3 ballotth.o ⊢O=c∈𝒫1…M+N|c=M
4 ballotth.p ⊢P=x∈𝒫O⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
9 ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
10 ballotth.r ⊢R=c∈O∖E⟼S⁡cc
11 1 2 3 4 5 6 7 8 9 10 ballotlem7 ⊢R↾c∈O∖E|1∈c:c∈O∖E|1∈c⟶1-1 ontoc∈O∖E|¬1∈c
12 1 2 3 ballotlemoex ⊢O∈V
13 difexg ⊢O∈V→O∖E∈V
14 12 13 ax-mp ⊢O∖E∈V
15 14 rabex ⊢c∈O∖E|1∈c∈V
16 15 f1oen ⊢R↾c∈O∖E|1∈c:c∈O∖E|1∈c⟶1-1 ontoc∈O∖E|¬1∈c→c∈O∖E|1∈c≈c∈O∖E|¬1∈c
17 hasheni ⊢c∈O∖E|1∈c≈c∈O∖E|¬1∈c→c∈O∖E|1∈c=c∈O∖E|¬1∈c
18 11 16 17 mp2b ⊢c∈O∖E|1∈c=c∈O∖E|¬1∈c