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 |
|
eldifi |
|- ( C e. ( O \ E ) -> C e. O ) |
10 |
9
|
ad2antrr |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> C e. O ) |
11 |
1 2 3 4 5 6 7 8
|
ballotlemiex |
|- ( C e. ( O \ E ) -> ( ( I ` C ) e. ( 1 ... ( M + N ) ) /\ ( ( F ` C ) ` ( I ` C ) ) = 0 ) ) |
12 |
11
|
simpld |
|- ( C e. ( O \ E ) -> ( I ` C ) e. ( 1 ... ( M + N ) ) ) |
13 |
|
elfznn |
|- ( ( I ` C ) e. ( 1 ... ( M + N ) ) -> ( I ` C ) e. NN ) |
14 |
12 13
|
syl |
|- ( C e. ( O \ E ) -> ( I ` C ) e. NN ) |
15 |
14
|
adantr |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) e. NN ) |
16 |
1 2 3 4 5 6 7 8
|
ballotlemi1 |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) =/= 1 ) |
17 |
|
eluz2b3 |
|- ( ( I ` C ) e. ( ZZ>= ` 2 ) <-> ( ( I ` C ) e. NN /\ ( I ` C ) =/= 1 ) ) |
18 |
15 16 17
|
sylanbrc |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) e. ( ZZ>= ` 2 ) ) |
19 |
|
uz2m1nn |
|- ( ( I ` C ) e. ( ZZ>= ` 2 ) -> ( ( I ` C ) - 1 ) e. NN ) |
20 |
18 19
|
syl |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( ( I ` C ) - 1 ) e. NN ) |
21 |
20
|
adantr |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> ( ( I ` C ) - 1 ) e. NN ) |
22 |
|
elnnuz |
|- ( ( ( I ` C ) - 1 ) e. NN <-> ( ( I ` C ) - 1 ) e. ( ZZ>= ` 1 ) ) |
23 |
22
|
biimpi |
|- ( ( ( I ` C ) - 1 ) e. NN -> ( ( I ` C ) - 1 ) e. ( ZZ>= ` 1 ) ) |
24 |
|
eluzfz1 |
|- ( ( ( I ` C ) - 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( ( I ` C ) - 1 ) ) ) |
25 |
20 23 24
|
3syl |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> 1 e. ( 1 ... ( ( I ` C ) - 1 ) ) ) |
26 |
25
|
adantr |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> 1 e. ( 1 ... ( ( I ` C ) - 1 ) ) ) |
27 |
|
1nn |
|- 1 e. NN |
28 |
27
|
a1i |
|- ( C e. ( O \ E ) -> 1 e. NN ) |
29 |
1 2 3 4 5 9 28
|
ballotlemfp1 |
|- ( C e. ( O \ E ) -> ( ( -. 1 e. C -> ( ( F ` C ) ` 1 ) = ( ( ( F ` C ) ` ( 1 - 1 ) ) - 1 ) ) /\ ( 1 e. C -> ( ( F ` C ) ` 1 ) = ( ( ( F ` C ) ` ( 1 - 1 ) ) + 1 ) ) ) ) |
30 |
29
|
simpld |
|- ( C e. ( O \ E ) -> ( -. 1 e. C -> ( ( F ` C ) ` 1 ) = ( ( ( F ` C ) ` ( 1 - 1 ) ) - 1 ) ) ) |
31 |
30
|
imp |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( ( F ` C ) ` 1 ) = ( ( ( F ` C ) ` ( 1 - 1 ) ) - 1 ) ) |
32 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
33 |
32
|
fveq2i |
|- ( ( F ` C ) ` ( 1 - 1 ) ) = ( ( F ` C ) ` 0 ) |
34 |
33
|
oveq1i |
|- ( ( ( F ` C ) ` ( 1 - 1 ) ) - 1 ) = ( ( ( F ` C ) ` 0 ) - 1 ) |
35 |
34
|
a1i |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( ( ( F ` C ) ` ( 1 - 1 ) ) - 1 ) = ( ( ( F ` C ) ` 0 ) - 1 ) ) |
36 |
1 2 3 4 5
|
ballotlemfval0 |
|- ( C e. O -> ( ( F ` C ) ` 0 ) = 0 ) |
37 |
9 36
|
syl |
|- ( C e. ( O \ E ) -> ( ( F ` C ) ` 0 ) = 0 ) |
38 |
37
|
adantr |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( ( F ` C ) ` 0 ) = 0 ) |
39 |
38
|
oveq1d |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( ( ( F ` C ) ` 0 ) - 1 ) = ( 0 - 1 ) ) |
40 |
31 35 39
|
3eqtrrd |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( 0 - 1 ) = ( ( F ` C ) ` 1 ) ) |
41 |
|
0le1 |
|- 0 <_ 1 |
42 |
|
0re |
|- 0 e. RR |
43 |
|
1re |
|- 1 e. RR |
44 |
|
suble0 |
|- ( ( 0 e. RR /\ 1 e. RR ) -> ( ( 0 - 1 ) <_ 0 <-> 0 <_ 1 ) ) |
45 |
42 43 44
|
mp2an |
|- ( ( 0 - 1 ) <_ 0 <-> 0 <_ 1 ) |
46 |
41 45
|
mpbir |
|- ( 0 - 1 ) <_ 0 |
47 |
40 46
|
eqbrtrrdi |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( ( F ` C ) ` 1 ) <_ 0 ) |
48 |
47
|
adantr |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> ( ( F ` C ) ` 1 ) <_ 0 ) |
49 |
|
fveq2 |
|- ( i = 1 -> ( ( F ` C ) ` i ) = ( ( F ` C ) ` 1 ) ) |
50 |
49
|
breq1d |
|- ( i = 1 -> ( ( ( F ` C ) ` i ) <_ 0 <-> ( ( F ` C ) ` 1 ) <_ 0 ) ) |
51 |
50
|
rspcev |
|- ( ( 1 e. ( 1 ... ( ( I ` C ) - 1 ) ) /\ ( ( F ` C ) ` 1 ) <_ 0 ) -> E. i e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` i ) <_ 0 ) |
52 |
26 48 51
|
syl2anc |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> E. i e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` i ) <_ 0 ) |
53 |
|
0lt1 |
|- 0 < 1 |
54 |
|
1p0e1 |
|- ( 1 + 0 ) = 1 |
55 |
1 2 3 4 5 9 14
|
ballotlemfp1 |
|- ( C e. ( O \ E ) -> ( ( -. ( I ` C ) e. C -> ( ( F ` C ) ` ( I ` C ) ) = ( ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) - 1 ) ) /\ ( ( I ` C ) e. C -> ( ( F ` C ) ` ( I ` C ) ) = ( ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) + 1 ) ) ) ) |
56 |
55
|
simpld |
|- ( C e. ( O \ E ) -> ( -. ( I ` C ) e. C -> ( ( F ` C ) ` ( I ` C ) ) = ( ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) - 1 ) ) ) |
57 |
56
|
imp |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( ( F ` C ) ` ( I ` C ) ) = ( ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) - 1 ) ) |
58 |
11
|
simprd |
|- ( C e. ( O \ E ) -> ( ( F ` C ) ` ( I ` C ) ) = 0 ) |
59 |
58
|
adantr |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( ( F ` C ) ` ( I ` C ) ) = 0 ) |
60 |
57 59
|
eqtr3d |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) - 1 ) = 0 ) |
61 |
9
|
adantr |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> C e. O ) |
62 |
14
|
nnzd |
|- ( C e. ( O \ E ) -> ( I ` C ) e. ZZ ) |
63 |
62
|
adantr |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( I ` C ) e. ZZ ) |
64 |
|
1zzd |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> 1 e. ZZ ) |
65 |
63 64
|
zsubcld |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( ( I ` C ) - 1 ) e. ZZ ) |
66 |
1 2 3 4 5 61 65
|
ballotlemfelz |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) e. ZZ ) |
67 |
66
|
zcnd |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) e. CC ) |
68 |
|
1cnd |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> 1 e. CC ) |
69 |
|
0cnd |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> 0 e. CC ) |
70 |
67 68 69
|
subaddd |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( ( ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) - 1 ) = 0 <-> ( 1 + 0 ) = ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) ) ) |
71 |
60 70
|
mpbid |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> ( 1 + 0 ) = ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) ) |
72 |
54 71
|
eqtr3id |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> 1 = ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) ) |
73 |
53 72
|
breqtrid |
|- ( ( C e. ( O \ E ) /\ -. ( I ` C ) e. C ) -> 0 < ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) ) |
74 |
73
|
adantlr |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> 0 < ( ( F ` C ) ` ( ( I ` C ) - 1 ) ) ) |
75 |
1 2 3 4 5 10 21 52 74
|
ballotlemfc0 |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> E. k e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` k ) = 0 ) |
76 |
1 2 3 4 5 6 7 8
|
ballotlemimin |
|- ( C e. ( O \ E ) -> -. E. k e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` k ) = 0 ) |
77 |
76
|
ad2antrr |
|- ( ( ( C e. ( O \ E ) /\ -. 1 e. C ) /\ -. ( I ` C ) e. C ) -> -. E. k e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` k ) = 0 ) |
78 |
75 77
|
condan |
|- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) e. C ) |