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
ballotth.n N
ballotth.o O = c 𝒫 1 M + N | c = M
ballotth.p P = x 𝒫 O x O
ballotth.f F = c O i 1 i c 1 i c
ballotth.e E = c O | i 1 M + N 0 < F c i
ballotth.mgtn N < M
ballotth.i I = c O E sup k 1 M + N | F c k = 0 <
ballotth.s S = c O E i 1 M + N if i I c I c + 1 - i i
Assertion ballotlemsima C O E J 1 I C S C 1 J = S C J I C

Proof

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