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⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈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⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈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−10≤F⁡C⁡i
49 26 45 48 syl2anc ⊢C∈O∖E∧1∈C∧I⁡C∈C→∃i∈1…I⁡C−10≤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 eqtrid ⊢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−1F⁡C⁡k=0
73 1 2 3 4 5 6 7 8 ballotlemimin ⊢C∈O∖E→¬∃k∈1…I⁡C−1F⁡C⁡k=0
74 73 ad2antrr ⊢C∈O∖E∧1∈C∧I⁡C∈C→¬∃k∈1…I⁡C−1F⁡C⁡k=0
75 72 74 pm2.65da ⊢C∈O∖E∧1∈C→¬I⁡C∈C