Metamath Proof Explorer


Theorem ballotlemsup

Description: The set of zeroes of F satisfies the conditions to have a supremum. (Contributed by Thierry Arnoux, 1-Dec-2016) (Revised by AV, 6-Oct-2020)

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 ) ) ) ) )
ballotth.e
|- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }
ballotth.mgtn
|- N < M
ballotth.i
|- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )
Assertion ballotlemsup
|- ( C e. ( O \ E ) -> E. z e. RR ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) )

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 ballotth.e
 |-  E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }
7 ballotth.mgtn
 |-  N < M
8 ballotth.i
 |-  I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )
9 fzfi
 |-  ( 1 ... ( M + N ) ) e. Fin
10 ssrab2
 |-  { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } C_ ( 1 ... ( M + N ) )
11 ssfi
 |-  ( ( ( 1 ... ( M + N ) ) e. Fin /\ { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } C_ ( 1 ... ( M + N ) ) ) -> { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } e. Fin )
12 9 10 11 mp2an
 |-  { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } e. Fin
13 12 a1i
 |-  ( C e. ( O \ E ) -> { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } e. Fin )
14 1 2 3 4 5 6 7 ballotlem5
 |-  ( C e. ( O \ E ) -> E. k e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` k ) = 0 )
15 rabn0
 |-  ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } =/= (/) <-> E. k e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` k ) = 0 )
16 14 15 sylibr
 |-  ( C e. ( O \ E ) -> { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } =/= (/) )
17 fz1ssnn
 |-  ( 1 ... ( M + N ) ) C_ NN
18 nnssre
 |-  NN C_ RR
19 17 18 sstri
 |-  ( 1 ... ( M + N ) ) C_ RR
20 10 19 sstri
 |-  { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } C_ RR
21 20 a1i
 |-  ( C e. ( O \ E ) -> { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } C_ RR )
22 13 16 21 3jca
 |-  ( C e. ( O \ E ) -> ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } e. Fin /\ { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } =/= (/) /\ { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } C_ RR ) )
23 ltso
 |-  < Or RR
24 22 23 jctil
 |-  ( C e. ( O \ E ) -> ( < Or RR /\ ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } e. Fin /\ { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } =/= (/) /\ { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } C_ RR ) ) )
25 fiinf2g
 |-  ( ( < Or RR /\ ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } e. Fin /\ { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } =/= (/) /\ { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } C_ RR ) ) -> E. z e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) )
26 20 sseli
 |-  ( z e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -> z e. RR )
27 26 anim1i
 |-  ( ( z e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } /\ ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) ) -> ( z e. RR /\ ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) ) )
28 27 reximi2
 |-  ( E. z e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) -> E. z e. RR ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) )
29 24 25 28 3syl
 |-  ( C e. ( O \ E ) -> E. z e. RR ( A. w e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } -. w < z /\ A. w e. RR ( z < w -> E. y e. { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } y < w ) ) )