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