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⟼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 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⟼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 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