Metamath Proof Explorer

Theorem ballotlemfrcn0

Description: Value of F for a reversed counting ( RC ) , before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017) (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 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
Assertion ballotlemfrcn0 ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 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 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11 1zzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 ∈ ℤ )
12 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
13 1 2 12 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ
14 13 nnzi ⊢ ( 𝑀 + 𝑁 ) ∈ ℤ
15 14 a1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
16 1 2 3 4 5 6 7 8 9 ballotlemsdom ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
17 elfzelz ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
18 16 17 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
19 18 3adant3 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
20 19 11 zsubcld ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ℤ )
21 1 2 3 4 5 6 7 8 9 ballotlemsgt1 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) )
22 zltlem1 ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ ) → ( 1 < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ↔ 1 ≤ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) )
23 22 biimpa ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ ) ∧ 1 < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ) → 1 ≤ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) )
24 11 19 21 23 syl21anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 ≤ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) )
25 19 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℝ )
26 1red ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 ∈ ℝ )
27 25 26 resubcld ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ℝ )
28 simp1 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) )
29 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
30 29 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
31 elfzelz ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
32 28 30 31 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
33 32 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℝ )
34 15 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
35 elfzelz ⊢ ( 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝐽 ∈ ℤ )
36 35 3ad2ant2 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
37 elfzle1 ⊢ ( 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 1 ≤ 𝐽 )
38 37 3ad2ant2 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 ≤ 𝐽 )
39 36 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℝ )
40 simp3 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 < ( 𝐼 ‘ 𝐶 ) )
41 39 33 40 ltled ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) )
42 elfz4 ⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝐼 ‘ 𝐶 ) ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 1 ≤ 𝐽 ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
43 11 32 36 38 41 42 syl32anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
44 1 2 3 4 5 6 7 8 9 ballotlemsel1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
45 28 43 44 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
46 elfzle2 ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) )
47 45 46 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) )
48 zlem1lt ⊢ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ ∧ ( 𝐼 ‘ 𝐶 ) ∈ ℤ ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ) )
49 19 32 48 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ) )
50 47 49 mpbid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) )
51 27 33 50 ltled ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ≤ ( 𝐼 ‘ 𝐶 ) )
52 elfzle2 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
53 28 30 52 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
54 27 33 34 51 53 letrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) )
55 elfz4 ⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ℤ ) ∧ ( 1 ≤ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∧ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
56 11 15 20 24 54 55 syl32anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
57 biid ⊢ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) )
58 50 57 sylibr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) )
59 1 2 3 4 5 6 7 8 ballotlemi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
60 59 breq2d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
61 60 3ad2ant1 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
62 58 61 mpbid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
63 ltso ⊢ < Or ℝ
64 63 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → < Or ℝ )
65 1 2 3 4 5 6 7 8 ballotlemsup ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )
66 64 65 inflb ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } → ¬ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
67 66 con2d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) → ¬ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ) )
68 28 62 67 sylc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ¬ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } )
69 fveqeq2 ⊢ ( 𝑘 = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
70 69 elrab ⊢ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ↔ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
71 68 70 sylnib ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ¬ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
72 imnan ⊢ ( ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) ↔ ¬ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
73 71 72 sylibr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
74 56 73 mpd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 )
75 74 neqned ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ≠ 0 )
76 1 2 3 4 5 6 7 8 9 10 ballotlemro ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
77 76 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
78 elfzelz ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
79 78 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ℤ )
80 1 2 3 4 5 77 79 ballotlemfelz ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ∈ ℤ )
81 80 zcnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ∈ ℂ )
82 81 negeq0d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ↔ - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ) )
83 eqid ⊢ ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) ) = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
84 1 2 3 4 5 6 7 8 9 10 83 ballotlemfrceq ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) )
85 84 eqeq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ↔ - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ) )
86 82 85 bitr4d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
87 86 necon3bid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ≠ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ≠ 0 ) )
88 28 43 87 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ≠ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ≠ 0 ) )
89 75 88 mpbird ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ≠ 0 )