Metamath Proof Explorer

Theorem cshwidxmod

Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 13-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 30-Oct-2018) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Assertion cshwidxmod 
|- ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )

Proof

Step Hyp Ref Expression
1 elfzo0 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) <-> ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) )
2 nnne0 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) =/= 0 )
3 eqneqall 
 |-  ( ( # ` W ) = 0 -> ( ( # ` W ) =/= 0 -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
4 2 3 syl5com 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) = 0 -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
5 4 3ad2ant2 
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) -> ( ( # ` W ) = 0 -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
6 1 5 sylbi 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( ( # ` W ) = 0 -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
7 6 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` W ) = 0 -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
8 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
9 elnnne0 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) )
10 simprl 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> N e. ZZ )
11 cshword 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
12 10 11 sylan2 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
13 12 fveq1d 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( W cyclShift N ) ` I ) = ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) )
14 swrdcl 
 |-  ( W e. Word V -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V )
15 14 adantr 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V )
16 pfxcl 
 |-  ( W e. Word V -> ( W prefix ( N mod ( # ` W ) ) ) e. Word V )
17 16 adantr 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( W prefix ( N mod ( # ` W ) ) ) e. Word V )
18 simpl 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> W e. Word V )
19 simpl 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> N e. ZZ )
20 19 anim2i 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( # ` W ) e. NN /\ N e. ZZ ) )
21 20 adantl 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( # ` W ) e. NN /\ N e. ZZ ) )
22 21 ancomd 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( N e. ZZ /\ ( # ` W ) e. NN ) )
23 zmodfzp1 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) )
24 22 23 syl 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) )
25 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
26 8 25 sylib 
 |-  ( W e. Word V -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
27 26 adantr 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
28 swrdlen 
 |-  ( ( W e. Word V /\ ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( N mod ( # ` W ) ) ) )
29 18 24 27 28 syl3anc 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( N mod ( # ` W ) ) ) )
30 20 ancomd 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( N e. ZZ /\ ( # ` W ) e. NN ) )
31 30 23 syl 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) )
32 pfxlen 
 |-  ( ( W e. Word V /\ ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) = ( N mod ( # ` W ) ) )
33 31 32 sylan2 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) = ( N mod ( # ` W ) ) )
34 29 33 oveq12d 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) = ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) )
35 29 34 oveq12d 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ..^ ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) ) = ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) )
36 35 eleq2d 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( I e. ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ..^ ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) ) <-> I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) ) )
37 36 biimparc 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> I e. ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ..^ ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) ) )
38 ccatval2 
 |-  ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V /\ ( W prefix ( N mod ( # ` W ) ) ) e. Word V /\ I e. ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ..^ ( ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) + ( # ` ( W prefix ( N mod ( # ` W ) ) ) ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( ( W prefix ( N mod ( # ` W ) ) ) ` ( I - ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ) ) )
39 15 17 37 38 syl2an23an 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( ( W prefix ( N mod ( # ` W ) ) ) ` ( I - ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ) ) )
40 26 ad2antrl 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
41 18 24 40 28 syl2an23an 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( N mod ( # ` W ) ) ) )
42 41 oveq2d 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( I - ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ) = ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) )
43 42 fveq2d 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( ( W prefix ( N mod ( # ` W ) ) ) ` ( I - ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ) ) = ( ( W prefix ( N mod ( # ` W ) ) ) ` ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) )
44 elfzo2 
 |-  ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) <-> ( I e. ( ZZ>= ` ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) /\ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) e. ZZ /\ I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) )
45 eluz2 
 |-  ( I e. ( ZZ>= ` ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) <-> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) e. ZZ /\ I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) )
46 simpl 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> I e. ZZ )
47 nnz 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. ZZ )
48 47 adantl 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( # ` W ) e. ZZ )
49 zmodcl 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. NN0 )
50 49 nn0zd 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. ZZ )
51 48 50 zsubcld 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( ( # ` W ) - ( N mod ( # ` W ) ) ) e. ZZ )
52 51 adantl 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( ( # ` W ) - ( N mod ( # ` W ) ) ) e. ZZ )
53 46 52 zsubcld 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ZZ )
54 53 adantlr 
 |-  ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ZZ )
55 zre 
 |-  ( I e. ZZ -> I e. RR )
56 nnre 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR )
57 56 adantl 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( # ` W ) e. RR )
58 49 nn0red 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. RR )
59 57 58 resubcld 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( ( # ` W ) - ( N mod ( # ` W ) ) ) e. RR )
60 subge0 
 |-  ( ( I e. RR /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) e. RR ) -> ( 0 <_ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) <-> ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) )
61 55 59 60 syl2an 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( 0 <_ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) <-> ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) )
62 61 exbiri 
 |-  ( I e. ZZ -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I -> 0 <_ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) ) )
63 62 com23 
 |-  ( I e. ZZ -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> 0 <_ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) ) )
64 63 imp31 
 |-  ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> 0 <_ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) )
65 elnn0uz 
 |-  ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. NN0 <-> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( ZZ>= ` 0 ) )
66 elnn0z 
 |-  ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. NN0 <-> ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ZZ /\ 0 <_ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) )
67 65 66 bitr3i 
 |-  ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( ZZ>= ` 0 ) <-> ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ZZ /\ 0 <_ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) )
68 54 64 67 sylanbrc 
 |-  ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( ZZ>= ` 0 ) )
69 68 adantlr 
 |-  ( ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( ZZ>= ` 0 ) )
70 50 adantl 
 |-  ( ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( N mod ( # ` W ) ) e. ZZ )
71 55 adantr 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> I e. RR )
72 59 adantl 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( ( # ` W ) - ( N mod ( # ` W ) ) ) e. RR )
73 58 adantl 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( N mod ( # ` W ) ) e. RR )
74 71 72 73 ltsubadd2d 
 |-  ( ( I e. ZZ /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) < ( N mod ( # ` W ) ) <-> I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) )
75 74 adantlr 
 |-  ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) < ( N mod ( # ` W ) ) <-> I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) )
76 75 exbiri 
 |-  ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) < ( N mod ( # ` W ) ) ) ) )
77 76 com23 
 |-  ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) -> ( I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) < ( N mod ( # ` W ) ) ) ) )
78 77 imp31 
 |-  ( ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) < ( N mod ( # ` W ) ) )
79 elfzo2 
 |-  ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) <-> ( ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( ZZ>= ` 0 ) /\ ( N mod ( # ` W ) ) e. ZZ /\ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) < ( N mod ( # ` W ) ) ) )
80 69 70 78 79 syl3anbrc 
 |-  ( ( ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) /\ I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( N e. ZZ /\ ( # ` W ) e. NN ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) )
81 80 exp31 
 |-  ( ( I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) -> ( I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) ) )
82 81 3adant1 
 |-  ( ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) e. ZZ /\ I e. ZZ /\ ( ( # ` W ) - ( N mod ( # ` W ) ) ) <_ I ) -> ( I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) ) )
83 45 82 sylbi 
 |-  ( I e. ( ZZ>= ` ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) -> ( I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) ) )
84 83 imp 
 |-  ( ( I e. ( ZZ>= ` ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) /\ I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) )
85 84 3adant2 
 |-  ( ( I e. ( ZZ>= ` ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) /\ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) e. ZZ /\ I < ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) )
86 44 85 sylbi 
 |-  ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) )
87 86 expdcom 
 |-  ( N e. ZZ -> ( ( # ` W ) e. NN -> ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) ) )
88 87 adantr 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` W ) e. NN -> ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) ) )
89 88 impcom 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) )
90 89 adantl 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) )
91 90 impcom 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) )
92 pfxfv 
 |-  ( ( W e. Word V /\ ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) /\ ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) e. ( 0 ..^ ( N mod ( # ` W ) ) ) ) -> ( ( W prefix ( N mod ( # ` W ) ) ) ` ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) = ( W ` ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) )
93 18 24 91 92 syl2an23an 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( ( W prefix ( N mod ( # ` W ) ) ) ` ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) = ( W ` ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) )
94 elfzoelz 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. ZZ )
95 94 zcnd 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. CC )
96 95 ad2antll 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> I e. CC )
97 nncn 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. CC )
98 97 adantr 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( # ` W ) e. CC )
99 30 49 syl 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( N mod ( # ` W ) ) e. NN0 )
100 99 nn0cnd 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( N mod ( # ` W ) ) e. CC )
101 96 98 100 subsub3d 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) = ( ( I + ( N mod ( # ` W ) ) ) - ( # ` W ) ) )
102 101 ad2antll 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) = ( ( I + ( N mod ( # ` W ) ) ) - ( # ` W ) ) )
103 30 ad2antll 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( N e. ZZ /\ ( # ` W ) e. NN ) )
104 97 adantl 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( # ` W ) e. CC )
105 49 nn0cnd 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( N mod ( # ` W ) ) e. CC )
106 104 105 npcand 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) = ( # ` W ) )
107 106 ex 
 |-  ( N e. ZZ -> ( ( # ` W ) e. NN -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) = ( # ` W ) ) )
108 107 adantr 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` W ) e. NN -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) = ( # ` W ) ) )
109 108 impcom 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) = ( # ` W ) )
110 109 adantl 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) = ( # ` W ) )
111 110 oveq2d 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) = ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) )
112 111 eleq2d 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) <-> I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) )
113 112 biimpac 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) )
114 modaddmodup 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) -> ( ( I + ( N mod ( # ` W ) ) ) - ( # ` W ) ) = ( ( I + N ) mod ( # ` W ) ) ) )
115 103 113 114 sylc 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( ( I + ( N mod ( # ` W ) ) ) - ( # ` W ) ) = ( ( I + N ) mod ( # ` W ) ) )
116 102 115 eqtrd 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) = ( ( I + N ) mod ( # ` W ) ) )
117 116 fveq2d 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( W ` ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
118 93 117 eqtrd 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( ( W prefix ( N mod ( # ` W ) ) ) ` ( I - ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
119 39 43 118 3eqtrd 
 |-  ( ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) /\ ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
120 119 ex 
 |-  ( I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
121 112 notbid 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) <-> -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) )
122 14 ad2antrr 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V )
123 16 ad2antrr 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( W prefix ( N mod ( # ` W ) ) ) e. Word V )
124 49 ancoms 
 |-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( N mod ( # ` W ) ) e. NN0 )
125 124 nn0zd 
 |-  ( ( ( # ` W ) e. NN /\ N e. ZZ ) -> ( N mod ( # ` W ) ) e. ZZ )
126 125 adantrr 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( N mod ( # ` W ) ) e. ZZ )
127 zre 
 |-  ( N e. ZZ -> N e. RR )
128 127 adantr 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> N e. RR )
129 nnrp 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
130 modlt 
 |-  ( ( N e. RR /\ ( # ` W ) e. RR+ ) -> ( N mod ( # ` W ) ) < ( # ` W ) )
131 128 129 130 syl2anr 
 |-  ( ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( N mod ( # ` W ) ) < ( # ` W ) )
132 simprrr 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> I e. ( 0 ..^ ( # ` W ) ) )
133 fzonfzoufzol 
 |-  ( ( ( N mod ( # ` W ) ) e. ZZ /\ ( N mod ( # ` W ) ) < ( # ` W ) /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) -> I e. ( 0 ..^ ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) )
134 126 131 132 133 syl2an23an 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) -> I e. ( 0 ..^ ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) )
135 134 imp 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> I e. ( 0 ..^ ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) )
136 simpll 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> W e. Word V )
137 24 adantr 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) )
138 26 ad2antrr 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
139 136 137 138 28 syl3anc 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( N mod ( # ` W ) ) ) )
140 139 oveq2d 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( 0 ..^ ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ) = ( 0 ..^ ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) )
141 135 140 eleqtrrd 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> I e. ( 0 ..^ ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ) )
142 ccatval1 
 |-  ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) e. Word V /\ ( W prefix ( N mod ( # ` W ) ) ) e. Word V /\ I e. ( 0 ..^ ( # ` ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ` I ) )
143 122 123 141 142 syl3anc 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ` I ) )
144 swrdfv 
 |-  ( ( ( W e. Word V /\ ( N mod ( # ` W ) ) e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) /\ I e. ( 0 ..^ ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) ) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ` I ) = ( W ` ( I + ( N mod ( # ` W ) ) ) ) )
145 136 137 138 135 144 syl31anc 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ` I ) = ( W ` ( I + ( N mod ( # ` W ) ) ) ) )
146 30 ad2antlr 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( N e. ZZ /\ ( # ` W ) e. NN ) )
147 modaddmodlo 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. NN ) -> ( I e. ( 0 ..^ ( ( # ` W ) - ( N mod ( # ` W ) ) ) ) -> ( I + ( N mod ( # ` W ) ) ) = ( ( I + N ) mod ( # ` W ) ) ) )
148 146 135 147 sylc 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( I + ( N mod ( # ` W ) ) ) = ( ( I + N ) mod ( # ` W ) ) )
149 148 fveq2d 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( W ` ( I + ( N mod ( # ` W ) ) ) ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
150 143 145 149 3eqtrd 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) /\ -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
151 150 ex 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( # ` W ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
152 121 151 sylbid 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
153 152 com12 
 |-  ( -. I e. ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) ..^ ( ( ( # ` W ) - ( N mod ( # ` W ) ) ) + ( N mod ( # ` W ) ) ) ) -> ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
154 120 153 pm2.61i 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
155 13 154 eqtrd 
 |-  ( ( W e. Word V /\ ( ( # ` W ) e. NN /\ ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )
156 155 exp32 
 |-  ( W e. Word V -> ( ( # ` W ) e. NN -> ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) ) )
157 156 com12 
 |-  ( ( # ` W ) e. NN -> ( W e. Word V -> ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) ) )
158 9 157 sylbir 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> ( W e. Word V -> ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) ) )
159 158 ex 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) =/= 0 -> ( W e. Word V -> ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) ) ) )
160 159 com23 
 |-  ( ( # ` W ) e. NN0 -> ( W e. Word V -> ( ( # ` W ) =/= 0 -> ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) ) ) )
161 8 160 mpcom 
 |-  ( W e. Word V -> ( ( # ` W ) =/= 0 -> ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) ) )
162 161 com23 
 |-  ( W e. Word V -> ( ( N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` W ) =/= 0 -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) ) )
163 162 3impib 
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` W ) =/= 0 -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) ) )
164 7 163 pm2.61dne 
 |-  ( ( W e. Word V /\ N e. ZZ /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` I ) = ( W ` ( ( I + N ) mod ( # ` W ) ) ) )