Metamath Proof Explorer

Theorem ballotlemii

Description: The first tie cannot be reached at the first pick. (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 ballotlemii ⊢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 1e0p1 ⊢1=0+1
10 ax-1ne0 ⊢1≠0
11 9 10 eqnetrri ⊢0+1≠0
12 11 neii ⊢¬0+1=0
13 eldifi ⊢C∈O∖E→C∈O
14 1nn ⊢1∈ℕ
15 14 a1i ⊢C∈O∖E→1∈ℕ
16 1 2 3 4 5 13 15 ballotlemfp1 ⊢C∈O∖E→¬1∈C→F⁡C⁡1=F⁡C⁡1−1−1∧1∈C→F⁡C⁡1=F⁡C⁡1−1+1
17 16 simprd ⊢C∈O∖E→1∈C→F⁡C⁡1=F⁡C⁡1−1+1
18 17 imp ⊢C∈O∖E∧1∈C→F⁡C⁡1=F⁡C⁡1−1+1
19 1m1e0 ⊢1−1=0
20 19 fveq2i ⊢F⁡C⁡1−1=F⁡C⁡0
21 20 oveq1i ⊢F⁡C⁡1−1+1=F⁡C⁡0+1
22 21 a1i ⊢C∈O∖E∧1∈C→F⁡C⁡1−1+1=F⁡C⁡0+1
23 1 2 3 4 5 ballotlemfval0 ⊢C∈O→F⁡C⁡0=0
24 13 23 syl ⊢C∈O∖E→F⁡C⁡0=0
25 24 adantr ⊢C∈O∖E∧1∈C→F⁡C⁡0=0
26 25 oveq1d ⊢C∈O∖E∧1∈C→F⁡C⁡0+1=0+1
27 18 22 26 3eqtrrd ⊢C∈O∖E∧1∈C→0+1=F⁡C⁡1
28 27 eqeq1d ⊢C∈O∖E∧1∈C→0+1=0↔F⁡C⁡1=0
29 12 28 mtbii ⊢C∈O∖E∧1∈C→¬F⁡C⁡1=0
30 1 2 3 4 5 6 7 8 ballotlemiex ⊢C∈O∖E→I⁡C∈1…M+N∧F⁡C⁡I⁡C=0
31 30 simprd ⊢C∈O∖E→F⁡C⁡I⁡C=0
32 31 ad2antrr ⊢C∈O∖E∧1∈C∧I⁡C=1→F⁡C⁡I⁡C=0
33 fveqeq2 ⊢I⁡C=1→F⁡C⁡I⁡C=0↔F⁡C⁡1=0
34 33 adantl ⊢C∈O∖E∧1∈C∧I⁡C=1→F⁡C⁡I⁡C=0↔F⁡C⁡1=0
35 32 34 mpbid ⊢C∈O∖E∧1∈C∧I⁡C=1→F⁡C⁡1=0
36 29 35 mtand ⊢C∈O∖E∧1∈C→¬I⁡C=1
37 36 neqned ⊢C∈O∖E∧1∈C→I⁡C≠1