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∈WordV∧N∈ℤ∧I∈0..^W→WcyclShiftN⁡I=W⁡I+NmodW

Proof

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