Metamath Proof Explorer

Theorem ballotlemfrceq

Description: Value of F for a reverse counting ( RC ) . (Contributed by Thierry Arnoux, 27-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 ) − 𝑖 ) , 𝑖 ) ) )
ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
ballotlemg ⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
Assertion ballotlemfrceq ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 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 ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11 ballotlemg ⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
12 1 2 3 4 5 6 7 8 9 ballotlemsel1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
13 1zzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 1 ∈ ℤ )
14 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
15 14 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
16 15 simpld ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
17 elfzelz ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
18 16 17 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
19 elfzuz3 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) )
20 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) → ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
21 16 19 20 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
22 simpr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
23 21 22 sseldd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
24 1 2 3 4 5 6 7 8 9 ballotlemsdom ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
25 23 24 syldan ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
26 elfzelz ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
27 25 26 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ )
28 fzsubel ⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝐼 ‘ 𝐶 ) ∈ ℤ ) ∧ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) )
29 13 18 27 13 28 syl22anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ↔ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) )
30 12 29 mpbid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( ( 1 − 1 ) ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
31 1m1e0 ⊢ ( 1 − 1 ) = 0
32 31 oveq1i ⊢ ( ( 1 − 1 ) ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) = ( 0 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) )
33 30 32 eleqtrdi ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 0 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
34 14 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
35 34 17 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
36 1zzd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 1 ∈ ℤ )
37 35 36 zsubcld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℤ )
38 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
39 1 2 38 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ
40 39 nnzi ⊢ ( 𝑀 + 𝑁 ) ∈ ℤ
41 40 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
42 elfzle2 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
43 34 42 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
44 zlem1lt ⊢ ( ( ( 𝐼 ‘ 𝐶 ) ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) ↔ ( ( 𝐼 ‘ 𝐶 ) − 1 ) < ( 𝑀 + 𝑁 ) ) )
45 35 41 44 syl2anc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) ↔ ( ( 𝐼 ‘ 𝐶 ) − 1 ) < ( 𝑀 + 𝑁 ) ) )
46 37 zred ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℝ )
47 41 zred ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
48 ltle ⊢ ( ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℝ ∧ ( 𝑀 + 𝑁 ) ∈ ℝ ) → ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) < ( 𝑀 + 𝑁 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) ) )
49 46 47 48 syl2anc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) < ( 𝑀 + 𝑁 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) ) )
50 45 49 sylbid ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) ) )
51 43 50 mpd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) )
52 eluz2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) ) )
53 37 41 51 52 syl3anbrc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
54 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) → ( 0 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
55 53 54 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 0 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
56 55 sselda ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 0 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
57 33 56 syldan ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
58 1 2 3 4 5 6 7 8 9 10 11 ballotlemfg ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = ( 𝐶 ↑ ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ) )
59 57 58 syldan ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = ( 𝐶 ↑ ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ) )
60 1 2 3 4 5 6 7 8 9 10 11 ballotlemfrc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) = ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )
61 59 60 oveq12d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) + ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ) = ( ( 𝐶 ↑ ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ) + ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) ) )
62 fzsplit3 ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → ( 1 ... ( 𝐼 ‘ 𝐶 ) ) = ( ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∪ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )
63 12 62 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 1 ... ( 𝐼 ‘ 𝐶 ) ) = ( ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∪ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )
64 63 oveq2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐶 ↑ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) = ( 𝐶 ↑ ( ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∪ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) ) )
65 fz1ssfz0 ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) )
66 65 sseli ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
67 1 2 3 4 5 6 7 8 9 10 11 ballotlemfg ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = ( 𝐶 ↑ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) )
68 66 67 sylan2 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = ( 𝐶 ↑ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) )
69 16 68 syldan ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = ( 𝐶 ↑ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) )
70 15 simprd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
71 69 70 eqtr3d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐶 ↑ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) = 0 )
72 fzfi ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
73 eldifi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ∈ 𝑂 )
74 1 2 3 ballotlemelo ⊢ ( 𝐶 ∈ 𝑂 ↔ ( 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ♯ ‘ 𝐶 ) = 𝑀 ) )
75 74 simplbi ⊢ ( 𝐶 ∈ 𝑂 → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
76 73 75 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
77 ssfi ⊢ ( ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ 𝐶 ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝐶 ∈ Fin )
78 72 76 77 sylancr ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ∈ Fin )
79 78 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐶 ∈ Fin )
80 fzfid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∈ Fin )
81 fzfid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ∈ Fin )
82 27 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℝ )
83 ltm1 ⊢ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ∈ ℝ → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) )
84 fzdisj ⊢ ( ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) < ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) → ( ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∩ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) = ∅ )
85 82 83 84 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∩ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) = ∅ )
86 1 2 3 4 5 6 7 8 9 10 11 79 80 81 85 ballotlemgun ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐶 ↑ ( ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∪ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) ) = ( ( 𝐶 ↑ ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ) + ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) ) )
87 64 71 86 3eqtr3rd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐶 ↑ ( 1 ... ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ) + ( 𝐶 ↑ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) ) = 0 )
88 61 87 eqtrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) + ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ) = 0 )
89 73 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐶 ∈ 𝑂 )
90 27 13 zsubcld ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ∈ ℤ )
91 1 2 3 4 5 89 90 ballotlemfelz ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∈ ℤ )
92 91 zcnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∈ ℂ )
93 1 2 3 4 5 6 7 8 9 10 ballotlemro ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
94 93 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑅 ‘ 𝐶 ) ∈ 𝑂 )
95 elfzelz ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
96 22 95 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ℤ )
97 1 2 3 4 5 94 96 ballotlemfelz ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ∈ ℤ )
98 97 zcnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ∈ ℂ )
99 addeq0 ⊢ ( ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) ∈ ℂ ∧ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ∈ ℂ ) → ( ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) + ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ) )
100 92 98 99 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) + ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) ) )
101 88 100 mpbid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) − 1 ) ) = - ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝐽 ) )