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 𝑀 ∈ ℕ
ballotth.n 𝑁 ∈ ℕ
ballotth.o 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f 𝐹 = ( 𝑐𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e 𝐸 = { 𝑐𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹𝑐 ) ‘ 𝑖 ) }
ballotth.mgtn 𝑁 < 𝑀
ballotth.i 𝐼 = ( 𝑐 ∈ ( 𝑂𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
Assertion ballotlemsup ( 𝐶 ∈ ( 𝑂𝐸 ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m 𝑀 ∈ ℕ
2 ballotth.n 𝑁 ∈ ℕ
3 ballotth.o 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f 𝐹 = ( 𝑐𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotth.e 𝐸 = { 𝑐𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹𝑐 ) ‘ 𝑖 ) }
7 ballotth.mgtn 𝑁 < 𝑀
8 ballotth.i 𝐼 = ( 𝑐 ∈ ( 𝑂𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 fzfi ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
10 ssrab2 { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ( 1 ... ( 𝑀 + 𝑁 ) )
11 ssfi ( ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin )
12 9 10 11 mp2an { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin
13 12 a1i ( 𝐶 ∈ ( 𝑂𝐸 ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin )
14 1 2 3 4 5 6 7 ballotlem5 ( 𝐶 ∈ ( 𝑂𝐸 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 )
15 rabn0 ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ ↔ ∃ 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 )
16 14 15 sylibr ( 𝐶 ∈ ( 𝑂𝐸 ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ )
17 fz1ssnn ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ℕ
18 nnssre ℕ ⊆ ℝ
19 17 18 sstri ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ℝ
20 10 19 sstri { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ
21 20 a1i ( 𝐶 ∈ ( 𝑂𝐸 ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ )
22 13 16 21 3jca ( 𝐶 ∈ ( 𝑂𝐸 ) → ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ ) )
23 ltso < Or ℝ
24 22 23 jctil ( 𝐶 ∈ ( 𝑂𝐸 ) → ( < Or ℝ ∧ ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ ) ) )
25 fiinf2g ( ( < Or ℝ ∧ ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ ) ) → ∃ 𝑧 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )
26 20 sseli ( 𝑧 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } → 𝑧 ∈ ℝ )
27 26 anim1i ( ( 𝑧 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ∧ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) ) → ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) ) )
28 27 reximi2 ( ∃ 𝑧 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )
29 24 25 28 3syl ( 𝐶 ∈ ( 𝑂𝐸 ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )