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