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 16 elfzelzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
18 17 3adant3 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
19 18 11 zsubcld ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ℤ )
20 1 2 3 4 5 6 7 8 9 ballotlemsgt1 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) )
21 zltlem1 ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ ) → ( 1 < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ↔ 1 ≤ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) )
22 21 biimpa ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ ) ∧ 1 < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ) → 1 ≤ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) )
23 11 18 20 22 syl21anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 ≤ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) )
24 18 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℝ )
25 1red ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 ∈ ℝ )
26 24 25 resubcld ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ℝ )
27 simp1 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) )
28 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
29 28 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
30 elfzelz ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
31 27 29 30 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
32 31 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℝ )
33 15 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
34 elfzelz ⊢ ( 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝐽 ∈ ℤ )
35 34 3ad2ant2 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
36 elfzle1 ⊢ ( 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 1 ≤ 𝐽 )
37 36 3ad2ant2 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 1 ≤ 𝐽 )
38 35 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℝ )
39 simp3 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 < ( 𝐼 ‘ 𝐶 ) )
40 38 32 39 ltled ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) )
41 11 31 35 37 40 elfzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
42 1 2 3 4 5 6 7 8 9 ballotlemsel1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
43 27 41 42 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
44 elfzle2 ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) )
45 43 44 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) )
46 zlem1lt ⊢ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ ∧ ( 𝐼 ‘ 𝐶 ) ∈ ℤ ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ) )
47 18 31 46 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ≤ ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ) )
48 45 47 mpbid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) )
49 26 32 48 ltled ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ≤ ( 𝐼 ‘ 𝐶 ) )
50 elfzle2 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
51 27 29 50 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
52 26 32 33 49 51 letrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) )
53 11 15 19 23 52 elfzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
54 biid ⊢ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) )
55 48 54 sylibr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) )
56 1 2 3 4 5 6 7 8 ballotlemi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
57 56 breq2d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
58 57 3ad2ant1 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( 𝐼 ‘ 𝐶 ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
59 55 58 mpbid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
60 ltso ⊢ < Or ℝ
61 60 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → < Or ℝ )
62 1 2 3 4 5 6 7 8 ballotlemsup ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )
63 61 62 inflb ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } → ¬ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
64 63 con2d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) → ¬ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ) )
65 27 59 64 sylc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ¬ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } )
66 fveqeq2 ⊢ ( 𝑘 = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
67 66 elrab ⊢ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ↔ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
68 65 67 sylnib ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ¬ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
69 imnan ⊢ ( ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) ↔ ¬ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
70 68 69 sylibr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
71 53 70 mpd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 )
72 71 neqned ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ≠ 0 )
73 1 2 3 4 5 6 7 8 9 10 ballotlemro ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
74 73 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
75 elfzelz ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
76 75 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ℤ )
77 1 2 3 4 5 74 76 ballotlemfelz ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ∈ ℤ )
78 77 zcnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ∈ ℂ )
79 78 negeq0d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ↔ - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ) )
80 eqid ⊢ ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) ) = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
81 1 2 3 4 5 6 7 8 9 10 80 ballotlemfrceq ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) )
82 81 eqeq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ↔ - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ) )
83 79 82 bitr4d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = 0 ) )
84 83 necon3bid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ≠ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ≠ 0 ) )
85 27 41 84 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ≠ 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ≠ 0 ) )
86 72 85 mpbird ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ≠ 0 )