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 |
|
ballotth.s |
|- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) ) |
10 |
1 2 3 4 5 6 7 8 9
|
ballotlemsval |
|- ( C e. ( O \ E ) -> ( S ` C ) = ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) ) |
11 |
1 2 3 4 5 6 7 8 9
|
ballotlemsv |
|- ( ( C e. ( O \ E ) /\ i e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` i ) = if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) |
12 |
1 2 3 4 5 6 7 8 9
|
ballotlemsdom |
|- ( ( C e. ( O \ E ) /\ i e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` i ) e. ( 1 ... ( M + N ) ) ) |
13 |
11 12
|
eqeltrrd |
|- ( ( C e. ( O \ E ) /\ i e. ( 1 ... ( M + N ) ) ) -> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) e. ( 1 ... ( M + N ) ) ) |
14 |
1 2 3 4 5 6 7 8 9
|
ballotlemsv |
|- ( ( C e. ( O \ E ) /\ j e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` j ) = if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) |
15 |
1 2 3 4 5 6 7 8 9
|
ballotlemsdom |
|- ( ( C e. ( O \ E ) /\ j e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` j ) e. ( 1 ... ( M + N ) ) ) |
16 |
14 15
|
eqeltrrd |
|- ( ( C e. ( O \ E ) /\ j e. ( 1 ... ( M + N ) ) ) -> if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) e. ( 1 ... ( M + N ) ) ) |
17 |
|
oveq2 |
|- ( i = ( ( ( I ` C ) + 1 ) - j ) -> ( ( ( I ` C ) + 1 ) - i ) = ( ( ( I ` C ) + 1 ) - ( ( ( I ` C ) + 1 ) - j ) ) ) |
18 |
|
id |
|- ( i = j -> i = j ) |
19 |
|
breq1 |
|- ( i = ( ( ( I ` C ) + 1 ) - j ) -> ( i <_ ( I ` C ) <-> ( ( ( I ` C ) + 1 ) - j ) <_ ( I ` C ) ) ) |
20 |
|
breq1 |
|- ( i = j -> ( i <_ ( I ` C ) <-> j <_ ( I ` C ) ) ) |
21 |
1 2 3 4 5 6 7 8
|
ballotlemiex |
|- ( C e. ( O \ E ) -> ( ( I ` C ) e. ( 1 ... ( M + N ) ) /\ ( ( F ` C ) ` ( I ` C ) ) = 0 ) ) |
22 |
21
|
simpld |
|- ( C e. ( O \ E ) -> ( I ` C ) e. ( 1 ... ( M + N ) ) ) |
23 |
|
elfzelz |
|- ( ( I ` C ) e. ( 1 ... ( M + N ) ) -> ( I ` C ) e. ZZ ) |
24 |
23
|
peano2zd |
|- ( ( I ` C ) e. ( 1 ... ( M + N ) ) -> ( ( I ` C ) + 1 ) e. ZZ ) |
25 |
22 24
|
syl |
|- ( C e. ( O \ E ) -> ( ( I ` C ) + 1 ) e. ZZ ) |
26 |
25
|
zcnd |
|- ( C e. ( O \ E ) -> ( ( I ` C ) + 1 ) e. CC ) |
27 |
26
|
adantr |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( ( I ` C ) + 1 ) e. CC ) |
28 |
|
elfzelz |
|- ( j e. ( 1 ... ( M + N ) ) -> j e. ZZ ) |
29 |
28
|
zcnd |
|- ( j e. ( 1 ... ( M + N ) ) -> j e. CC ) |
30 |
29
|
ad2antll |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> j e. CC ) |
31 |
27 30
|
nncand |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( ( ( I ` C ) + 1 ) - ( ( ( I ` C ) + 1 ) - j ) ) = j ) |
32 |
31
|
eqcomd |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> j = ( ( ( I ` C ) + 1 ) - ( ( ( I ` C ) + 1 ) - j ) ) ) |
33 |
22 23
|
syl |
|- ( C e. ( O \ E ) -> ( I ` C ) e. ZZ ) |
34 |
33
|
adantr |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( I ` C ) e. ZZ ) |
35 |
|
elfznn |
|- ( j e. ( 1 ... ( M + N ) ) -> j e. NN ) |
36 |
35
|
ad2antll |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> j e. NN ) |
37 |
34 36
|
ltesubnnd |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( ( ( I ` C ) + 1 ) - j ) <_ ( I ` C ) ) |
38 |
37
|
adantr |
|- ( ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) /\ j <_ ( I ` C ) ) -> ( ( ( I ` C ) + 1 ) - j ) <_ ( I ` C ) ) |
39 |
|
vex |
|- j e. _V |
40 |
39
|
a1i |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> j e. _V ) |
41 |
|
ovexd |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( ( ( I ` C ) + 1 ) - j ) e. _V ) |
42 |
17 18 19 20 32 38 40 41
|
ifeqeqx |
|- ( ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) /\ i = if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) -> j = if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) |
43 |
|
oveq2 |
|- ( j = ( ( ( I ` C ) + 1 ) - i ) -> ( ( ( I ` C ) + 1 ) - j ) = ( ( ( I ` C ) + 1 ) - ( ( ( I ` C ) + 1 ) - i ) ) ) |
44 |
|
id |
|- ( j = i -> j = i ) |
45 |
|
breq1 |
|- ( j = ( ( ( I ` C ) + 1 ) - i ) -> ( j <_ ( I ` C ) <-> ( ( ( I ` C ) + 1 ) - i ) <_ ( I ` C ) ) ) |
46 |
|
breq1 |
|- ( j = i -> ( j <_ ( I ` C ) <-> i <_ ( I ` C ) ) ) |
47 |
|
elfzelz |
|- ( i e. ( 1 ... ( M + N ) ) -> i e. ZZ ) |
48 |
47
|
zcnd |
|- ( i e. ( 1 ... ( M + N ) ) -> i e. CC ) |
49 |
48
|
ad2antrl |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> i e. CC ) |
50 |
27 49
|
nncand |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( ( ( I ` C ) + 1 ) - ( ( ( I ` C ) + 1 ) - i ) ) = i ) |
51 |
50
|
eqcomd |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> i = ( ( ( I ` C ) + 1 ) - ( ( ( I ` C ) + 1 ) - i ) ) ) |
52 |
34
|
adantr |
|- ( ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) /\ i <_ ( I ` C ) ) -> ( I ` C ) e. ZZ ) |
53 |
|
simplrl |
|- ( ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) /\ i <_ ( I ` C ) ) -> i e. ( 1 ... ( M + N ) ) ) |
54 |
|
elfznn |
|- ( i e. ( 1 ... ( M + N ) ) -> i e. NN ) |
55 |
53 54
|
syl |
|- ( ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) /\ i <_ ( I ` C ) ) -> i e. NN ) |
56 |
52 55
|
ltesubnnd |
|- ( ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) /\ i <_ ( I ` C ) ) -> ( ( ( I ` C ) + 1 ) - i ) <_ ( I ` C ) ) |
57 |
|
vex |
|- i e. _V |
58 |
57
|
a1i |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> i e. _V ) |
59 |
|
ovexd |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( ( ( I ` C ) + 1 ) - i ) e. _V ) |
60 |
43 44 45 46 51 56 58 59
|
ifeqeqx |
|- ( ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) /\ j = if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) -> i = if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) |
61 |
42 60
|
impbida |
|- ( ( C e. ( O \ E ) /\ ( i e. ( 1 ... ( M + N ) ) /\ j e. ( 1 ... ( M + N ) ) ) ) -> ( i = if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) <-> j = if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) ) |
62 |
10 13 16 61
|
f1o3d |
|- ( C e. ( O \ E ) -> ( ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) /\ `' ( S ` C ) = ( j e. ( 1 ... ( M + N ) ) |-> if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) ) ) |
63 |
62
|
simpld |
|- ( C e. ( O \ E ) -> ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) ) |
64 |
|
oveq2 |
|- ( i = j -> ( ( ( I ` C ) + 1 ) - i ) = ( ( ( I ` C ) + 1 ) - j ) ) |
65 |
20 64 18
|
ifbieq12d |
|- ( i = j -> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) = if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) |
66 |
65
|
cbvmptv |
|- ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) = ( j e. ( 1 ... ( M + N ) ) |-> if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) |
67 |
66
|
a1i |
|- ( C e. ( O \ E ) -> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) = ( j e. ( 1 ... ( M + N ) ) |-> if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) ) |
68 |
62
|
simprd |
|- ( C e. ( O \ E ) -> `' ( S ` C ) = ( j e. ( 1 ... ( M + N ) ) |-> if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) ) ) |
69 |
67 10 68
|
3eqtr4rd |
|- ( C e. ( O \ E ) -> `' ( S ` C ) = ( S ` C ) ) |
70 |
63 69
|
jca |
|- ( C e. ( O \ E ) -> ( ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) /\ `' ( S ` C ) = ( S ` C ) ) ) |