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 | |
|
ballotth.n | |
||
ballotth.o | |
||
ballotth.p | |
||
ballotth.f | |
||
ballotth.e | |
||
ballotth.mgtn | |
||
ballotth.i | |
||
ballotth.s | |
||
ballotth.r | |
||
Assertion | ballotlem1ri | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ballotth.m | |
|
2 | ballotth.n | |
|
3 | ballotth.o | |
|
4 | ballotth.p | |
|
5 | ballotth.f | |
|
6 | ballotth.e | |
|
7 | ballotth.mgtn | |
|
8 | ballotth.i | |
|
9 | ballotth.s | |
|
10 | ballotth.r | |
|
11 | nnaddcl | |
|
12 | 1 2 11 | mp2an | |
13 | nnuz | |
|
14 | 12 13 | eleqtri | |
15 | eluzfz1 | |
|
16 | 14 15 | mp1i | |
17 | 1 2 3 4 5 6 7 8 | ballotlemiex | |
18 | 17 | simpld | |
19 | elfzle1 | |
|
20 | 18 19 | syl | |
21 | 1 2 3 4 5 6 7 8 9 10 | ballotlemrv1 | |
22 | 16 20 21 | mpd3an23 | |
23 | 18 | elfzelzd | |
24 | 23 | zcnd | |
25 | 1cnd | |
|
26 | 24 25 | pncand | |
27 | 26 | eleq1d | |
28 | 22 27 | bitrd | |