Metamath Proof Explorer


Theorem ballotlemfcc

Description: F takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-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
ballotlemfcc.c φ C O
ballotlemfcc.j φ J
ballotlemfcc.3 φ i 1 J 0 F C i
ballotlemfcc.4 φ F C J < 0
Assertion ballotlemfcc φ k 1 J F C k = 0

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 ballotlemfcc.c φ C O
7 ballotlemfcc.j φ J
8 ballotlemfcc.3 φ i 1 J 0 F C i
9 ballotlemfcc.4 φ F C J < 0
10 fveq2 i = k F C i = F C k
11 10 breq2d i = k 0 F C i 0 F C k
12 11 elrab k i 1 J | 0 F C i k 1 J 0 F C k
13 12 anbi1i k i 1 J | 0 F C i j i 1 J | 0 F C i j k k 1 J 0 F C k j i 1 J | 0 F C i j k
14 simprl φ k 1 J 0 F C k k 1 J
15 14 adantrr φ k 1 J 0 F C k j i 1 J | 0 F C i j k k 1 J
16 fzssuz 1 J 1
17 uzssz 1
18 16 17 sstri 1 J
19 zssre
20 18 19 sstri 1 J
21 20 sseli k 1 J k
22 21 ltp1d k 1 J k < k + 1
23 1red k 1 J 1
24 21 23 readdcld k 1 J k + 1
25 21 24 ltnled k 1 J k < k + 1 ¬ k + 1 k
26 22 25 mpbid k 1 J ¬ k + 1 k
27 15 26 syl φ k 1 J 0 F C k j i 1 J | 0 F C i j k ¬ k + 1 k
28 simprr φ k 1 J 0 F C k j i 1 J | 0 F C i j k j i 1 J | 0 F C i j k
29 9 adantr φ k = J F C J < 0
30 simpr φ k = J k = J
31 30 fveq2d φ k = J F C k = F C J
32 31 breq1d φ k = J F C k < 0 F C J < 0
33 elnnuz J J 1
34 7 33 sylib φ J 1
35 eluzfz2 J 1 J 1 J
36 34 35 syl φ J 1 J
37 eleq1 k = J k 1 J J 1 J
38 36 37 syl5ibrcom φ k = J k 1 J
39 38 anc2li φ k = J φ k 1 J
40 1eluzge0 1 0
41 fzss1 1 0 1 J 0 J
42 41 sseld 1 0 k 1 J k 0 J
43 40 42 ax-mp k 1 J k 0 J
44 6 adantr φ k 0 J C O
45 elfzelz k 0 J k
46 45 adantl φ k 0 J k
47 1 2 3 4 5 44 46 ballotlemfelz φ k 0 J F C k
48 47 zred φ k 0 J F C k
49 0red φ k 0 J 0
50 48 49 ltnled φ k 0 J F C k < 0 ¬ 0 F C k
51 43 50 sylan2 φ k 1 J F C k < 0 ¬ 0 F C k
52 39 51 syl6 φ k = J F C k < 0 ¬ 0 F C k
53 52 imp φ k = J F C k < 0 ¬ 0 F C k
54 32 53 bitr3d φ k = J F C J < 0 ¬ 0 F C k
55 29 54 mpbid φ k = J ¬ 0 F C k
56 55 ex φ k = J ¬ 0 F C k
57 56 con2d φ 0 F C k ¬ k = J
58 nn1m1nn J J = 1 J 1
59 7 58 syl φ J = 1 J 1
60 8 adantr φ J = 1 i 1 J 0 F C i
61 oveq1 J = 1 J J = 1 J
62 61 adantl φ J = 1 J J = 1 J
63 7 nnzd φ J
64 fzsn J J J = J
65 63 64 syl φ J J = J
66 65 adantr φ J = 1 J J = J
67 62 66 eqtr3d φ J = 1 1 J = J
68 67 rexeqdv φ J = 1 i 1 J 0 F C i i J 0 F C i
69 60 68 mpbid φ J = 1 i J 0 F C i
70 fveq2 i = J F C i = F C J
71 70 breq2d i = J 0 F C i 0 F C J
72 71 rexsng J i J 0 F C i 0 F C J
73 7 72 syl φ i J 0 F C i 0 F C J
74 73 adantr φ J = 1 i J 0 F C i 0 F C J
75 69 74 mpbid φ J = 1 0 F C J
76 9 adantr φ J = 1 F C J < 0
77 1 2 3 4 5 6 63 ballotlemfelz φ F C J
78 77 zred φ F C J
79 0red φ 0
80 78 79 ltnled φ F C J < 0 ¬ 0 F C J
81 80 adantr φ J = 1 F C J < 0 ¬ 0 F C J
82 76 81 mpbid φ J = 1 ¬ 0 F C J
83 75 82 pm2.65da φ ¬ J = 1
84 biortn ¬ J = 1 J 1 ¬ ¬ J = 1 J 1
85 83 84 syl φ J 1 ¬ ¬ J = 1 J 1
86 notnotb J = 1 ¬ ¬ J = 1
87 86 orbi1i J = 1 J 1 ¬ ¬ J = 1 J 1
88 85 87 bitr4di φ J 1 J = 1 J 1
89 59 88 mpbird φ J 1
90 elnnuz J 1 J 1 1
91 89 90 sylib φ J 1 1
92 elfzp1 J 1 1 k 1 J - 1 + 1 k 1 J 1 k = J - 1 + 1
93 91 92 syl φ k 1 J - 1 + 1 k 1 J 1 k = J - 1 + 1
94 7 nncnd φ J
95 1cnd φ 1
96 94 95 npcand φ J - 1 + 1 = J
97 96 oveq2d φ 1 J - 1 + 1 = 1 J
98 97 eleq2d φ k 1 J - 1 + 1 k 1 J
99 96 eqeq2d φ k = J - 1 + 1 k = J
100 99 orbi2d φ k 1 J 1 k = J - 1 + 1 k 1 J 1 k = J
101 93 98 100 3bitr3d φ k 1 J k 1 J 1 k = J
102 orcom k 1 J 1 k = J k = J k 1 J 1
103 101 102 bitrdi φ k 1 J k = J k 1 J 1
104 103 biimpd φ k 1 J k = J k 1 J 1
105 pm5.6 k 1 J ¬ k = J k 1 J 1 k 1 J k = J k 1 J 1
106 104 105 sylibr φ k 1 J ¬ k = J k 1 J 1
107 89 nnzd φ J 1
108 1z 1
109 107 108 jctil φ 1 J 1
110 elfzelz k 1 J 1 k
111 110 108 jctir k 1 J 1 k 1
112 fzaddel 1 J 1 k 1 k 1 J 1 k + 1 1 + 1 J - 1 + 1
113 109 111 112 syl2an φ k 1 J 1 k 1 J 1 k + 1 1 + 1 J - 1 + 1
114 113 biimp3a φ k 1 J 1 k 1 J 1 k + 1 1 + 1 J - 1 + 1
115 114 3anidm23 φ k 1 J 1 k + 1 1 + 1 J - 1 + 1
116 1p1e2 1 + 1 = 2
117 116 a1i φ 1 + 1 = 2
118 117 96 oveq12d φ 1 + 1 J - 1 + 1 = 2 J
119 118 eleq2d φ k + 1 1 + 1 J - 1 + 1 k + 1 2 J
120 2eluzge1 2 1
121 fzss1 2 1 2 J 1 J
122 120 121 ax-mp 2 J 1 J
123 122 sseli k + 1 2 J k + 1 1 J
124 119 123 syl6bi φ k + 1 1 + 1 J - 1 + 1 k + 1 1 J
125 124 adantr φ k 1 J 1 k + 1 1 + 1 J - 1 + 1 k + 1 1 J
126 115 125 mpd φ k 1 J 1 k + 1 1 J
127 126 ex φ k 1 J 1 k + 1 1 J
128 106 127 syld φ k 1 J ¬ k = J k + 1 1 J
129 57 128 sylan2d φ k 1 J 0 F C k k + 1 1 J
130 129 imp φ k 1 J 0 F C k k + 1 1 J
131 130 adantrr φ k 1 J 0 F C k j i 1 J | 0 F C i j k k + 1 1 J
132 fveq2 i = k + 1 F C i = F C k + 1
133 132 breq2d i = k + 1 0 F C i 0 F C k + 1
134 133 elrab k + 1 i 1 J | 0 F C i k + 1 1 J 0 F C k + 1
135 breq1 j = k + 1 j k k + 1 k
136 135 rspccva j i 1 J | 0 F C i j k k + 1 i 1 J | 0 F C i k + 1 k
137 134 136 sylan2br j i 1 J | 0 F C i j k k + 1 1 J 0 F C k + 1 k + 1 k
138 137 expr j i 1 J | 0 F C i j k k + 1 1 J 0 F C k + 1 k + 1 k
139 138 con3d j i 1 J | 0 F C i j k k + 1 1 J ¬ k + 1 k ¬ 0 F C k + 1
140 28 131 139 syl2anc φ k 1 J 0 F C k j i 1 J | 0 F C i j k ¬ k + 1 k ¬ 0 F C k + 1
141 27 140 mpd φ k 1 J 0 F C k j i 1 J | 0 F C i j k ¬ 0 F C k + 1
142 simplrr φ k 1 J 0 F C k j i 1 J | 0 F C i j k k + 1 C j i 1 J | 0 F C i j k
143 131 adantr φ k 1 J 0 F C k j i 1 J | 0 F C i j k k + 1 C k + 1 1 J
144 0red φ k 1 J 0 F C k k + 1 C 0
145 simpll φ k 1 J 0 F C k k + 1 C φ
146 130 adantr φ k 1 J 0 F C k k + 1 C k + 1 1 J
147 41 sseld 1 0 k + 1 1 J k + 1 0 J
148 40 146 147 mpsyl φ k 1 J 0 F C k k + 1 C k + 1 0 J
149 6 adantr φ k + 1 0 J C O
150 elfzelz k + 1 0 J k + 1
151 150 adantl φ k + 1 0 J k + 1
152 1 2 3 4 5 149 151 ballotlemfelz φ k + 1 0 J F C k + 1
153 152 zred φ k + 1 0 J F C k + 1
154 145 148 153 syl2anc φ k 1 J 0 F C k k + 1 C F C k + 1
155 simplrr φ k 1 J 0 F C k k + 1 C 0 F C k
156 14 adantr φ k 1 J 0 F C k k + 1 C k 1 J
157 156 43 syl φ k 1 J 0 F C k k + 1 C k 0 J
158 129 imdistani φ k 1 J 0 F C k φ k + 1 1 J
159 6 adantr φ k + 1 1 J C O
160 elfznn k + 1 1 J k + 1
161 160 adantl φ k + 1 1 J k + 1
162 1 2 3 4 5 159 161 ballotlemfp1 φ k + 1 1 J ¬ k + 1 C F C k + 1 = F C k + 1 - 1 1 k + 1 C F C k + 1 = F C k + 1 - 1 + 1
163 162 simprd φ k + 1 1 J k + 1 C F C k + 1 = F C k + 1 - 1 + 1
164 163 imp φ k + 1 1 J k + 1 C F C k + 1 = F C k + 1 - 1 + 1
165 158 164 sylan φ k 1 J 0 F C k k + 1 C F C k + 1 = F C k + 1 - 1 + 1
166 elfzelz k 1 J k
167 166 zcnd k 1 J k
168 1cnd k 1 J 1
169 167 168 pncand k 1 J k + 1 - 1 = k
170 169 fveq2d k 1 J F C k + 1 - 1 = F C k
171 170 oveq1d k 1 J F C k + 1 - 1 + 1 = F C k + 1
172 171 eqeq2d k 1 J F C k + 1 = F C k + 1 - 1 + 1 F C k + 1 = F C k + 1
173 156 172 syl φ k 1 J 0 F C k k + 1 C F C k + 1 = F C k + 1 - 1 + 1 F C k + 1 = F C k + 1
174 165 173 mpbid φ k 1 J 0 F C k k + 1 C F C k + 1 = F C k + 1
175 0z 0
176 zleltp1 0 F C k 0 F C k 0 < F C k + 1
177 175 47 176 sylancr φ k 0 J 0 F C k 0 < F C k + 1
178 177 adantr φ k 0 J F C k + 1 = F C k + 1 0 F C k 0 < F C k + 1
179 breq2 F C k + 1 = F C k + 1 0 < F C k + 1 0 < F C k + 1
180 179 adantl φ k 0 J F C k + 1 = F C k + 1 0 < F C k + 1 0 < F C k + 1
181 178 180 bitr4d φ k 0 J F C k + 1 = F C k + 1 0 F C k 0 < F C k + 1
182 145 157 174 181 syl21anc φ k 1 J 0 F C k k + 1 C 0 F C k 0 < F C k + 1
183 155 182 mpbid φ k 1 J 0 F C k k + 1 C 0 < F C k + 1
184 144 154 183 ltled φ k 1 J 0 F C k k + 1 C 0 F C k + 1
185 184 adantlrr φ k 1 J 0 F C k j i 1 J | 0 F C i j k k + 1 C 0 F C k + 1
186 142 143 185 137 syl12anc φ k 1 J 0 F C k j i 1 J | 0 F C i j k k + 1 C k + 1 k
187 27 186 mtand φ k 1 J 0 F C k j i 1 J | 0 F C i j k ¬ k + 1 C
188 162 simpld φ k + 1 1 J ¬ k + 1 C F C k + 1 = F C k + 1 - 1 1
189 188 imp φ k + 1 1 J ¬ k + 1 C F C k + 1 = F C k + 1 - 1 1
190 158 189 sylan φ k 1 J 0 F C k ¬ k + 1 C F C k + 1 = F C k + 1 - 1 1
191 14 adantr φ k 1 J 0 F C k ¬ k + 1 C k 1 J
192 170 oveq1d k 1 J F C k + 1 - 1 1 = F C k 1
193 192 eqeq2d k 1 J F C k + 1 = F C k + 1 - 1 1 F C k + 1 = F C k 1
194 191 193 syl φ k 1 J 0 F C k ¬ k + 1 C F C k + 1 = F C k + 1 - 1 1 F C k + 1 = F C k 1
195 190 194 mpbid φ k 1 J 0 F C k ¬ k + 1 C F C k + 1 = F C k 1
196 195 adantlrr φ k 1 J 0 F C k j i 1 J | 0 F C i j k ¬ k + 1 C F C k + 1 = F C k 1
197 187 196 mpdan φ k 1 J 0 F C k j i 1 J | 0 F C i j k F C k + 1 = F C k 1
198 breq2 F C k + 1 = F C k 1 0 F C k + 1 0 F C k 1
199 198 notbid F C k + 1 = F C k 1 ¬ 0 F C k + 1 ¬ 0 F C k 1
200 197 199 syl φ k 1 J 0 F C k j i 1 J | 0 F C i j k ¬ 0 F C k + 1 ¬ 0 F C k 1
201 141 200 mpbid φ k 1 J 0 F C k j i 1 J | 0 F C i j k ¬ 0 F C k 1
202 14 43 syl φ k 1 J 0 F C k k 0 J
203 202 47 syldan φ k 1 J 0 F C k F C k
204 203 adantrr φ k 1 J 0 F C k j i 1 J | 0 F C i j k F C k
205 zlem1lt F C k 0 F C k 0 F C k 1 < 0
206 175 205 mpan2 F C k F C k 0 F C k 1 < 0
207 zre F C k F C k
208 1red F C k 1
209 207 208 resubcld F C k F C k 1
210 0red F C k 0
211 209 210 ltnled F C k F C k 1 < 0 ¬ 0 F C k 1
212 206 211 bitrd F C k F C k 0 ¬ 0 F C k 1
213 204 212 syl φ k 1 J 0 F C k j i 1 J | 0 F C i j k F C k 0 ¬ 0 F C k 1
214 201 213 mpbird φ k 1 J 0 F C k j i 1 J | 0 F C i j k F C k 0
215 simprlr φ k 1 J 0 F C k j i 1 J | 0 F C i j k 0 F C k
216 204 zred φ k 1 J 0 F C k j i 1 J | 0 F C i j k F C k
217 0red φ k 1 J 0 F C k j i 1 J | 0 F C i j k 0
218 216 217 letri3d φ k 1 J 0 F C k j i 1 J | 0 F C i j k F C k = 0 F C k 0 0 F C k
219 214 215 218 mpbir2and φ k 1 J 0 F C k j i 1 J | 0 F C i j k F C k = 0
220 13 219 sylan2b φ k i 1 J | 0 F C i j i 1 J | 0 F C i j k F C k = 0
221 ssrab2 i 1 J | 0 F C i 1 J
222 221 20 sstri i 1 J | 0 F C i
223 222 a1i φ i 1 J | 0 F C i
224 fzfi 1 J Fin
225 ssfi 1 J Fin i 1 J | 0 F C i 1 J i 1 J | 0 F C i Fin
226 224 221 225 mp2an i 1 J | 0 F C i Fin
227 226 a1i φ i 1 J | 0 F C i Fin
228 rabn0 i 1 J | 0 F C i i 1 J 0 F C i
229 8 228 sylibr φ i 1 J | 0 F C i
230 fimaxre i 1 J | 0 F C i i 1 J | 0 F C i Fin i 1 J | 0 F C i k i 1 J | 0 F C i j i 1 J | 0 F C i j k
231 223 227 229 230 syl3anc φ k i 1 J | 0 F C i j i 1 J | 0 F C i j k
232 220 231 reximddv φ k i 1 J | 0 F C i F C k = 0
233 elrabi k i 1 J | 0 F C i k 1 J
234 233 anim1i k i 1 J | 0 F C i F C k = 0 k 1 J F C k = 0
235 234 reximi2 k i 1 J | 0 F C i F C k = 0 k 1 J F C k = 0
236 232 235 syl φ k 1 J F C k = 0