Metamath Proof Explorer

Theorem ballotlemodife

Description: Elements of ( O \ E ) . (Contributed by Thierry Arnoux, 7-Dec-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 ) ) ) ) )
ballotth.e 
|- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }
Assertion ballotlemodife 
|- ( C e. ( O \ E ) <-> ( C e. O /\ E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 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 ballotth.e 
 |-  E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }
7 eldif 
 |-  ( C e. ( O \ E ) <-> ( C e. O /\ -. C e. E ) )
8 df-or 
 |-  ( ( ( C e. O /\ -. C e. O ) \/ ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) <-> ( -. ( C e. O /\ -. C e. O ) -> ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) )
9 pm3.24 
 |-  -. ( C e. O /\ -. C e. O )
10 9 a1bi 
 |-  ( ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) <-> ( -. ( C e. O /\ -. C e. O ) -> ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) )
11 8 10 bitr4i 
 |-  ( ( ( C e. O /\ -. C e. O ) \/ ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) <-> ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
12 1 2 3 4 5 6 ballotleme 
 |-  ( C e. E <-> ( C e. O /\ A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
13 12 notbii 
 |-  ( -. C e. E <-> -. ( C e. O /\ A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
14 13 anbi2i 
 |-  ( ( C e. O /\ -. C e. E ) <-> ( C e. O /\ -. ( C e. O /\ A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) )
15 ianor 
 |-  ( -. ( C e. O /\ A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) <-> ( -. C e. O \/ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
16 15 anbi2i 
 |-  ( ( C e. O /\ -. ( C e. O /\ A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) <-> ( C e. O /\ ( -. C e. O \/ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) )
17 andi 
 |-  ( ( C e. O /\ ( -. C e. O \/ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) <-> ( ( C e. O /\ -. C e. O ) \/ ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) )
18 14 16 17 3bitri 
 |-  ( ( C e. O /\ -. C e. E ) <-> ( ( C e. O /\ -. C e. O ) \/ ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) ) )
19 fz1ssfz0 
 |-  ( 1 ... ( M + N ) ) C_ ( 0 ... ( M + N ) )
20 19 a1i 
 |-  ( C e. O -> ( 1 ... ( M + N ) ) C_ ( 0 ... ( M + N ) ) )
21 20 sseld 
 |-  ( C e. O -> ( i e. ( 1 ... ( M + N ) ) -> i e. ( 0 ... ( M + N ) ) ) )
22 21 imdistani 
 |-  ( ( C e. O /\ i e. ( 1 ... ( M + N ) ) ) -> ( C e. O /\ i e. ( 0 ... ( M + N ) ) ) )
23 simpl 
 |-  ( ( C e. O /\ j e. ( 0 ... ( M + N ) ) ) -> C e. O )
24 elfzelz 
 |-  ( j e. ( 0 ... ( M + N ) ) -> j e. ZZ )
25 24 adantl 
 |-  ( ( C e. O /\ j e. ( 0 ... ( M + N ) ) ) -> j e. ZZ )
26 1 2 3 4 5 23 25 ballotlemfelz 
 |-  ( ( C e. O /\ j e. ( 0 ... ( M + N ) ) ) -> ( ( F ` C ) ` j ) e. ZZ )
27 26 zred 
 |-  ( ( C e. O /\ j e. ( 0 ... ( M + N ) ) ) -> ( ( F ` C ) ` j ) e. RR )
28 27 sbimi 
 |-  ( [ i / j ] ( C e. O /\ j e. ( 0 ... ( M + N ) ) ) -> [ i / j ] ( ( F ` C ) ` j ) e. RR )
29 sban 
 |-  ( [ i / j ] ( C e. O /\ j e. ( 0 ... ( M + N ) ) ) <-> ( [ i / j ] C e. O /\ [ i / j ] j e. ( 0 ... ( M + N ) ) ) )
30 sbv 
 |-  ( [ i / j ] C e. O <-> C e. O )
31 clelsb3 
 |-  ( [ i / j ] j e. ( 0 ... ( M + N ) ) <-> i e. ( 0 ... ( M + N ) ) )
32 30 31 anbi12i 
 |-  ( ( [ i / j ] C e. O /\ [ i / j ] j e. ( 0 ... ( M + N ) ) ) <-> ( C e. O /\ i e. ( 0 ... ( M + N ) ) ) )
33 29 32 bitri 
 |-  ( [ i / j ] ( C e. O /\ j e. ( 0 ... ( M + N ) ) ) <-> ( C e. O /\ i e. ( 0 ... ( M + N ) ) ) )
34 nfv 
 |-  F/ j ( ( F ` C ) ` i ) e. RR
35 fveq2 
 |-  ( j = i -> ( ( F ` C ) ` j ) = ( ( F ` C ) ` i ) )
36 35 eleq1d 
 |-  ( j = i -> ( ( ( F ` C ) ` j ) e. RR <-> ( ( F ` C ) ` i ) e. RR ) )
37 34 36 sbiev 
 |-  ( [ i / j ] ( ( F ` C ) ` j ) e. RR <-> ( ( F ` C ) ` i ) e. RR )
38 28 33 37 3imtr3i 
 |-  ( ( C e. O /\ i e. ( 0 ... ( M + N ) ) ) -> ( ( F ` C ) ` i ) e. RR )
39 22 38 syl 
 |-  ( ( C e. O /\ i e. ( 1 ... ( M + N ) ) ) -> ( ( F ` C ) ` i ) e. RR )
40 0red 
 |-  ( ( C e. O /\ i e. ( 1 ... ( M + N ) ) ) -> 0 e. RR )
41 39 40 lenltd 
 |-  ( ( C e. O /\ i e. ( 1 ... ( M + N ) ) ) -> ( ( ( F ` C ) ` i ) <_ 0 <-> -. 0 < ( ( F ` C ) ` i ) ) )
42 41 rexbidva 
 |-  ( C e. O -> ( E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 0 <-> E. i e. ( 1 ... ( M + N ) ) -. 0 < ( ( F ` C ) ` i ) ) )
43 rexnal 
 |-  ( E. i e. ( 1 ... ( M + N ) ) -. 0 < ( ( F ` C ) ` i ) <-> -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) )
44 42 43 bitrdi 
 |-  ( C e. O -> ( E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 0 <-> -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
45 44 pm5.32i 
 |-  ( ( C e. O /\ E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 0 ) <-> ( C e. O /\ -. A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
46 11 18 45 3bitr4i 
 |-  ( ( C e. O /\ -. C e. E ) <-> ( C e. O /\ E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 0 ) )
47 7 46 bitri 
 |-  ( C e. ( O \ E ) <-> ( C e. O /\ E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 0 ) )