Metamath Proof Explorer

Theorem ballotlem5

Description: If A is not ahead throughout, there is a k where votes are tied. (Contributed by Thierry Arnoux, 1-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
Assertion ballotlem5 ⊢C∈O∖E→∃k∈1…M+NF⁡C⁡k=0

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 eldifi ⊢C∈O∖E→C∈O
9 1 a1i ⊢C∈O∖E→M∈ℕ
10 2 a1i ⊢C∈O∖E→N∈ℕ
11 9 10 nnaddcld ⊢C∈O∖E→M+N∈ℕ
12 1 2 3 4 5 6 ballotlemodife ⊢C∈O∖E↔C∈O∧∃i∈1…M+NF⁡C⁡i≤0
13 12 simprbi ⊢C∈O∖E→∃i∈1…M+NF⁡C⁡i≤0
14 2 nnrei ⊢N∈ℝ
15 1 nnrei ⊢M∈ℝ
16 14 15 posdifi ⊢N<M↔0<M−N
17 7 16 mpbi ⊢0<M−N
18 1 2 3 4 5 ballotlemfmpn ⊢C∈O→F⁡C⁡M+N=M−N
19 8 18 syl ⊢C∈O∖E→F⁡C⁡M+N=M−N
20 17 19 breqtrrid ⊢C∈O∖E→0<F⁡C⁡M+N
21 1 2 3 4 5 8 11 13 20 ballotlemfc0 ⊢C∈O∖E→∃k∈1…M+NF⁡C⁡k=0