Step |
Hyp |
Ref |
Expression |
1 |
|
crctcshwlkn0lem.s |
|- ( ph -> S e. ( 1 ..^ N ) ) |
2 |
|
crctcshwlkn0lem.q |
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) ) |
3 |
|
crctcshwlkn0lem.h |
|- H = ( F cyclShift S ) |
4 |
|
crctcshwlkn0lem.n |
|- N = ( # ` F ) |
5 |
|
crctcshwlkn0lem.f |
|- ( ph -> F e. Word A ) |
6 |
|
crctcshwlkn0lem.p |
|- ( ph -> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) |
7 |
|
elfzoelz |
|- ( j e. ( 0 ..^ ( N - S ) ) -> j e. ZZ ) |
8 |
7
|
zcnd |
|- ( j e. ( 0 ..^ ( N - S ) ) -> j e. CC ) |
9 |
8
|
adantl |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> j e. CC ) |
10 |
|
elfzoelz |
|- ( S e. ( 1 ..^ N ) -> S e. ZZ ) |
11 |
10
|
zcnd |
|- ( S e. ( 1 ..^ N ) -> S e. CC ) |
12 |
11
|
adantr |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> S e. CC ) |
13 |
|
1cnd |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> 1 e. CC ) |
14 |
9 12 13
|
add32d |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) |
15 |
|
elfzo1 |
|- ( S e. ( 1 ..^ N ) <-> ( S e. NN /\ N e. NN /\ S < N ) ) |
16 |
|
elfzonn0 |
|- ( j e. ( 0 ..^ ( N - S ) ) -> j e. NN0 ) |
17 |
|
nnnn0 |
|- ( S e. NN -> S e. NN0 ) |
18 |
|
nn0addcl |
|- ( ( j e. NN0 /\ S e. NN0 ) -> ( j + S ) e. NN0 ) |
19 |
18
|
ex |
|- ( j e. NN0 -> ( S e. NN0 -> ( j + S ) e. NN0 ) ) |
20 |
16 17 19
|
syl2imc |
|- ( S e. NN -> ( j e. ( 0 ..^ ( N - S ) ) -> ( j + S ) e. NN0 ) ) |
21 |
20
|
3ad2ant1 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j e. ( 0 ..^ ( N - S ) ) -> ( j + S ) e. NN0 ) ) |
22 |
15 21
|
sylbi |
|- ( S e. ( 1 ..^ N ) -> ( j e. ( 0 ..^ ( N - S ) ) -> ( j + S ) e. NN0 ) ) |
23 |
22
|
imp |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. NN0 ) |
24 |
|
fzo0ss1 |
|- ( 1 ..^ N ) C_ ( 0 ..^ N ) |
25 |
24
|
sseli |
|- ( S e. ( 1 ..^ N ) -> S e. ( 0 ..^ N ) ) |
26 |
|
elfzo0 |
|- ( S e. ( 0 ..^ N ) <-> ( S e. NN0 /\ N e. NN /\ S < N ) ) |
27 |
26
|
simp2bi |
|- ( S e. ( 0 ..^ N ) -> N e. NN ) |
28 |
25 27
|
syl |
|- ( S e. ( 1 ..^ N ) -> N e. NN ) |
29 |
28
|
adantr |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> N e. NN ) |
30 |
|
elfzo0 |
|- ( j e. ( 0 ..^ ( N - S ) ) <-> ( j e. NN0 /\ ( N - S ) e. NN /\ j < ( N - S ) ) ) |
31 |
|
nn0re |
|- ( j e. NN0 -> j e. RR ) |
32 |
|
nnre |
|- ( S e. NN -> S e. RR ) |
33 |
|
nnre |
|- ( N e. NN -> N e. RR ) |
34 |
32 33
|
anim12i |
|- ( ( S e. NN /\ N e. NN ) -> ( S e. RR /\ N e. RR ) ) |
35 |
34
|
3adant3 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( S e. RR /\ N e. RR ) ) |
36 |
15 35
|
sylbi |
|- ( S e. ( 1 ..^ N ) -> ( S e. RR /\ N e. RR ) ) |
37 |
31 36
|
anim12i |
|- ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j e. RR /\ ( S e. RR /\ N e. RR ) ) ) |
38 |
|
3anass |
|- ( ( j e. RR /\ S e. RR /\ N e. RR ) <-> ( j e. RR /\ ( S e. RR /\ N e. RR ) ) ) |
39 |
37 38
|
sylibr |
|- ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j e. RR /\ S e. RR /\ N e. RR ) ) |
40 |
|
ltaddsub |
|- ( ( j e. RR /\ S e. RR /\ N e. RR ) -> ( ( j + S ) < N <-> j < ( N - S ) ) ) |
41 |
40
|
bicomd |
|- ( ( j e. RR /\ S e. RR /\ N e. RR ) -> ( j < ( N - S ) <-> ( j + S ) < N ) ) |
42 |
39 41
|
syl |
|- ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j < ( N - S ) <-> ( j + S ) < N ) ) |
43 |
42
|
biimpd |
|- ( ( j e. NN0 /\ S e. ( 1 ..^ N ) ) -> ( j < ( N - S ) -> ( j + S ) < N ) ) |
44 |
43
|
ex |
|- ( j e. NN0 -> ( S e. ( 1 ..^ N ) -> ( j < ( N - S ) -> ( j + S ) < N ) ) ) |
45 |
44
|
com23 |
|- ( j e. NN0 -> ( j < ( N - S ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) ) ) |
46 |
45
|
a1d |
|- ( j e. NN0 -> ( ( N - S ) e. NN -> ( j < ( N - S ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) ) ) ) |
47 |
46
|
3imp |
|- ( ( j e. NN0 /\ ( N - S ) e. NN /\ j < ( N - S ) ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) ) |
48 |
30 47
|
sylbi |
|- ( j e. ( 0 ..^ ( N - S ) ) -> ( S e. ( 1 ..^ N ) -> ( j + S ) < N ) ) |
49 |
48
|
impcom |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) < N ) |
50 |
|
elfzo0 |
|- ( ( j + S ) e. ( 0 ..^ N ) <-> ( ( j + S ) e. NN0 /\ N e. NN /\ ( j + S ) < N ) ) |
51 |
23 29 49 50
|
syl3anbrc |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. ( 0 ..^ N ) ) |
52 |
51
|
adantr |
|- ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( j + S ) e. ( 0 ..^ N ) ) |
53 |
|
fveq2 |
|- ( i = ( j + S ) -> ( P ` i ) = ( P ` ( j + S ) ) ) |
54 |
53
|
adantl |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( P ` i ) = ( P ` ( j + S ) ) ) |
55 |
|
fvoveq1 |
|- ( i = ( j + S ) -> ( P ` ( i + 1 ) ) = ( P ` ( ( j + S ) + 1 ) ) ) |
56 |
|
simpr |
|- ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) |
57 |
56
|
fveq2d |
|- ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( P ` ( ( j + S ) + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) ) |
58 |
55 57
|
sylan9eqr |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( P ` ( i + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) ) |
59 |
54 58
|
eqeq12d |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( ( P ` i ) = ( P ` ( i + 1 ) ) <-> ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) ) ) |
60 |
|
2fveq3 |
|- ( i = ( j + S ) -> ( I ` ( F ` i ) ) = ( I ` ( F ` ( j + S ) ) ) ) |
61 |
53
|
sneqd |
|- ( i = ( j + S ) -> { ( P ` i ) } = { ( P ` ( j + S ) ) } ) |
62 |
60 61
|
eqeq12d |
|- ( i = ( j + S ) -> ( ( I ` ( F ` i ) ) = { ( P ` i ) } <-> ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } ) ) |
63 |
62
|
adantl |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( ( I ` ( F ` i ) ) = { ( P ` i ) } <-> ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } ) ) |
64 |
54 58
|
preq12d |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } ) |
65 |
60
|
adantl |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( I ` ( F ` i ) ) = ( I ` ( F ` ( j + S ) ) ) ) |
66 |
64 65
|
sseq12d |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) <-> { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) |
67 |
59 63 66
|
ifpbi123d |
|- ( ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) /\ i = ( j + S ) ) -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) |
68 |
52 67
|
rspcdv |
|- ( ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) /\ ( ( j + S ) + 1 ) = ( ( j + 1 ) + S ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) |
69 |
14 68
|
mpdan |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) |
70 |
1 69
|
sylan |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) |
71 |
70
|
ex |
|- ( ph -> ( j e. ( 0 ..^ ( N - S ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) ) |
72 |
6 71
|
mpid |
|- ( ph -> ( j e. ( 0 ..^ ( N - S ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) |
73 |
72
|
imp |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) |
74 |
|
elfzofz |
|- ( j e. ( 0 ..^ ( N - S ) ) -> j e. ( 0 ... ( N - S ) ) ) |
75 |
1 2
|
crctcshwlkn0lem2 |
|- ( ( ph /\ j e. ( 0 ... ( N - S ) ) ) -> ( Q ` j ) = ( P ` ( j + S ) ) ) |
76 |
74 75
|
sylan2 |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( Q ` j ) = ( P ` ( j + S ) ) ) |
77 |
|
fzofzp1 |
|- ( j e. ( 0 ..^ ( N - S ) ) -> ( j + 1 ) e. ( 0 ... ( N - S ) ) ) |
78 |
1 2
|
crctcshwlkn0lem2 |
|- ( ( ph /\ ( j + 1 ) e. ( 0 ... ( N - S ) ) ) -> ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) ) |
79 |
77 78
|
sylan2 |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) ) |
80 |
3
|
fveq1i |
|- ( H ` j ) = ( ( F cyclShift S ) ` j ) |
81 |
5
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> F e. Word A ) |
82 |
1 10
|
syl |
|- ( ph -> S e. ZZ ) |
83 |
82
|
adantr |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> S e. ZZ ) |
84 |
|
nnz |
|- ( N e. NN -> N e. ZZ ) |
85 |
84
|
adantl |
|- ( ( S e. NN /\ N e. NN ) -> N e. ZZ ) |
86 |
|
nnz |
|- ( S e. NN -> S e. ZZ ) |
87 |
86
|
adantr |
|- ( ( S e. NN /\ N e. NN ) -> S e. ZZ ) |
88 |
85 87
|
zsubcld |
|- ( ( S e. NN /\ N e. NN ) -> ( N - S ) e. ZZ ) |
89 |
17
|
nn0ge0d |
|- ( S e. NN -> 0 <_ S ) |
90 |
89
|
adantr |
|- ( ( S e. NN /\ N e. NN ) -> 0 <_ S ) |
91 |
|
subge02 |
|- ( ( N e. RR /\ S e. RR ) -> ( 0 <_ S <-> ( N - S ) <_ N ) ) |
92 |
33 32 91
|
syl2anr |
|- ( ( S e. NN /\ N e. NN ) -> ( 0 <_ S <-> ( N - S ) <_ N ) ) |
93 |
90 92
|
mpbid |
|- ( ( S e. NN /\ N e. NN ) -> ( N - S ) <_ N ) |
94 |
88 85 93
|
3jca |
|- ( ( S e. NN /\ N e. NN ) -> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) ) |
95 |
94
|
3adant3 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) ) |
96 |
15 95
|
sylbi |
|- ( S e. ( 1 ..^ N ) -> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) ) |
97 |
|
eluz2 |
|- ( N e. ( ZZ>= ` ( N - S ) ) <-> ( ( N - S ) e. ZZ /\ N e. ZZ /\ ( N - S ) <_ N ) ) |
98 |
96 97
|
sylibr |
|- ( S e. ( 1 ..^ N ) -> N e. ( ZZ>= ` ( N - S ) ) ) |
99 |
|
fzoss2 |
|- ( N e. ( ZZ>= ` ( N - S ) ) -> ( 0 ..^ ( N - S ) ) C_ ( 0 ..^ N ) ) |
100 |
1 98 99
|
3syl |
|- ( ph -> ( 0 ..^ ( N - S ) ) C_ ( 0 ..^ N ) ) |
101 |
100
|
sselda |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> j e. ( 0 ..^ N ) ) |
102 |
4
|
oveq2i |
|- ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) ) |
103 |
101 102
|
eleqtrdi |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> j e. ( 0 ..^ ( # ` F ) ) ) |
104 |
|
cshwidxmod |
|- ( ( F e. Word A /\ S e. ZZ /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) |
105 |
81 83 103 104
|
syl3anc |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( ( j + S ) mod ( # ` F ) ) ) ) |
106 |
4
|
eqcomi |
|- ( # ` F ) = N |
107 |
106
|
oveq2i |
|- ( ( j + S ) mod ( # ` F ) ) = ( ( j + S ) mod N ) |
108 |
21
|
imp |
|- ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. NN0 ) |
109 |
|
nnm1nn0 |
|- ( N e. NN -> ( N - 1 ) e. NN0 ) |
110 |
109
|
3ad2ant2 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - 1 ) e. NN0 ) |
111 |
110
|
adantr |
|- ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( N - 1 ) e. NN0 ) |
112 |
31 35
|
anim12i |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j e. RR /\ ( S e. RR /\ N e. RR ) ) ) |
113 |
112 38
|
sylibr |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j e. RR /\ S e. RR /\ N e. RR ) ) |
114 |
113 41
|
syl |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j < ( N - S ) <-> ( j + S ) < N ) ) |
115 |
17
|
3ad2ant1 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> S e. NN0 ) |
116 |
115 18
|
sylan2 |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j + S ) e. NN0 ) |
117 |
116
|
nn0zd |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j + S ) e. ZZ ) |
118 |
84
|
3ad2ant2 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> N e. ZZ ) |
119 |
118
|
adantl |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> N e. ZZ ) |
120 |
|
zltlem1 |
|- ( ( ( j + S ) e. ZZ /\ N e. ZZ ) -> ( ( j + S ) < N <-> ( j + S ) <_ ( N - 1 ) ) ) |
121 |
117 119 120
|
syl2anc |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( ( j + S ) < N <-> ( j + S ) <_ ( N - 1 ) ) ) |
122 |
121
|
biimpd |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( ( j + S ) < N -> ( j + S ) <_ ( N - 1 ) ) ) |
123 |
114 122
|
sylbid |
|- ( ( j e. NN0 /\ ( S e. NN /\ N e. NN /\ S < N ) ) -> ( j < ( N - S ) -> ( j + S ) <_ ( N - 1 ) ) ) |
124 |
123
|
impancom |
|- ( ( j e. NN0 /\ j < ( N - S ) ) -> ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j + S ) <_ ( N - 1 ) ) ) |
125 |
124
|
3adant2 |
|- ( ( j e. NN0 /\ ( N - S ) e. NN /\ j < ( N - S ) ) -> ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j + S ) <_ ( N - 1 ) ) ) |
126 |
30 125
|
sylbi |
|- ( j e. ( 0 ..^ ( N - S ) ) -> ( ( S e. NN /\ N e. NN /\ S < N ) -> ( j + S ) <_ ( N - 1 ) ) ) |
127 |
126
|
impcom |
|- ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) <_ ( N - 1 ) ) |
128 |
108 111 127
|
3jca |
|- ( ( ( S e. NN /\ N e. NN /\ S < N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( j + S ) <_ ( N - 1 ) ) ) |
129 |
15 128
|
sylanb |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( j + S ) <_ ( N - 1 ) ) ) |
130 |
|
elfz2nn0 |
|- ( ( j + S ) e. ( 0 ... ( N - 1 ) ) <-> ( ( j + S ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( j + S ) <_ ( N - 1 ) ) ) |
131 |
129 130
|
sylibr |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. ( 0 ... ( N - 1 ) ) ) |
132 |
|
zaddcl |
|- ( ( j e. ZZ /\ S e. ZZ ) -> ( j + S ) e. ZZ ) |
133 |
7 10 132
|
syl2anr |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( j + S ) e. ZZ ) |
134 |
|
zmodid2 |
|- ( ( ( j + S ) e. ZZ /\ N e. NN ) -> ( ( ( j + S ) mod N ) = ( j + S ) <-> ( j + S ) e. ( 0 ... ( N - 1 ) ) ) ) |
135 |
133 29 134
|
syl2anc |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( ( j + S ) mod N ) = ( j + S ) <-> ( j + S ) e. ( 0 ... ( N - 1 ) ) ) ) |
136 |
131 135
|
mpbird |
|- ( ( S e. ( 1 ..^ N ) /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) mod N ) = ( j + S ) ) |
137 |
1 136
|
sylan |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) mod N ) = ( j + S ) ) |
138 |
107 137
|
syl5eq |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( j + S ) mod ( # ` F ) ) = ( j + S ) ) |
139 |
138
|
fveq2d |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( F ` ( ( j + S ) mod ( # ` F ) ) ) = ( F ` ( j + S ) ) ) |
140 |
105 139
|
eqtrd |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( ( F cyclShift S ) ` j ) = ( F ` ( j + S ) ) ) |
141 |
80 140
|
syl5eq |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( H ` j ) = ( F ` ( j + S ) ) ) |
142 |
141
|
fveq2d |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) |
143 |
|
simp1 |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( Q ` j ) = ( P ` ( j + S ) ) ) |
144 |
|
simp2 |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) ) |
145 |
143 144
|
eqeq12d |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( ( Q ` j ) = ( Q ` ( j + 1 ) ) <-> ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) ) ) |
146 |
|
simp3 |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) |
147 |
143
|
sneqd |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> { ( Q ` j ) } = { ( P ` ( j + S ) ) } ) |
148 |
146 147
|
eqeq12d |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( ( I ` ( H ` j ) ) = { ( Q ` j ) } <-> ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } ) ) |
149 |
143 144
|
preq12d |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> { ( Q ` j ) , ( Q ` ( j + 1 ) ) } = { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } ) |
150 |
149 146
|
sseq12d |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) <-> { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) |
151 |
145 148 150
|
ifpbi123d |
|- ( ( ( Q ` j ) = ( P ` ( j + S ) ) /\ ( Q ` ( j + 1 ) ) = ( P ` ( ( j + 1 ) + S ) ) /\ ( I ` ( H ` j ) ) = ( I ` ( F ` ( j + S ) ) ) ) -> ( if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) |
152 |
76 79 142 151
|
syl3anc |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> ( if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( P ` ( j + S ) ) = ( P ` ( ( j + 1 ) + S ) ) , ( I ` ( F ` ( j + S ) ) ) = { ( P ` ( j + S ) ) } , { ( P ` ( j + S ) ) , ( P ` ( ( j + 1 ) + S ) ) } C_ ( I ` ( F ` ( j + S ) ) ) ) ) ) |
153 |
73 152
|
mpbird |
|- ( ( ph /\ j e. ( 0 ..^ ( N - S ) ) ) -> if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |
154 |
153
|
ralrimiva |
|- ( ph -> A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |