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 ∈ Word V ∧ N ∈ ℤ ∧ I ∈ 0 ..^ W → W cyclShift N ⁡ I = W ⁡ I + N mod W

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