Metamath Proof Explorer

Theorem ballotlemsima

Description: The image by S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-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 ) ) ) ) )
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 , < ) )
ballotth.s 
|- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )
Assertion ballotlemsima 
|- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) " ( 1 ... J ) ) = ( ( ( S ` C ) ` J ) ... ( I ` C ) ) )

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 ballotth.s 
 |-  S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )
10 imassrn 
 |-  ( ( S ` C ) " ( 1 ... J ) ) C_ ran ( S ` C )
11 1 2 3 4 5 6 7 8 9 ballotlemsf1o 
 |-  ( C e. ( O \ E ) -> ( ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) /\ `' ( S ` C ) = ( S ` C ) ) )
12 11 simpld 
 |-  ( C e. ( O \ E ) -> ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) )
13 f1of 
 |-  ( ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) -> ( S ` C ) : ( 1 ... ( M + N ) ) --> ( 1 ... ( M + N ) ) )
14 frn 
 |-  ( ( S ` C ) : ( 1 ... ( M + N ) ) --> ( 1 ... ( M + N ) ) -> ran ( S ` C ) C_ ( 1 ... ( M + N ) ) )
15 12 13 14 3syl 
 |-  ( C e. ( O \ E ) -> ran ( S ` C ) C_ ( 1 ... ( M + N ) ) )
16 10 15 sstrid 
 |-  ( C e. ( O \ E ) -> ( ( S ` C ) " ( 1 ... J ) ) C_ ( 1 ... ( M + N ) ) )
17 fzssuz 
 |-  ( 1 ... ( M + N ) ) C_ ( ZZ>= ` 1 )
18 uzssz 
 |-  ( ZZ>= ` 1 ) C_ ZZ
19 17 18 sstri 
 |-  ( 1 ... ( M + N ) ) C_ ZZ
20 16 19 sstrdi 
 |-  ( C e. ( O \ E ) -> ( ( S ` C ) " ( 1 ... J ) ) C_ ZZ )
21 20 adantr 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) " ( 1 ... J ) ) C_ ZZ )
22 21 sselda 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ( ( S ` C ) " ( 1 ... J ) ) ) -> k e. ZZ )
23 elfzelz 
 |-  ( k e. ( ( ( S ` C ) ` J ) ... ( I ` C ) ) -> k e. ZZ )
24 23 adantl 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ( ( ( S ` C ) ` J ) ... ( I ` C ) ) ) -> k e. ZZ )
25 f1ofn 
 |-  ( ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) -> ( S ` C ) Fn ( 1 ... ( M + N ) ) )
26 12 25 syl 
 |-  ( C e. ( O \ E ) -> ( S ` C ) Fn ( 1 ... ( M + N ) ) )
27 26 adantr 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( S ` C ) Fn ( 1 ... ( M + N ) ) )
28 1 2 3 4 5 6 7 8 ballotlemiex 
 |-  ( C e. ( O \ E ) -> ( ( I ` C ) e. ( 1 ... ( M + N ) ) /\ ( ( F ` C ) ` ( I ` C ) ) = 0 ) )
29 28 simpld 
 |-  ( C e. ( O \ E ) -> ( I ` C ) e. ( 1 ... ( M + N ) ) )
30 29 adantr 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( I ` C ) e. ( 1 ... ( M + N ) ) )
31 elfzuz3 
 |-  ( ( I ` C ) e. ( 1 ... ( M + N ) ) -> ( M + N ) e. ( ZZ>= ` ( I ` C ) ) )
32 30 31 syl 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( M + N ) e. ( ZZ>= ` ( I ` C ) ) )
33 elfzuz3 
 |-  ( J e. ( 1 ... ( I ` C ) ) -> ( I ` C ) e. ( ZZ>= ` J ) )
34 33 adantl 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( I ` C ) e. ( ZZ>= ` J ) )
35 uztrn 
 |-  ( ( ( M + N ) e. ( ZZ>= ` ( I ` C ) ) /\ ( I ` C ) e. ( ZZ>= ` J ) ) -> ( M + N ) e. ( ZZ>= ` J ) )
36 32 34 35 syl2anc 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( M + N ) e. ( ZZ>= ` J ) )
37 fzss2 
 |-  ( ( M + N ) e. ( ZZ>= ` J ) -> ( 1 ... J ) C_ ( 1 ... ( M + N ) ) )
38 36 37 syl 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( 1 ... J ) C_ ( 1 ... ( M + N ) ) )
39 fvelimab 
 |-  ( ( ( S ` C ) Fn ( 1 ... ( M + N ) ) /\ ( 1 ... J ) C_ ( 1 ... ( M + N ) ) ) -> ( k e. ( ( S ` C ) " ( 1 ... J ) ) <-> E. j e. ( 1 ... J ) ( ( S ` C ) ` j ) = k ) )
40 27 38 39 syl2anc 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( k e. ( ( S ` C ) " ( 1 ... J ) ) <-> E. j e. ( 1 ... J ) ( ( S ` C ) ` j ) = k ) )
41 40 adantr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( k e. ( ( S ` C ) " ( 1 ... J ) ) <-> E. j e. ( 1 ... J ) ( ( S ` C ) ` j ) = k ) )
42 1zzd 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> 1 e. ZZ )
43 1 nnzi 
 |-  M e. ZZ
44 2 nnzi 
 |-  N e. ZZ
45 zaddcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
46 43 44 45 mp2an 
 |-  ( M + N ) e. ZZ
47 46 a1i 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( M + N ) e. ZZ )
48 elfzelz 
 |-  ( J e. ( 1 ... ( I ` C ) ) -> J e. ZZ )
49 48 adantl 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> J e. ZZ )
50 elfzle1 
 |-  ( J e. ( 1 ... ( I ` C ) ) -> 1 <_ J )
51 50 adantl 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> 1 <_ J )
52 49 zred 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> J e. RR )
53 elfzelz 
 |-  ( ( I ` C ) e. ( 1 ... ( M + N ) ) -> ( I ` C ) e. ZZ )
54 29 53 syl 
 |-  ( C e. ( O \ E ) -> ( I ` C ) e. ZZ )
55 54 adantr 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( I ` C ) e. ZZ )
56 55 zred 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( I ` C ) e. RR )
57 47 zred 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( M + N ) e. RR )
58 elfzle2 
 |-  ( J e. ( 1 ... ( I ` C ) ) -> J <_ ( I ` C ) )
59 58 adantl 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> J <_ ( I ` C ) )
60 elfzle2 
 |-  ( ( I ` C ) e. ( 1 ... ( M + N ) ) -> ( I ` C ) <_ ( M + N ) )
61 29 60 syl 
 |-  ( C e. ( O \ E ) -> ( I ` C ) <_ ( M + N ) )
62 61 adantr 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( I ` C ) <_ ( M + N ) )
63 52 56 57 59 62 letrd 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> J <_ ( M + N ) )
64 42 47 49 51 63 elfzd 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> J e. ( 1 ... ( M + N ) ) )
65 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 ) )
66 64 65 syldan 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) ` J ) = if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) )
67 simpr 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> J e. ( 1 ... ( I ` C ) ) )
68 iftrue 
 |-  ( J <_ ( I ` C ) -> if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) = ( ( ( I ` C ) + 1 ) - J ) )
69 67 58 68 3syl 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) = ( ( ( I ` C ) + 1 ) - J ) )
70 66 69 eqtrd 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) ` J ) = ( ( ( I ` C ) + 1 ) - J ) )
71 70 oveq1d 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( ( S ` C ) ` J ) ... ( I ` C ) ) = ( ( ( ( I ` C ) + 1 ) - J ) ... ( I ` C ) ) )
72 71 eleq2d 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( k e. ( ( ( S ` C ) ` J ) ... ( I ` C ) ) <-> k e. ( ( ( ( I ` C ) + 1 ) - J ) ... ( I ` C ) ) ) )
73 72 adantr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( k e. ( ( ( S ` C ) ` J ) ... ( I ` C ) ) <-> k e. ( ( ( ( I ` C ) + 1 ) - J ) ... ( I ` C ) ) ) )
74 54 ad2antrr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( I ` C ) e. ZZ )
75 74 zcnd 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( I ` C ) e. CC )
76 1cnd 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> 1 e. CC )
77 75 76 pncand 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( ( ( I ` C ) + 1 ) - 1 ) = ( I ` C ) )
78 77 oveq2d 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( ( ( ( I ` C ) + 1 ) - J ) ... ( ( ( I ` C ) + 1 ) - 1 ) ) = ( ( ( ( I ` C ) + 1 ) - J ) ... ( I ` C ) ) )
79 78 eleq2d 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( k e. ( ( ( ( I ` C ) + 1 ) - J ) ... ( ( ( I ` C ) + 1 ) - 1 ) ) <-> k e. ( ( ( ( I ` C ) + 1 ) - J ) ... ( I ` C ) ) ) )
80 1zzd 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> 1 e. ZZ )
81 48 ad2antlr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> J e. ZZ )
82 74 peano2zd 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( ( I ` C ) + 1 ) e. ZZ )
83 simpr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> k e. ZZ )
84 fzrev 
 |-  ( ( ( 1 e. ZZ /\ J e. ZZ ) /\ ( ( ( I ` C ) + 1 ) e. ZZ /\ k e. ZZ ) ) -> ( k e. ( ( ( ( I ` C ) + 1 ) - J ) ... ( ( ( I ` C ) + 1 ) - 1 ) ) <-> ( ( ( I ` C ) + 1 ) - k ) e. ( 1 ... J ) ) )
85 80 81 82 83 84 syl22anc 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( k e. ( ( ( ( I ` C ) + 1 ) - J ) ... ( ( ( I ` C ) + 1 ) - 1 ) ) <-> ( ( ( I ` C ) + 1 ) - k ) e. ( 1 ... J ) ) )
86 73 79 85 3bitr2d 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( k e. ( ( ( S ` C ) ` J ) ... ( I ` C ) ) <-> ( ( ( I ` C ) + 1 ) - k ) e. ( 1 ... J ) ) )
87 risset 
 |-  ( ( ( ( I ` C ) + 1 ) - k ) e. ( 1 ... J ) <-> E. j e. ( 1 ... J ) j = ( ( ( I ` C ) + 1 ) - k ) )
88 87 a1i 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( ( ( ( I ` C ) + 1 ) - k ) e. ( 1 ... J ) <-> E. j e. ( 1 ... J ) j = ( ( ( I ` C ) + 1 ) - k ) ) )
89 eqcom 
 |-  ( ( ( ( I ` C ) + 1 ) - k ) = j <-> j = ( ( ( I ` C ) + 1 ) - k ) )
90 54 ad2antrr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> ( I ` C ) e. ZZ )
91 90 adantlr 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> ( I ` C ) e. ZZ )
92 91 zcnd 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> ( I ` C ) e. CC )
93 1cnd 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> 1 e. CC )
94 92 93 addcld 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> ( ( I ` C ) + 1 ) e. CC )
95 simplr 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> k e. ZZ )
96 95 zcnd 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> k e. CC )
97 elfzelz 
 |-  ( j e. ( 1 ... J ) -> j e. ZZ )
98 97 adantl 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> j e. ZZ )
99 98 zcnd 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> j e. CC )
100 subsub23 
 |-  ( ( ( ( I ` C ) + 1 ) e. CC /\ k e. CC /\ j e. CC ) -> ( ( ( ( I ` C ) + 1 ) - k ) = j <-> ( ( ( I ` C ) + 1 ) - j ) = k ) )
101 94 96 99 100 syl3anc 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> ( ( ( ( I ` C ) + 1 ) - k ) = j <-> ( ( ( I ` C ) + 1 ) - j ) = k ) )
102 89 101 bitr3id 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> ( j = ( ( ( I ` C ) + 1 ) - k ) <-> ( ( ( I ` C ) + 1 ) - j ) = k ) )
103 simpll 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> C e. ( O \ E ) )
104 38 sselda 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> j e. ( 1 ... ( M + N ) ) )
105 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 ) )
106 103 104 105 syl2anc 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> ( ( S ` C ) ` j ) = if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) )
107 97 adantl 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> j e. ZZ )
108 107 zred 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> j e. RR )
109 48 ad2antlr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> J e. ZZ )
110 109 zred 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> J e. RR )
111 90 zred 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> ( I ` C ) e. RR )
112 elfzle2 
 |-  ( j e. ( 1 ... J ) -> j <_ J )
113 112 adantl 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> j <_ J )
114 58 ad2antlr 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> J <_ ( I ` C ) )
115 108 110 111 113 114 letrd 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> j <_ ( I ` C ) )
116 iftrue 
 |-  ( j <_ ( I ` C ) -> if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) = ( ( ( I ` C ) + 1 ) - j ) )
117 115 116 syl 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> if ( j <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - j ) , j ) = ( ( ( I ` C ) + 1 ) - j ) )
118 106 117 eqtrd 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> ( ( S ` C ) ` j ) = ( ( ( I ` C ) + 1 ) - j ) )
119 118 eqeq1d 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ j e. ( 1 ... J ) ) -> ( ( ( S ` C ) ` j ) = k <-> ( ( ( I ` C ) + 1 ) - j ) = k ) )
120 119 adantlr 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> ( ( ( S ` C ) ` j ) = k <-> ( ( ( I ` C ) + 1 ) - j ) = k ) )
121 102 120 bitr4d 
 |-  ( ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) /\ j e. ( 1 ... J ) ) -> ( j = ( ( ( I ` C ) + 1 ) - k ) <-> ( ( S ` C ) ` j ) = k ) )
122 121 rexbidva 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( E. j e. ( 1 ... J ) j = ( ( ( I ` C ) + 1 ) - k ) <-> E. j e. ( 1 ... J ) ( ( S ` C ) ` j ) = k ) )
123 86 88 122 3bitrd 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( k e. ( ( ( S ` C ) ` J ) ... ( I ` C ) ) <-> E. j e. ( 1 ... J ) ( ( S ` C ) ` j ) = k ) )
124 41 123 bitr4d 
 |-  ( ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) /\ k e. ZZ ) -> ( k e. ( ( S ` C ) " ( 1 ... J ) ) <-> k e. ( ( ( S ` C ) ` J ) ... ( I ` C ) ) ) )
125 22 24 124 eqrdav 
 |-  ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) " ( 1 ... J ) ) = ( ( ( S ` C ) ` J ) ... ( I ` C ) ) )