Step |
Hyp |
Ref |
Expression |
1 |
|
0csh0 |
|- ( (/) cyclShift I ) = (/) |
2 |
|
repsw0 |
|- ( S e. V -> ( S repeatS 0 ) = (/) ) |
3 |
2
|
oveq1d |
|- ( S e. V -> ( ( S repeatS 0 ) cyclShift I ) = ( (/) cyclShift I ) ) |
4 |
1 3 2
|
3eqtr4a |
|- ( S e. V -> ( ( S repeatS 0 ) cyclShift I ) = ( S repeatS 0 ) ) |
5 |
4
|
3ad2ant1 |
|- ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS 0 ) cyclShift I ) = ( S repeatS 0 ) ) |
6 |
|
oveq2 |
|- ( N = 0 -> ( S repeatS N ) = ( S repeatS 0 ) ) |
7 |
6
|
oveq1d |
|- ( N = 0 -> ( ( S repeatS N ) cyclShift I ) = ( ( S repeatS 0 ) cyclShift I ) ) |
8 |
7 6
|
eqeq12d |
|- ( N = 0 -> ( ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) <-> ( ( S repeatS 0 ) cyclShift I ) = ( S repeatS 0 ) ) ) |
9 |
5 8
|
syl5ibr |
|- ( N = 0 -> ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) ) ) |
10 |
|
idd |
|- ( -. N = 0 -> ( S e. V -> S e. V ) ) |
11 |
|
df-ne |
|- ( N =/= 0 <-> -. N = 0 ) |
12 |
|
elnnne0 |
|- ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) ) |
13 |
12
|
simplbi2com |
|- ( N =/= 0 -> ( N e. NN0 -> N e. NN ) ) |
14 |
11 13
|
sylbir |
|- ( -. N = 0 -> ( N e. NN0 -> N e. NN ) ) |
15 |
|
idd |
|- ( -. N = 0 -> ( I e. ZZ -> I e. ZZ ) ) |
16 |
10 14 15
|
3anim123d |
|- ( -. N = 0 -> ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( S e. V /\ N e. NN /\ I e. ZZ ) ) ) |
17 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
18 |
17
|
anim2i |
|- ( ( S e. V /\ N e. NN ) -> ( S e. V /\ N e. NN0 ) ) |
19 |
|
repsw |
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) e. Word V ) |
20 |
18 19
|
syl |
|- ( ( S e. V /\ N e. NN ) -> ( S repeatS N ) e. Word V ) |
21 |
|
cshword |
|- ( ( ( S repeatS N ) e. Word V /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) ) |
22 |
20 21
|
stoic3 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) ) |
23 |
|
repswlen |
|- ( ( S e. V /\ N e. NN0 ) -> ( # ` ( S repeatS N ) ) = N ) |
24 |
18 23
|
syl |
|- ( ( S e. V /\ N e. NN ) -> ( # ` ( S repeatS N ) ) = N ) |
25 |
24
|
oveq2d |
|- ( ( S e. V /\ N e. NN ) -> ( I mod ( # ` ( S repeatS N ) ) ) = ( I mod N ) ) |
26 |
25 24
|
opeq12d |
|- ( ( S e. V /\ N e. NN ) -> <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. = <. ( I mod N ) , N >. ) |
27 |
26
|
oveq2d |
|- ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) = ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ) |
28 |
25
|
oveq2d |
|- ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) = ( ( S repeatS N ) prefix ( I mod N ) ) ) |
29 |
27 28
|
oveq12d |
|- ( ( S e. V /\ N e. NN ) -> ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) = ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) ) |
30 |
29
|
3adant3 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) = ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) ) |
31 |
18
|
3adant3 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( S e. V /\ N e. NN0 ) ) |
32 |
|
zmodcl |
|- ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. NN0 ) |
33 |
32
|
ancoms |
|- ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) e. NN0 ) |
34 |
17
|
adantr |
|- ( ( N e. NN /\ I e. ZZ ) -> N e. NN0 ) |
35 |
33 34
|
jca |
|- ( ( N e. NN /\ I e. ZZ ) -> ( ( I mod N ) e. NN0 /\ N e. NN0 ) ) |
36 |
35
|
3adant1 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( I mod N ) e. NN0 /\ N e. NN0 ) ) |
37 |
|
nnre |
|- ( N e. NN -> N e. RR ) |
38 |
37
|
leidd |
|- ( N e. NN -> N <_ N ) |
39 |
38
|
3ad2ant2 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> N <_ N ) |
40 |
|
repswswrd |
|- ( ( ( S e. V /\ N e. NN0 ) /\ ( ( I mod N ) e. NN0 /\ N e. NN0 ) /\ N <_ N ) -> ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) = ( S repeatS ( N - ( I mod N ) ) ) ) |
41 |
31 36 39 40
|
syl3anc |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) = ( S repeatS ( N - ( I mod N ) ) ) ) |
42 |
|
simp1 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> S e. V ) |
43 |
17
|
3ad2ant2 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> N e. NN0 ) |
44 |
|
zmodfzp1 |
|- ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. ( 0 ... N ) ) |
45 |
44
|
ancoms |
|- ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) e. ( 0 ... N ) ) |
46 |
45
|
3adant1 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( I mod N ) e. ( 0 ... N ) ) |
47 |
|
repswpfx |
|- ( ( S e. V /\ N e. NN0 /\ ( I mod N ) e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix ( I mod N ) ) = ( S repeatS ( I mod N ) ) ) |
48 |
42 43 46 47
|
syl3anc |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) prefix ( I mod N ) ) = ( S repeatS ( I mod N ) ) ) |
49 |
41 48
|
oveq12d |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) = ( ( S repeatS ( N - ( I mod N ) ) ) ++ ( S repeatS ( I mod N ) ) ) ) |
50 |
32
|
nn0red |
|- ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. RR ) |
51 |
50
|
ancoms |
|- ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) e. RR ) |
52 |
37
|
adantr |
|- ( ( N e. NN /\ I e. ZZ ) -> N e. RR ) |
53 |
|
zre |
|- ( I e. ZZ -> I e. RR ) |
54 |
|
nnrp |
|- ( N e. NN -> N e. RR+ ) |
55 |
|
modlt |
|- ( ( I e. RR /\ N e. RR+ ) -> ( I mod N ) < N ) |
56 |
53 54 55
|
syl2anr |
|- ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) < N ) |
57 |
51 52 56
|
ltled |
|- ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) <_ N ) |
58 |
57
|
3adant1 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( I mod N ) <_ N ) |
59 |
33
|
3adant1 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( I mod N ) e. NN0 ) |
60 |
|
nn0sub |
|- ( ( ( I mod N ) e. NN0 /\ N e. NN0 ) -> ( ( I mod N ) <_ N <-> ( N - ( I mod N ) ) e. NN0 ) ) |
61 |
59 43 60
|
syl2anc |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( I mod N ) <_ N <-> ( N - ( I mod N ) ) e. NN0 ) ) |
62 |
58 61
|
mpbid |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( N - ( I mod N ) ) e. NN0 ) |
63 |
|
repswccat |
|- ( ( S e. V /\ ( N - ( I mod N ) ) e. NN0 /\ ( I mod N ) e. NN0 ) -> ( ( S repeatS ( N - ( I mod N ) ) ) ++ ( S repeatS ( I mod N ) ) ) = ( S repeatS ( ( N - ( I mod N ) ) + ( I mod N ) ) ) ) |
64 |
42 62 59 63
|
syl3anc |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS ( N - ( I mod N ) ) ) ++ ( S repeatS ( I mod N ) ) ) = ( S repeatS ( ( N - ( I mod N ) ) + ( I mod N ) ) ) ) |
65 |
|
nncn |
|- ( N e. NN -> N e. CC ) |
66 |
65
|
adantl |
|- ( ( I e. ZZ /\ N e. NN ) -> N e. CC ) |
67 |
32
|
nn0cnd |
|- ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. CC ) |
68 |
66 67
|
npcand |
|- ( ( I e. ZZ /\ N e. NN ) -> ( ( N - ( I mod N ) ) + ( I mod N ) ) = N ) |
69 |
68
|
ancoms |
|- ( ( N e. NN /\ I e. ZZ ) -> ( ( N - ( I mod N ) ) + ( I mod N ) ) = N ) |
70 |
69
|
3adant1 |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( N - ( I mod N ) ) + ( I mod N ) ) = N ) |
71 |
70
|
oveq2d |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( S repeatS ( ( N - ( I mod N ) ) + ( I mod N ) ) ) = ( S repeatS N ) ) |
72 |
49 64 71
|
3eqtrd |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) = ( S repeatS N ) ) |
73 |
22 30 72
|
3eqtrd |
|- ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) ) |
74 |
16 73
|
syl6 |
|- ( -. N = 0 -> ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) ) ) |
75 |
9 74
|
pm2.61i |
|- ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) ) |