Metamath Proof Explorer

Theorem ballotlemiex

Description: Properties of ( IC ) . (Contributed by Thierry Arnoux, 12-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 ballotlemiex ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 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 1 2 3 4 5 6 7 8 ballotlemi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
10 ltso ⊢ < Or ℝ
11 10 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → < Or ℝ )
12 fzfi ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
13 ssrab2 ⊢ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ( 1 ... ( 𝑀 + 𝑁 ) )
14 ssfi ⊢ ( ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin )
15 12 13 14 mp2an ⊢ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin
16 15 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin )
17 1 2 3 4 5 6 7 ballotlem5 ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
18 rabn0 ⊢ ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ ↔ ∃ 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
19 17 18 sylibr ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ )
20 fzssuz ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ( ℤ≥ ‘ 1 )
21 uzssz ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
22 20 21 sstri ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ℤ
23 zssre ⊢ ℤ ⊆ ℝ
24 22 23 sstri ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ℝ
25 13 24 sstri ⊢ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ
26 25 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ )
27 fiinfcl ⊢ ( ( < Or ℝ ∧ ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ∈ Fin ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ≠ ∅ ∧ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ⊆ ℝ ) ) → inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } )
28 11 16 19 26 27 syl13anc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } )
29 9 28 eqeltrd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } )
30 fveqeq2 ⊢ ( 𝑘 = ( 𝐼 ‘ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
31 30 elrab ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ↔ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
32 29 31 sylib ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )