Metamath Proof Explorer


Theorem ballotlemi1

Description: The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-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 ballotlemi1 C O E ¬ 1 C I C 1

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 0re 0
10 1re 1
11 9 10 resubcli 0 1
12 0lt1 0 < 1
13 ltsub23 0 1 0 0 1 < 0 0 0 < 1
14 9 10 9 13 mp3an 0 1 < 0 0 0 < 1
15 0m0e0 0 0 = 0
16 15 breq1i 0 0 < 1 0 < 1
17 14 16 bitr2i 0 < 1 0 1 < 0
18 12 17 mpbi 0 1 < 0
19 11 18 gtneii 0 0 1
20 19 nesymi ¬ 0 1 = 0
21 eldifi C O E C O
22 1nn 1
23 22 a1i C O E 1
24 1 2 3 4 5 21 23 ballotlemfp1 C O E ¬ 1 C F C 1 = F C 1 1 1 1 C F C 1 = F C 1 1 + 1
25 24 simpld C O E ¬ 1 C F C 1 = F C 1 1 1
26 25 imp C O E ¬ 1 C F C 1 = F C 1 1 1
27 1m1e0 1 1 = 0
28 27 fveq2i F C 1 1 = F C 0
29 28 oveq1i F C 1 1 1 = F C 0 1
30 29 a1i C O E ¬ 1 C F C 1 1 1 = F C 0 1
31 1 2 3 4 5 ballotlemfval0 C O F C 0 = 0
32 21 31 syl C O E F C 0 = 0
33 32 adantr C O E ¬ 1 C F C 0 = 0
34 33 oveq1d C O E ¬ 1 C F C 0 1 = 0 1
35 26 30 34 3eqtrrd C O E ¬ 1 C 0 1 = F C 1
36 35 eqeq1d C O E ¬ 1 C 0 1 = 0 F C 1 = 0
37 20 36 mtbii C O E ¬ 1 C ¬ F C 1 = 0
38 1 2 3 4 5 6 7 8 ballotlemiex C O E I C 1 M + N F C I C = 0
39 38 simprd C O E F C I C = 0
40 39 ad2antrr C O E ¬ 1 C I C = 1 F C I C = 0
41 fveqeq2 I C = 1 F C I C = 0 F C 1 = 0
42 41 adantl C O E ¬ 1 C I C = 1 F C I C = 0 F C 1 = 0
43 40 42 mpbid C O E ¬ 1 C I C = 1 F C 1 = 0
44 37 43 mtand C O E ¬ 1 C ¬ I C = 1
45 44 neqned C O E ¬ 1 C I C 1