# Metamath Proof Explorer

## Theorem ballotlemsima

Description: The image by S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017)

Ref Expression
Hypotheses ballotth.m ${⊢}{M}\in ℕ$
ballotth.n ${⊢}{N}\in ℕ$
ballotth.o ${⊢}{O}=\left\{{c}\in 𝒫\left(1\dots {M}+{N}\right)|\left|{c}\right|={M}\right\}$
ballotth.p ${⊢}{P}=\left({x}\in 𝒫{O}⟼\frac{\left|{x}\right|}{\left|{O}\right|}\right)$
ballotth.f ${⊢}{F}=\left({c}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|\right)\right)$
ballotth.e ${⊢}{E}=\left\{{c}\in {O}|\forall {i}\in \left(1\dots {M}+{N}\right)\phantom{\rule{.4em}{0ex}}0<{F}\left({c}\right)\left({i}\right)\right\}$
ballotth.mgtn ${⊢}{N}<{M}$
ballotth.i ${⊢}{I}=\left({c}\in \left({O}\setminus {E}\right)⟼sup\left(\left\{{k}\in \left(1\dots {M}+{N}\right)|{F}\left({c}\right)\left({k}\right)=0\right\},ℝ,<\right)\right)$
ballotth.s ${⊢}{S}=\left({c}\in \left({O}\setminus {E}\right)⟼\left({i}\in \left(1\dots {M}+{N}\right)⟼if\left({i}\le {I}\left({c}\right),{I}\left({c}\right)+1-{i},{i}\right)\right)\right)$
Assertion ballotlemsima ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]=\left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ballotth.m ${⊢}{M}\in ℕ$
2 ballotth.n ${⊢}{N}\in ℕ$
3 ballotth.o ${⊢}{O}=\left\{{c}\in 𝒫\left(1\dots {M}+{N}\right)|\left|{c}\right|={M}\right\}$
4 ballotth.p ${⊢}{P}=\left({x}\in 𝒫{O}⟼\frac{\left|{x}\right|}{\left|{O}\right|}\right)$
5 ballotth.f ${⊢}{F}=\left({c}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|\right)\right)$
6 ballotth.e ${⊢}{E}=\left\{{c}\in {O}|\forall {i}\in \left(1\dots {M}+{N}\right)\phantom{\rule{.4em}{0ex}}0<{F}\left({c}\right)\left({i}\right)\right\}$
7 ballotth.mgtn ${⊢}{N}<{M}$
8 ballotth.i ${⊢}{I}=\left({c}\in \left({O}\setminus {E}\right)⟼sup\left(\left\{{k}\in \left(1\dots {M}+{N}\right)|{F}\left({c}\right)\left({k}\right)=0\right\},ℝ,<\right)\right)$
9 ballotth.s ${⊢}{S}=\left({c}\in \left({O}\setminus {E}\right)⟼\left({i}\in \left(1\dots {M}+{N}\right)⟼if\left({i}\le {I}\left({c}\right),{I}\left({c}\right)+1-{i},{i}\right)\right)\right)$
10 imassrn ${⊢}{S}\left({C}\right)\left[\left(1\dots {J}\right)\right]\subseteq \mathrm{ran}{S}\left({C}\right)$
11 1 2 3 4 5 6 7 8 9 ballotlemsf1o ${⊢}{C}\in \left({O}\setminus {E}\right)\to \left({S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)\wedge {{S}\left({C}\right)}^{-1}={S}\left({C}\right)\right)$
12 11 simpld ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)$
13 f1of ${⊢}{S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)\to {S}\left({C}\right):\left(1\dots {M}+{N}\right)⟶\left(1\dots {M}+{N}\right)$
14 frn ${⊢}{S}\left({C}\right):\left(1\dots {M}+{N}\right)⟶\left(1\dots {M}+{N}\right)\to \mathrm{ran}{S}\left({C}\right)\subseteq \left(1\dots {M}+{N}\right)$
15 12 13 14 3syl ${⊢}{C}\in \left({O}\setminus {E}\right)\to \mathrm{ran}{S}\left({C}\right)\subseteq \left(1\dots {M}+{N}\right)$
16 10 15 sstrid ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]\subseteq \left(1\dots {M}+{N}\right)$
17 fzssuz ${⊢}\left(1\dots {M}+{N}\right)\subseteq {ℤ}_{\ge 1}$
18 uzssz ${⊢}{ℤ}_{\ge 1}\subseteq ℤ$
19 17 18 sstri ${⊢}\left(1\dots {M}+{N}\right)\subseteq ℤ$
20 16 19 sstrdi ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]\subseteq ℤ$
21 20 adantr ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]\subseteq ℤ$
22 21 sselda ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]\right)\to {k}\in ℤ$
23 elfzelz ${⊢}{k}\in \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)\to {k}\in ℤ$
24 23 adantl ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)\right)\to {k}\in ℤ$
25 f1ofn ${⊢}{S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)\to {S}\left({C}\right)Fn\left(1\dots {M}+{N}\right)$
26 12 25 syl ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right)Fn\left(1\dots {M}+{N}\right)$
27 26 adantr ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {S}\left({C}\right)Fn\left(1\dots {M}+{N}\right)$
28 1 2 3 4 5 6 7 8 ballotlemiex ${⊢}{C}\in \left({O}\setminus {E}\right)\to \left({I}\left({C}\right)\in \left(1\dots {M}+{N}\right)\wedge {F}\left({C}\right)\left({I}\left({C}\right)\right)=0\right)$
29 28 simpld ${⊢}{C}\in \left({O}\setminus {E}\right)\to {I}\left({C}\right)\in \left(1\dots {M}+{N}\right)$
30 29 adantr ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {I}\left({C}\right)\in \left(1\dots {M}+{N}\right)$
31 elfzuz3 ${⊢}{I}\left({C}\right)\in \left(1\dots {M}+{N}\right)\to {M}+{N}\in {ℤ}_{\ge {I}\left({C}\right)}$
32 30 31 syl ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {M}+{N}\in {ℤ}_{\ge {I}\left({C}\right)}$
33 elfzuz3 ${⊢}{J}\in \left(1\dots {I}\left({C}\right)\right)\to {I}\left({C}\right)\in {ℤ}_{\ge {J}}$
34 33 adantl ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {I}\left({C}\right)\in {ℤ}_{\ge {J}}$
35 uztrn ${⊢}\left({M}+{N}\in {ℤ}_{\ge {I}\left({C}\right)}\wedge {I}\left({C}\right)\in {ℤ}_{\ge {J}}\right)\to {M}+{N}\in {ℤ}_{\ge {J}}$
36 32 34 35 syl2anc ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {M}+{N}\in {ℤ}_{\ge {J}}$
37 fzss2 ${⊢}{M}+{N}\in {ℤ}_{\ge {J}}\to \left(1\dots {J}\right)\subseteq \left(1\dots {M}+{N}\right)$
38 36 37 syl ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to \left(1\dots {J}\right)\subseteq \left(1\dots {M}+{N}\right)$
39 fvelimab ${⊢}\left({S}\left({C}\right)Fn\left(1\dots {M}+{N}\right)\wedge \left(1\dots {J}\right)\subseteq \left(1\dots {M}+{N}\right)\right)\to \left({k}\in {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]↔\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{S}\left({C}\right)\left({j}\right)={k}\right)$
40 27 38 39 syl2anc ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to \left({k}\in {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]↔\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{S}\left({C}\right)\left({j}\right)={k}\right)$
41 40 adantr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({k}\in {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]↔\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{S}\left({C}\right)\left({j}\right)={k}\right)$
42 1zzd ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to 1\in ℤ$
43 1 nnzi ${⊢}{M}\in ℤ$
44 2 nnzi ${⊢}{N}\in ℤ$
45 zaddcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}+{N}\in ℤ$
46 43 44 45 mp2an ${⊢}{M}+{N}\in ℤ$
47 46 a1i ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {M}+{N}\in ℤ$
48 elfzelz ${⊢}{J}\in \left(1\dots {I}\left({C}\right)\right)\to {J}\in ℤ$
49 48 adantl ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {J}\in ℤ$
50 elfzle1 ${⊢}{J}\in \left(1\dots {I}\left({C}\right)\right)\to 1\le {J}$
51 50 adantl ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to 1\le {J}$
52 49 zred ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {J}\in ℝ$
53 elfzelz ${⊢}{I}\left({C}\right)\in \left(1\dots {M}+{N}\right)\to {I}\left({C}\right)\in ℤ$
54 29 53 syl ${⊢}{C}\in \left({O}\setminus {E}\right)\to {I}\left({C}\right)\in ℤ$
55 54 adantr ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {I}\left({C}\right)\in ℤ$
56 55 zred ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {I}\left({C}\right)\in ℝ$
57 47 zred ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {M}+{N}\in ℝ$
58 elfzle2 ${⊢}{J}\in \left(1\dots {I}\left({C}\right)\right)\to {J}\le {I}\left({C}\right)$
59 58 adantl ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {J}\le {I}\left({C}\right)$
60 elfzle2 ${⊢}{I}\left({C}\right)\in \left(1\dots {M}+{N}\right)\to {I}\left({C}\right)\le {M}+{N}$
61 29 60 syl ${⊢}{C}\in \left({O}\setminus {E}\right)\to {I}\left({C}\right)\le {M}+{N}$
62 61 adantr ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {I}\left({C}\right)\le {M}+{N}$
63 52 56 57 59 62 letrd ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {J}\le {M}+{N}$
64 elfz4 ${⊢}\left(\left(1\in ℤ\wedge {M}+{N}\in ℤ\wedge {J}\in ℤ\right)\wedge \left(1\le {J}\wedge {J}\le {M}+{N}\right)\right)\to {J}\in \left(1\dots {M}+{N}\right)$
65 42 47 49 51 63 64 syl32anc ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {J}\in \left(1\dots {M}+{N}\right)$
66 1 2 3 4 5 6 7 8 9 ballotlemsv ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {M}+{N}\right)\right)\to {S}\left({C}\right)\left({J}\right)=if\left({J}\le {I}\left({C}\right),{I}\left({C}\right)+1-{J},{J}\right)$
67 65 66 syldan ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {S}\left({C}\right)\left({J}\right)=if\left({J}\le {I}\left({C}\right),{I}\left({C}\right)+1-{J},{J}\right)$
68 simpr ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {J}\in \left(1\dots {I}\left({C}\right)\right)$
69 iftrue ${⊢}{J}\le {I}\left({C}\right)\to if\left({J}\le {I}\left({C}\right),{I}\left({C}\right)+1-{J},{J}\right)={I}\left({C}\right)+1-{J}$
70 68 58 69 3syl ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to if\left({J}\le {I}\left({C}\right),{I}\left({C}\right)+1-{J},{J}\right)={I}\left({C}\right)+1-{J}$
71 67 70 eqtrd ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {S}\left({C}\right)\left({J}\right)={I}\left({C}\right)+1-{J}$
72 71 oveq1d ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)=\left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)\right)$
73 72 eleq2d ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to \left({k}\in \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)↔{k}\in \left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)\right)\right)$
74 73 adantr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({k}\in \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)↔{k}\in \left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)\right)\right)$
75 54 ad2antrr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to {I}\left({C}\right)\in ℤ$
76 75 zcnd ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to {I}\left({C}\right)\in ℂ$
77 1cnd ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to 1\in ℂ$
78 76 77 pncand ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to {I}\left({C}\right)+1-1={I}\left({C}\right)$
79 78 oveq2d ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)+1-1\right)=\left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)\right)$
80 79 eleq2d ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({k}\in \left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)+1-1\right)↔{k}\in \left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)\right)\right)$
81 1zzd ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to 1\in ℤ$
82 48 ad2antlr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to {J}\in ℤ$
83 75 peano2zd ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to {I}\left({C}\right)+1\in ℤ$
84 simpr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to {k}\in ℤ$
85 fzrev ${⊢}\left(\left(1\in ℤ\wedge {J}\in ℤ\right)\wedge \left({I}\left({C}\right)+1\in ℤ\wedge {k}\in ℤ\right)\right)\to \left({k}\in \left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)+1-1\right)↔{I}\left({C}\right)+1-{k}\in \left(1\dots {J}\right)\right)$
86 81 82 83 84 85 syl22anc ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({k}\in \left({I}\left({C}\right)+1-{J}\dots {I}\left({C}\right)+1-1\right)↔{I}\left({C}\right)+1-{k}\in \left(1\dots {J}\right)\right)$
87 74 80 86 3bitr2d ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({k}\in \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)↔{I}\left({C}\right)+1-{k}\in \left(1\dots {J}\right)\right)$
88 risset ${⊢}{I}\left({C}\right)+1-{k}\in \left(1\dots {J}\right)↔\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{j}={I}\left({C}\right)+1-{k}$
89 88 a1i ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({I}\left({C}\right)+1-{k}\in \left(1\dots {J}\right)↔\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{j}={I}\left({C}\right)+1-{k}\right)$
90 eqcom ${⊢}{I}\left({C}\right)+1-{k}={j}↔{j}={I}\left({C}\right)+1-{k}$
91 54 ad2antrr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {I}\left({C}\right)\in ℤ$
92 91 adantlr ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {I}\left({C}\right)\in ℤ$
93 92 zcnd ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {I}\left({C}\right)\in ℂ$
94 1cnd ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to 1\in ℂ$
95 93 94 addcld ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {I}\left({C}\right)+1\in ℂ$
96 simplr ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {k}\in ℤ$
97 96 zcnd ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {k}\in ℂ$
98 elfzelz ${⊢}{j}\in \left(1\dots {J}\right)\to {j}\in ℤ$
99 98 adantl ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {j}\in ℤ$
100 99 zcnd ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {j}\in ℂ$
101 subsub23 ${⊢}\left({I}\left({C}\right)+1\in ℂ\wedge {k}\in ℂ\wedge {j}\in ℂ\right)\to \left({I}\left({C}\right)+1-{k}={j}↔{I}\left({C}\right)+1-{j}={k}\right)$
102 95 97 100 101 syl3anc ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to \left({I}\left({C}\right)+1-{k}={j}↔{I}\left({C}\right)+1-{j}={k}\right)$
103 90 102 syl5bbr ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to \left({j}={I}\left({C}\right)+1-{k}↔{I}\left({C}\right)+1-{j}={k}\right)$
104 simpll ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {C}\in \left({O}\setminus {E}\right)$
105 38 sselda ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {j}\in \left(1\dots {M}+{N}\right)$
106 1 2 3 4 5 6 7 8 9 ballotlemsv ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {j}\in \left(1\dots {M}+{N}\right)\right)\to {S}\left({C}\right)\left({j}\right)=if\left({j}\le {I}\left({C}\right),{I}\left({C}\right)+1-{j},{j}\right)$
107 104 105 106 syl2anc ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {S}\left({C}\right)\left({j}\right)=if\left({j}\le {I}\left({C}\right),{I}\left({C}\right)+1-{j},{j}\right)$
108 98 adantl ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {j}\in ℤ$
109 108 zred ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {j}\in ℝ$
110 48 ad2antlr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {J}\in ℤ$
111 110 zred ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {J}\in ℝ$
112 91 zred ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {I}\left({C}\right)\in ℝ$
113 elfzle2 ${⊢}{j}\in \left(1\dots {J}\right)\to {j}\le {J}$
114 113 adantl ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {j}\le {J}$
115 58 ad2antlr ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {J}\le {I}\left({C}\right)$
116 109 111 112 114 115 letrd ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {j}\le {I}\left({C}\right)$
117 iftrue ${⊢}{j}\le {I}\left({C}\right)\to if\left({j}\le {I}\left({C}\right),{I}\left({C}\right)+1-{j},{j}\right)={I}\left({C}\right)+1-{j}$
118 116 117 syl ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to if\left({j}\le {I}\left({C}\right),{I}\left({C}\right)+1-{j},{j}\right)={I}\left({C}\right)+1-{j}$
119 107 118 eqtrd ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to {S}\left({C}\right)\left({j}\right)={I}\left({C}\right)+1-{j}$
120 119 eqeq1d ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to \left({S}\left({C}\right)\left({j}\right)={k}↔{I}\left({C}\right)+1-{j}={k}\right)$
121 120 adantlr ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to \left({S}\left({C}\right)\left({j}\right)={k}↔{I}\left({C}\right)+1-{j}={k}\right)$
122 103 121 bitr4d ${⊢}\left(\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\wedge {j}\in \left(1\dots {J}\right)\right)\to \left({j}={I}\left({C}\right)+1-{k}↔{S}\left({C}\right)\left({j}\right)={k}\right)$
123 122 rexbidva ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left(\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{j}={I}\left({C}\right)+1-{k}↔\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{S}\left({C}\right)\left({j}\right)={k}\right)$
124 87 89 123 3bitrd ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({k}\in \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)↔\exists {j}\in \left(1\dots {J}\right)\phantom{\rule{.4em}{0ex}}{S}\left({C}\right)\left({j}\right)={k}\right)$
125 41 124 bitr4d ${⊢}\left(\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\wedge {k}\in ℤ\right)\to \left({k}\in {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]↔{k}\in \left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)\right)$
126 22 24 125 eqrdav ${⊢}\left({C}\in \left({O}\setminus {E}\right)\wedge {J}\in \left(1\dots {I}\left({C}\right)\right)\right)\to {S}\left({C}\right)\left[\left(1\dots {J}\right)\right]=\left({S}\left({C}\right)\left({J}\right)\dots {I}\left({C}\right)\right)$