Metamath Proof Explorer


Theorem ballotlemimin

Description: ( IC ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016) (Revised by AV, 6-Oct-2020)

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
ballotth.i I = c O E sup k 1 M + N | F c k = 0 <
Assertion ballotlemimin C O E ¬ k 1 I C 1 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 ballotth.i I = c O E sup k 1 M + N | F c k = 0 <
9 elfzle2 k 1 I C 1 k I C 1
10 9 adantl C O E k 1 I C 1 k I C 1
11 elfzelz k 1 I C 1 k
12 1 2 3 4 5 6 7 8 ballotlemiex C O E I C 1 M + N F C I C = 0
13 12 simpld C O E I C 1 M + N
14 13 elfzelzd C O E I C
15 zltlem1 k I C k < I C k I C 1
16 11 14 15 syl2anr C O E k 1 I C 1 k < I C k I C 1
17 10 16 mpbird C O E k 1 I C 1 k < I C
18 17 adantr C O E k 1 I C 1 F C k = 0 k < I C
19 1zzd C O E 1
20 14 19 zsubcld C O E I C 1
21 20 zred C O E I C 1
22 nnaddcl M N M + N
23 1 2 22 mp2an M + N
24 23 a1i C O E M + N
25 24 nnred C O E M + N
26 elfzle2 I C 1 M + N I C M + N
27 13 26 syl C O E I C M + N
28 24 nnzd C O E M + N
29 zlem1lt I C M + N I C M + N I C 1 < M + N
30 14 28 29 syl2anc C O E I C M + N I C 1 < M + N
31 27 30 mpbid C O E I C 1 < M + N
32 21 25 31 ltled C O E I C 1 M + N
33 eluz I C 1 M + N M + N I C 1 I C 1 M + N
34 20 28 33 syl2anc C O E M + N I C 1 I C 1 M + N
35 32 34 mpbird C O E M + N I C 1
36 fzss2 M + N I C 1 1 I C 1 1 M + N
37 35 36 syl C O E 1 I C 1 1 M + N
38 37 sseld C O E k 1 I C 1 k 1 M + N
39 rabid k k 1 M + N | F C k = 0 k 1 M + N F C k = 0
40 1 2 3 4 5 6 7 8 ballotlemsup C O E z w k 1 M + N | F C k = 0 ¬ w < z w z < w y k 1 M + N | F C k = 0 y < w
41 ltso < Or
42 41 a1i z w k 1 M + N | F C k = 0 ¬ w < z w z < w y k 1 M + N | F C k = 0 y < w < Or
43 id z w k 1 M + N | F C k = 0 ¬ w < z w z < w y k 1 M + N | F C k = 0 y < w z w k 1 M + N | F C k = 0 ¬ w < z w z < w y k 1 M + N | F C k = 0 y < w
44 42 43 inflb z w k 1 M + N | F C k = 0 ¬ w < z w z < w y k 1 M + N | F C k = 0 y < w k k 1 M + N | F C k = 0 ¬ k < sup k 1 M + N | F C k = 0 <
45 40 44 syl C O E k k 1 M + N | F C k = 0 ¬ k < sup k 1 M + N | F C k = 0 <
46 1 2 3 4 5 6 7 8 ballotlemi C O E I C = sup k 1 M + N | F C k = 0 <
47 46 breq2d C O E k < I C k < sup k 1 M + N | F C k = 0 <
48 47 notbid C O E ¬ k < I C ¬ k < sup k 1 M + N | F C k = 0 <
49 45 48 sylibrd C O E k k 1 M + N | F C k = 0 ¬ k < I C
50 39 49 syl5bir C O E k 1 M + N F C k = 0 ¬ k < I C
51 38 50 syland C O E k 1 I C 1 F C k = 0 ¬ k < I C
52 51 imp C O E k 1 I C 1 F C k = 0 ¬ k < I C
53 biid k < I C k < I C
54 52 53 sylnib C O E k 1 I C 1 F C k = 0 ¬ k < I C
55 54 anassrs C O E k 1 I C 1 F C k = 0 ¬ k < I C
56 18 55 pm2.65da C O E k 1 I C 1 ¬ F C k = 0
57 56 nrexdv C O E ¬ k 1 I C 1 F C k = 0