Metamath Proof Explorer


Theorem ballotlem1ri

Description: When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-Apr-2017)

Ref Expression
Hypotheses ballotth.m M
ballotth.n N
ballotth.o O=c𝒫1M+N|c=M
ballotth.p P=x𝒫OxO
ballotth.f F=cOi1ic1ic
ballotth.e E=cO|i1M+N0<Fci
ballotth.mgtn N<M
ballotth.i I=cOEsupk1M+N|Fck=0<
ballotth.s S=cOEi1M+NifiIcIc+1-ii
ballotth.r R=cOEScc
Assertion ballotlem1ri COE1RCICC

Proof

Step Hyp Ref Expression
1 ballotth.m M
2 ballotth.n N
3 ballotth.o O=c𝒫1M+N|c=M
4 ballotth.p P=x𝒫OxO
5 ballotth.f F=cOi1ic1ic
6 ballotth.e E=cO|i1M+N0<Fci
7 ballotth.mgtn N<M
8 ballotth.i I=cOEsupk1M+N|Fck=0<
9 ballotth.s S=cOEi1M+NifiIcIc+1-ii
10 ballotth.r R=cOEScc
11 nnaddcl MNM+N
12 1 2 11 mp2an M+N
13 nnuz =1
14 12 13 eleqtri M+N1
15 eluzfz1 M+N111M+N
16 14 15 mp1i COE11M+N
17 1 2 3 4 5 6 7 8 ballotlemiex COEIC1M+NFCIC=0
18 17 simpld COEIC1M+N
19 elfzle1 IC1M+N1IC
20 18 19 syl COE1IC
21 1 2 3 4 5 6 7 8 9 10 ballotlemrv1 COE11M+N1IC1RCIC+1-1C
22 16 20 21 mpd3an23 COE1RCIC+1-1C
23 18 elfzelzd COEIC
24 23 zcnd COEIC
25 1cnd COE1
26 24 25 pncand COEIC+1-1=IC
27 26 eleq1d COEIC+1-1CICC
28 22 27 bitrd COE1RCICC