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 ⟼ x O
ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
ballotth.mgtn ⊢ N < M
ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 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 = 0 y < 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 ⟼ x O
5 ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
6 ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
7 ballotth.mgtn ⊢ N < M
8 ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 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 + N F ⁡ C ⁡ k = 0
15 rabn0 ⊢ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ≠ ∅ ↔ ∃ k ∈ 1 … M + N F ⁡ 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 = 0 y < 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 = 0 y < w → z ∈ ℝ ∧ ∀ w ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ¬ w < z ∧ ∀ w ∈ ℝ z < w → ∃ y ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 y < 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 = 0 y < w → ∃ z ∈ ℝ ∀ w ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 ¬ w < z ∧ ∀ w ∈ ℝ z < w → ∃ y ∈ k ∈ 1 … M + N | F ⁡ C ⁡ k = 0 y < 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 = 0 y < w