Metamath Proof Explorer


Theorem ballotlem4

Description: If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016)

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
Assertion ballotlem4 C O ¬ 1 C ¬ C E

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 nnaddcl M N M + N
8 1 2 7 mp2an M + N
9 elnnuz M + N M + N 1
10 8 9 mpbi M + N 1
11 eluzfz1 M + N 1 1 1 M + N
12 10 11 ax-mp 1 1 M + N
13 0le1 0 1
14 0re 0
15 1re 1
16 14 15 lenlti 0 1 ¬ 1 < 0
17 13 16 mpbi ¬ 1 < 0
18 ltsub13 0 0 1 0 < 0 1 1 < 0 0
19 14 14 15 18 mp3an 0 < 0 1 1 < 0 0
20 0m0e0 0 0 = 0
21 20 breq2i 1 < 0 0 1 < 0
22 19 21 bitri 0 < 0 1 1 < 0
23 17 22 mtbir ¬ 0 < 0 1
24 1m1e0 1 1 = 0
25 24 fveq2i F C 1 1 = F C 0
26 1 2 3 4 5 ballotlemfval0 C O F C 0 = 0
27 25 26 syl5eq C O F C 1 1 = 0
28 27 oveq1d C O F C 1 1 1 = 0 1
29 28 breq2d C O 0 < F C 1 1 1 0 < 0 1
30 23 29 mtbiri C O ¬ 0 < F C 1 1 1
31 30 adantr C O ¬ 1 C ¬ 0 < F C 1 1 1
32 simpl C O 1 1 M + N C O
33 1nn 1
34 33 a1i C O 1 1 M + N 1
35 1 2 3 4 5 32 34 ballotlemfp1 C O 1 1 M + N ¬ 1 C F C 1 = F C 1 1 1 1 C F C 1 = F C 1 1 + 1
36 35 simpld C O 1 1 M + N ¬ 1 C F C 1 = F C 1 1 1
37 12 36 mpan2 C O ¬ 1 C F C 1 = F C 1 1 1
38 37 imp C O ¬ 1 C F C 1 = F C 1 1 1
39 38 breq2d C O ¬ 1 C 0 < F C 1 0 < F C 1 1 1
40 31 39 mtbird C O ¬ 1 C ¬ 0 < F C 1
41 fveq2 i = 1 F C i = F C 1
42 41 breq2d i = 1 0 < F C i 0 < F C 1
43 42 notbid i = 1 ¬ 0 < F C i ¬ 0 < F C 1
44 43 rspcev 1 1 M + N ¬ 0 < F C 1 i 1 M + N ¬ 0 < F C i
45 12 40 44 sylancr C O ¬ 1 C i 1 M + N ¬ 0 < F C i
46 rexnal i 1 M + N ¬ 0 < F C i ¬ i 1 M + N 0 < F C i
47 45 46 sylib C O ¬ 1 C ¬ i 1 M + N 0 < F C i
48 1 2 3 4 5 6 ballotleme C E C O i 1 M + N 0 < F C i
49 48 simprbi C E i 1 M + N 0 < F C i
50 47 49 nsyl C O ¬ 1 C ¬ C E
51 50 ex C O ¬ 1 C ¬ C E