Metamath Proof Explorer


Theorem ballotlem1c

Description: If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017)

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 ballotlem1c C O E 1 C ¬ I C C

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 eldifi C O E C O
10 9 ad2antrr C O E 1 C I C C C O
11 1 2 3 4 5 6 7 8 ballotlemiex C O E I C 1 M + N F C I C = 0
12 11 simpld C O E I C 1 M + N
13 elfznn I C 1 M + N I C
14 12 13 syl C O E I C
15 14 adantr C O E 1 C I C
16 1 2 3 4 5 6 7 8 ballotlemii C O E 1 C I C 1
17 eluz2b3 I C 2 I C I C 1
18 15 16 17 sylanbrc C O E 1 C I C 2
19 uz2m1nn I C 2 I C 1
20 18 19 syl C O E 1 C I C 1
21 20 adantr C O E 1 C I C C I C 1
22 elnnuz I C 1 I C 1 1
23 22 biimpi I C 1 I C 1 1
24 eluzfz1 I C 1 1 1 1 I C 1
25 20 23 24 3syl C O E 1 C 1 1 I C 1
26 25 adantr C O E 1 C I C C 1 1 I C 1
27 0le1 0 1
28 1e0p1 1 = 0 + 1
29 27 28 breqtri 0 0 + 1
30 1nn 1
31 30 a1i C O E 1
32 1 2 3 4 5 9 31 ballotlemfp1 C O E ¬ 1 C F C 1 = F C 1 1 1 1 C F C 1 = F C 1 1 + 1
33 32 simprd C O E 1 C F C 1 = F C 1 1 + 1
34 33 imp C O E 1 C F C 1 = F C 1 1 + 1
35 1m1e0 1 1 = 0
36 35 fveq2i F C 1 1 = F C 0
37 36 oveq1i F C 1 1 + 1 = F C 0 + 1
38 37 a1i C O E 1 C F C 1 1 + 1 = F C 0 + 1
39 1 2 3 4 5 ballotlemfval0 C O F C 0 = 0
40 9 39 syl C O E F C 0 = 0
41 40 adantr C O E 1 C F C 0 = 0
42 41 oveq1d C O E 1 C F C 0 + 1 = 0 + 1
43 34 38 42 3eqtrrd C O E 1 C 0 + 1 = F C 1
44 29 43 breqtrid C O E 1 C 0 F C 1
45 44 adantr C O E 1 C I C C 0 F C 1
46 fveq2 i = 1 F C i = F C 1
47 46 breq2d i = 1 0 F C i 0 F C 1
48 47 rspcev 1 1 I C 1 0 F C 1 i 1 I C 1 0 F C i
49 26 45 48 syl2anc C O E 1 C I C C i 1 I C 1 0 F C i
50 df-neg 1 = 0 1
51 1 2 3 4 5 9 14 ballotlemfp1 C O E ¬ I C C F C I C = F C I C 1 1 I C C F C I C = F C I C 1 + 1
52 51 simprd C O E I C C F C I C = F C I C 1 + 1
53 52 imp C O E I C C F C I C = F C I C 1 + 1
54 11 simprd C O E F C I C = 0
55 54 adantr C O E I C C F C I C = 0
56 53 55 eqtr3d C O E I C C F C I C 1 + 1 = 0
57 0cnd C O E I C C 0
58 1cnd C O E I C C 1
59 9 adantr C O E I C C C O
60 14 nnzd C O E I C
61 60 adantr C O E I C C I C
62 1zzd C O E I C C 1
63 61 62 zsubcld C O E I C C I C 1
64 1 2 3 4 5 59 63 ballotlemfelz C O E I C C F C I C 1
65 64 zcnd C O E I C C F C I C 1
66 57 58 65 subadd2d C O E I C C 0 1 = F C I C 1 F C I C 1 + 1 = 0
67 56 66 mpbird C O E I C C 0 1 = F C I C 1
68 50 67 syl5eq C O E I C C 1 = F C I C 1
69 neg1lt0 1 < 0
70 68 69 eqbrtrrdi C O E I C C F C I C 1 < 0
71 70 adantlr C O E 1 C I C C F C I C 1 < 0
72 1 2 3 4 5 10 21 49 71 ballotlemfcc C O E 1 C I C C k 1 I C 1 F C k = 0
73 1 2 3 4 5 6 7 8 ballotlemimin C O E ¬ k 1 I C 1 F C k = 0
74 73 ad2antrr C O E 1 C I C C ¬ k 1 I C 1 F C k = 0
75 72 74 pm2.65da C O E 1 C ¬ I C C