Metamath Proof Explorer

Theorem ballotlemsdom

Description: Domain of S for a given counting C . (Contributed by Thierry Arnoux, 12-Apr-2017)

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 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
Assertion ballotlemsdom ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )

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 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 1 2 3 4 5 6 7 8 9 ballotlemsv ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )
11 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
12 11 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
13 12 elfzelzd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
14 13 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
15 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
16 1 2 15 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ
17 16 nnzi ⊢ ( 𝑀 + 𝑁 ) ∈ ℤ
18 17 a1i ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
19 12 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
20 elfzle2 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
21 19 20 syl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
22 eluz2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) ↔ ( ( 𝐼 ‘ 𝐶 ) ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) ) )
23 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) → ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
24 22 23 sylbir ⊢ ( ( ( 𝐼 ‘ 𝐶 ) ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) ) → ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
25 14 18 21 24 syl3anc ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
26 1zzd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 1 ∈ ℤ )
27 simplr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
28 27 elfzelzd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
29 elfzle1 ⊢ ( 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 1 ≤ 𝐽 )
30 27 29 syl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 1 ≤ 𝐽 )
31 simpr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) )
32 26 14 28 30 31 elfzd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
33 fzrev3i ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → ( ( 1 + ( 𝐼 ‘ 𝐶 ) ) − 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
34 32 33 syl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( ( 1 + ( 𝐼 ‘ 𝐶 ) ) − 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
35 1cnd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 1 ∈ ℂ )
36 13 zcnd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℂ )
37 35 36 addcomd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 1 + ( 𝐼 ‘ 𝐶 ) ) = ( ( 𝐼 ‘ 𝐶 ) + 1 ) )
38 37 oveq1d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 1 + ( 𝐼 ‘ 𝐶 ) ) − 𝐽 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) )
39 38 eleq1d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( 1 + ( 𝐼 ‘ 𝐶 ) ) − 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) )
40 39 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 1 + ( 𝐼 ‘ 𝐶 ) ) − 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) )
41 34 40 mpbid ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
42 25 41 sseldd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
43 simplr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ ¬ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
44 42 43 ifclda ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
45 10 44 eqeltrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )