Metamath Proof Explorer

Theorem ballotlemimin

Description: ( IC ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016) (Revised by AV, 6-Oct-2020)

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 ballotlemimin ⊢C∈O∖E→¬∃k∈1…I⁡C−1F⁡C⁡k=0

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 elfzle2 ⊢k∈1…I⁡C−1→k≤I⁡C−1
10 9 adantl ⊢C∈O∖E∧k∈1…I⁡C−1→k≤I⁡C−1
11 elfzelz ⊢k∈1…I⁡C−1→k∈ℤ
12 1 2 3 4 5 6 7 8 ballotlemiex ⊢C∈O∖E→I⁡C∈1…M+N∧F⁡C⁡I⁡C=0
13 12 simpld ⊢C∈O∖E→I⁡C∈1…M+N
14 13 elfzelzd ⊢C∈O∖E→I⁡C∈ℤ
15 zltlem1 ⊢k∈ℤ∧I⁡C∈ℤ→k<I⁡C↔k≤I⁡C−1
16 11 14 15 syl2anr ⊢C∈O∖E∧k∈1…I⁡C−1→k<I⁡C↔k≤I⁡C−1
17 10 16 mpbird ⊢C∈O∖E∧k∈1…I⁡C−1→k<I⁡C
18 17 adantr ⊢C∈O∖E∧k∈1…I⁡C−1∧F⁡C⁡k=0→k<I⁡C
19 1zzd ⊢C∈O∖E→1∈ℤ
20 14 19 zsubcld ⊢C∈O∖E→I⁡C−1∈ℤ
21 20 zred ⊢C∈O∖E→I⁡C−1∈ℝ
22 nnaddcl ⊢M∈ℕ∧N∈ℕ→M+N∈ℕ
23 1 2 22 mp2an ⊢M+N∈ℕ
24 23 a1i ⊢C∈O∖E→M+N∈ℕ
25 24 nnred ⊢C∈O∖E→M+N∈ℝ
26 elfzle2 ⊢I⁡C∈1…M+N→I⁡C≤M+N
27 13 26 syl ⊢C∈O∖E→I⁡C≤M+N
28 24 nnzd ⊢C∈O∖E→M+N∈ℤ
29 zlem1lt ⊢I⁡C∈ℤ∧M+N∈ℤ→I⁡C≤M+N↔I⁡C−1<M+N
30 14 28 29 syl2anc ⊢C∈O∖E→I⁡C≤M+N↔I⁡C−1<M+N
31 27 30 mpbid ⊢C∈O∖E→I⁡C−1<M+N
32 21 25 31 ltled ⊢C∈O∖E→I⁡C−1≤M+N
33 eluz ⊢I⁡C−1∈ℤ∧M+N∈ℤ→M+N∈ℤ≥I⁡C−1↔I⁡C−1≤M+N
34 20 28 33 syl2anc ⊢C∈O∖E→M+N∈ℤ≥I⁡C−1↔I⁡C−1≤M+N
35 32 34 mpbird ⊢C∈O∖E→M+N∈ℤ≥I⁡C−1
36 fzss2 ⊢M+N∈ℤ≥I⁡C−1→1…I⁡C−1⊆1…M+N
37 35 36 syl ⊢C∈O∖E→1…I⁡C−1⊆1…M+N
38 37 sseld ⊢C∈O∖E→k∈1…I⁡C−1→k∈1…M+N
39 rabid ⊢k∈k∈1…M+N|F⁡C⁡k=0↔k∈1…M+N∧F⁡C⁡k=0
40 1 2 3 4 5 6 7 8 ballotlemsup ⊢C∈O∖E→∃z∈ℝ∀w∈k∈1…M+N|F⁡C⁡k=0¬w<z∧∀w∈ℝz<w→∃y∈k∈1…M+N|F⁡C⁡k=0y<w
41 ltso ⊢<Orℝ
42 41 a1i ⊢∃z∈ℝ∀w∈k∈1…M+N|F⁡C⁡k=0¬w<z∧∀w∈ℝz<w→∃y∈k∈1…M+N|F⁡C⁡k=0y<w→<Orℝ
43 id ⊢∃z∈ℝ∀w∈k∈1…M+N|F⁡C⁡k=0¬w<z∧∀w∈ℝz<w→∃y∈k∈1…M+N|F⁡C⁡k=0y<w→∃z∈ℝ∀w∈k∈1…M+N|F⁡C⁡k=0¬w<z∧∀w∈ℝz<w→∃y∈k∈1…M+N|F⁡C⁡k=0y<w
44 42 43 inflb ⊢∃z∈ℝ∀w∈k∈1…M+N|F⁡C⁡k=0¬w<z∧∀w∈ℝz<w→∃y∈k∈1…M+N|F⁡C⁡k=0y<w→k∈k∈1…M+N|F⁡C⁡k=0→¬k<supk∈1…M+N|F⁡C⁡k=0ℝ<
45 40 44 syl ⊢C∈O∖E→k∈k∈1…M+N|F⁡C⁡k=0→¬k<supk∈1…M+N|F⁡C⁡k=0ℝ<
46 1 2 3 4 5 6 7 8 ballotlemi ⊢C∈O∖E→I⁡C=supk∈1…M+N|F⁡C⁡k=0ℝ<
47 46 breq2d ⊢C∈O∖E→k<I⁡C↔k<supk∈1…M+N|F⁡C⁡k=0ℝ<
48 47 notbid ⊢C∈O∖E→¬k<I⁡C↔¬k<supk∈1…M+N|F⁡C⁡k=0ℝ<
49 45 48 sylibrd ⊢C∈O∖E→k∈k∈1…M+N|F⁡C⁡k=0→¬k<I⁡C
50 39 49 biimtrrid ⊢C∈O∖E→k∈1…M+N∧F⁡C⁡k=0→¬k<I⁡C
51 38 50 syland ⊢C∈O∖E→k∈1…I⁡C−1∧F⁡C⁡k=0→¬k<I⁡C
52 51 imp ⊢C∈O∖E∧k∈1…I⁡C−1∧F⁡C⁡k=0→¬k<I⁡C
53 biid ⊢k<I⁡C↔k<I⁡C
54 52 53 sylnib ⊢C∈O∖E∧k∈1…I⁡C−1∧F⁡C⁡k=0→¬k<I⁡C
55 54 anassrs ⊢C∈O∖E∧k∈1…I⁡C−1∧F⁡C⁡k=0→¬k<I⁡C
56 18 55 pm2.65da ⊢C∈O∖E∧k∈1…I⁡C−1→¬F⁡C⁡k=0
57 56 nrexdv ⊢C∈O∖E→¬∃k∈1…I⁡C−1F⁡C⁡k=0