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 x O
ballotth.f F = c O i 1 i c 1 i c
ballotth.e E = c O | i 1 M + N 0 < F c i
ballotth.mgtn N < M
Assertion ballotlem5 C O E k 1 M + N F 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 x O
5 ballotth.f F = c O i 1 i c 1 i c
6 ballotth.e E = c O | i 1 M + N 0 < 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 + N F C i 0
13 12 simprbi C O E i 1 M + N F 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 + N F C k = 0