Metamath Proof Explorer

Theorem ballotlemsup

Description: The set of zeroes of F satisfies the conditions to have a supremum. (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 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

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 fzfi ⊢1…M+N∈Fin
10 ssrab2 ⊢k∈1…M+N|F⁡C⁡k=0⊆1…M+N
11 ssfi ⊢1…M+N∈Fin∧k∈1…M+N|F⁡C⁡k=0⊆1…M+N→k∈1…M+N|F⁡C⁡k=0∈Fin
12 9 10 11 mp2an ⊢k∈1…M+N|F⁡C⁡k=0∈Fin
13 12 a1i ⊢C∈O∖E→k∈1…M+N|F⁡C⁡k=0∈Fin
14 1 2 3 4 5 6 7 ballotlem5 ⊢C∈O∖E→∃k∈1…M+NF⁡C⁡k=0
15 rabn0 ⊢k∈1…M+N|F⁡C⁡k=0≠∅↔∃k∈1…M+NF⁡C⁡k=0
16 14 15 sylibr ⊢C∈O∖E→k∈1…M+N|F⁡C⁡k=0≠∅
17 fz1ssnn ⊢1…M+N⊆ℕ
18 nnssre ⊢ℕ⊆ℝ
19 17 18 sstri ⊢1…M+N⊆ℝ
20 10 19 sstri ⊢k∈1…M+N|F⁡C⁡k=0⊆ℝ
21 20 a1i ⊢C∈O∖E→k∈1…M+N|F⁡C⁡k=0⊆ℝ
22 13 16 21 3jca ⊢C∈O∖E→k∈1…M+N|F⁡C⁡k=0∈Fin∧k∈1…M+N|F⁡C⁡k=0≠∅∧k∈1…M+N|F⁡C⁡k=0⊆ℝ
23 ltso ⊢<Orℝ
24 22 23 jctil ⊢C∈O∖E→<Orℝ∧k∈1…M+N|F⁡C⁡k=0∈Fin∧k∈1…M+N|F⁡C⁡k=0≠∅∧k∈1…M+N|F⁡C⁡k=0⊆ℝ
25 fiinf2g ⊢<Orℝ∧k∈1…M+N|F⁡C⁡k=0∈Fin∧k∈1…M+N|F⁡C⁡k=0≠∅∧k∈1…M+N|F⁡C⁡k=0⊆ℝ→∃z∈k∈1…M+N|F⁡C⁡k=0∀w∈k∈1…M+N|F⁡C⁡k=0¬w<z∧∀w∈ℝz<w→∃y∈k∈1…M+N|F⁡C⁡k=0y<w
26 20 sseli ⊢z∈k∈1…M+N|F⁡C⁡k=0→z∈ℝ
27 26 anim1i ⊢z∈k∈1…M+N|F⁡C⁡k=0∧∀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
28 27 reximi2 ⊢∃z∈k∈1…M+N|F⁡C⁡k=0∀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
29 24 25 28 3syl ⊢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