Metamath Proof Explorer

Theorem ballotlemfc0

Description: F takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016)

Ref Expression
Hypotheses ballotth.m 
|- M e. NN
ballotth.n 
|- N e. NN
ballotth.o 
|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
ballotth.p 
|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
ballotth.f 
|- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
ballotlemfp1.c 
|- ( ph -> C e. O )
ballotlemfp1.j 
|- ( ph -> J e. NN )
ballotlemfc0.3 
|- ( ph -> E. i e. ( 1 ... J ) ( ( F ` C ) ` i ) <_ 0 )
ballotlemfc0.4 
|- ( ph -> 0 < ( ( F ` C ) ` J ) )
Assertion ballotlemfc0 
|- ( ph -> E. k e. ( 1 ... J ) ( ( F ` C ) ` k ) = 0 )

Proof

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