Metamath Proof Explorer


Theorem ballotlemsi

Description: The image by S of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-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
Assertion ballotlemsi COESCIC=1

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 1 2 3 4 5 6 7 8 ballotlemiex COEIC1M+NFCIC=0
11 10 simpld COEIC1M+N
12 1 2 3 4 5 6 7 8 9 ballotlemsv COEIC1M+NSCIC=ifICICIC+1-ICIC
13 11 12 mpdan COESCIC=ifICICIC+1-ICIC
14 elfzelz IC1M+NIC
15 14 zred IC1M+NIC
16 11 15 syl COEIC
17 16 leidd COEICIC
18 17 iftrued COEifICICIC+1-ICIC=IC+1-IC
19 16 recnd COEIC
20 1cnd COE1
21 19 20 pncan2d COEIC+1-IC=1
22 13 18 21 3eqtrd COESCIC=1