Metamath Proof Explorer

Theorem cshwidxm1

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

Ref Expression
Assertion cshwidxm1 ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ W - N - 1 = W ⁡ W − 1

Proof

Step Hyp Ref Expression
1 simpl ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W ∈ Word V
2 elfzoelz ⊢ N ∈ 0 ..^ W → N ∈ ℤ
3 2 adantl ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → N ∈ ℤ
4 ubmelm1fzo ⊢ N ∈ 0 ..^ W → W - N - 1 ∈ 0 ..^ W
5 4 adantl ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W - N - 1 ∈ 0 ..^ W
6 cshwidxmod ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W - N - 1 ∈ 0 ..^ W → W cyclShift N ⁡ W - N - 1 = W ⁡ W − N - 1 + N mod W
7 1 3 5 6 syl3anc ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ W - N - 1 = W ⁡ W − N - 1 + N mod W
8 elfzoel2 ⊢ N ∈ 0 ..^ W → W ∈ ℤ
9 8 zcnd ⊢ N ∈ 0 ..^ W → W ∈ ℂ
10 2 zcnd ⊢ N ∈ 0 ..^ W → N ∈ ℂ
11 1cnd ⊢ N ∈ 0 ..^ W → 1 ∈ ℂ
12 nnpcan ⊢ W ∈ ℂ ∧ N ∈ ℂ ∧ 1 ∈ ℂ → W − N - 1 + N = W − 1
13 9 10 11 12 syl3anc ⊢ N ∈ 0 ..^ W → W − N - 1 + N = W − 1
14 13 oveq1d ⊢ N ∈ 0 ..^ W → W − N - 1 + N mod W = W − 1 mod W
15 14 adantl ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W − N - 1 + N mod W = W − 1 mod W
16 elfzo0 ⊢ N ∈ 0 ..^ W ↔ N ∈ ℕ 0 ∧ W ∈ ℕ ∧ N < W
17 nnre ⊢ W ∈ ℕ → W ∈ ℝ
18 peano2rem ⊢ W ∈ ℝ → W − 1 ∈ ℝ
19 17 18 syl ⊢ W ∈ ℕ → W − 1 ∈ ℝ
20 nnrp ⊢ W ∈ ℕ → W ∈ ℝ +
21 19 20 jca ⊢ W ∈ ℕ → W − 1 ∈ ℝ ∧ W ∈ ℝ +
22 21 3ad2ant2 ⊢ N ∈ ℕ 0 ∧ W ∈ ℕ ∧ N < W → W − 1 ∈ ℝ ∧ W ∈ ℝ +
23 16 22 sylbi ⊢ N ∈ 0 ..^ W → W − 1 ∈ ℝ ∧ W ∈ ℝ +
24 nnm1ge0 ⊢ W ∈ ℕ → 0 ≤ W − 1
25 24 3ad2ant2 ⊢ N ∈ ℕ 0 ∧ W ∈ ℕ ∧ N < W → 0 ≤ W − 1
26 16 25 sylbi ⊢ N ∈ 0 ..^ W → 0 ≤ W − 1
27 zre ⊢ W ∈ ℤ → W ∈ ℝ
28 27 ltm1d ⊢ W ∈ ℤ → W − 1 < W
29 8 28 syl ⊢ N ∈ 0 ..^ W → W − 1 < W
30 23 26 29 jca32 ⊢ N ∈ 0 ..^ W → W − 1 ∈ ℝ ∧ W ∈ ℝ + ∧ 0 ≤ W − 1 ∧ W − 1 < W
31 30 adantl ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W − 1 ∈ ℝ ∧ W ∈ ℝ + ∧ 0 ≤ W − 1 ∧ W − 1 < W
32 modid ⊢ W − 1 ∈ ℝ ∧ W ∈ ℝ + ∧ 0 ≤ W − 1 ∧ W − 1 < W → W − 1 mod W = W − 1
33 31 32 syl ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W − 1 mod W = W − 1
34 15 33 eqtrd ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W − N - 1 + N mod W = W − 1
35 34 fveq2d ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W ⁡ W − N - 1 + N mod W = W ⁡ W − 1
36 7 35 eqtrd ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ W - N - 1 = W ⁡ W − 1