Metamath Proof Explorer

Theorem cshwidxn

Description: The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) of the original word. (Contributed by AV, 18-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion cshwidxn ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W − 1 = W ⁡ N − 1

Proof

Step Hyp Ref Expression
1 simpl ⊢ W ∈ Word V ∧ N ∈ 1 … W → W ∈ Word V
2 elfzelz ⊢ N ∈ 1 … W → N ∈ ℤ
3 2 adantl ⊢ W ∈ Word V ∧ N ∈ 1 … W → N ∈ ℤ
4 elfz1b ⊢ N ∈ 1 … W ↔ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W
5 simp2 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → W ∈ ℕ
6 4 5 sylbi ⊢ N ∈ 1 … W → W ∈ ℕ
7 6 adantl ⊢ W ∈ Word V ∧ N ∈ 1 … W → W ∈ ℕ
8 fzo0end ⊢ W ∈ ℕ → W − 1 ∈ 0 ..^ W
9 7 8 syl ⊢ W ∈ Word V ∧ N ∈ 1 … W → W − 1 ∈ 0 ..^ W
10 cshwidxmod ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W − 1 ∈ 0 ..^ W → W cyclShift N ⁡ W − 1 = W ⁡ W - 1 + N mod W
11 1 3 9 10 syl3anc ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W − 1 = W ⁡ W - 1 + N mod W
12 nncn ⊢ W ∈ ℕ → W ∈ ℂ
13 12 adantl ⊢ N ∈ ℕ ∧ W ∈ ℕ → W ∈ ℂ
14 1cnd ⊢ N ∈ ℕ ∧ W ∈ ℕ → 1 ∈ ℂ
15 nncn ⊢ N ∈ ℕ → N ∈ ℂ
16 15 adantr ⊢ N ∈ ℕ ∧ W ∈ ℕ → N ∈ ℂ
17 13 14 16 3jca ⊢ N ∈ ℕ ∧ W ∈ ℕ → W ∈ ℂ ∧ 1 ∈ ℂ ∧ N ∈ ℂ
18 17 3adant3 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → W ∈ ℂ ∧ 1 ∈ ℂ ∧ N ∈ ℂ
19 4 18 sylbi ⊢ N ∈ 1 … W → W ∈ ℂ ∧ 1 ∈ ℂ ∧ N ∈ ℂ
20 subadd23 ⊢ W ∈ ℂ ∧ 1 ∈ ℂ ∧ N ∈ ℂ → W - 1 + N = W + N - 1
21 19 20 syl ⊢ N ∈ 1 … W → W - 1 + N = W + N - 1
22 21 oveq1d ⊢ N ∈ 1 … W → W - 1 + N mod W = W + N - 1 mod W
23 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
24 23 3ad2ant1 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → N − 1 ∈ ℕ 0
25 simp3 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → N ≤ W
26 nnz ⊢ N ∈ ℕ → N ∈ ℤ
27 nnz ⊢ W ∈ ℕ → W ∈ ℤ
28 26 27 anim12i ⊢ N ∈ ℕ ∧ W ∈ ℕ → N ∈ ℤ ∧ W ∈ ℤ
29 28 3adant3 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → N ∈ ℤ ∧ W ∈ ℤ
30 zlem1lt ⊢ N ∈ ℤ ∧ W ∈ ℤ → N ≤ W ↔ N − 1 < W
31 29 30 syl ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → N ≤ W ↔ N − 1 < W
32 25 31 mpbid ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → N − 1 < W
33 24 5 32 3jca ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → N − 1 ∈ ℕ 0 ∧ W ∈ ℕ ∧ N − 1 < W
34 4 33 sylbi ⊢ N ∈ 1 … W → N − 1 ∈ ℕ 0 ∧ W ∈ ℕ ∧ N − 1 < W
35 addmodid ⊢ N − 1 ∈ ℕ 0 ∧ W ∈ ℕ ∧ N − 1 < W → W + N - 1 mod W = N − 1
36 34 35 syl ⊢ N ∈ 1 … W → W + N - 1 mod W = N − 1
37 22 36 eqtrd ⊢ N ∈ 1 … W → W - 1 + N mod W = N − 1
38 37 fveq2d ⊢ N ∈ 1 … W → W ⁡ W - 1 + N mod W = W ⁡ N − 1
39 38 adantl ⊢ W ∈ Word V ∧ N ∈ 1 … W → W ⁡ W - 1 + N mod W = W ⁡ N − 1
40 11 39 eqtrd ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W − 1 = W ⁡ N − 1