Metamath Proof Explorer

Theorem cshwidxm

Description: The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 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 cshwidxm ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W − N = W ⁡ 0

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 ubmelfzo ⊢ N ∈ 1 … W → W − N ∈ 0 ..^ W
5 4 adantl ⊢ W ∈ Word V ∧ N ∈ 1 … W → W − N ∈ 0 ..^ W
6 cshwidxmod ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W − N ∈ 0 ..^ W → W cyclShift N ⁡ W − N = W ⁡ W - N + N mod W
7 1 3 5 6 syl3anc ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W − N = W ⁡ W - N + N mod W
8 elfz1b ⊢ N ∈ 1 … W ↔ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W
9 nncn ⊢ N ∈ ℕ → N ∈ ℂ
10 nncn ⊢ W ∈ ℕ → W ∈ ℂ
11 9 10 anim12ci ⊢ N ∈ ℕ ∧ W ∈ ℕ → W ∈ ℂ ∧ N ∈ ℂ
12 11 3adant3 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → W ∈ ℂ ∧ N ∈ ℂ
13 8 12 sylbi ⊢ N ∈ 1 … W → W ∈ ℂ ∧ N ∈ ℂ
14 npcan ⊢ W ∈ ℂ ∧ N ∈ ℂ → W - N + N = W
15 13 14 syl ⊢ N ∈ 1 … W → W - N + N = W
16 15 oveq1d ⊢ N ∈ 1 … W → W - N + N mod W = W mod W
17 16 adantl ⊢ W ∈ Word V ∧ N ∈ 1 … W → W - N + N mod W = W mod W
18 nnrp ⊢ W ∈ ℕ → W ∈ ℝ +
19 modid0 ⊢ W ∈ ℝ + → W mod W = 0
20 18 19 syl ⊢ W ∈ ℕ → W mod W = 0
21 20 3ad2ant2 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N ≤ W → W mod W = 0
22 8 21 sylbi ⊢ N ∈ 1 … W → W mod W = 0
23 22 adantl ⊢ W ∈ Word V ∧ N ∈ 1 … W → W mod W = 0
24 17 23 eqtrd ⊢ W ∈ Word V ∧ N ∈ 1 … W → W - N + N mod W = 0
25 24 fveq2d ⊢ W ∈ Word V ∧ N ∈ 1 … W → W ⁡ W - N + N mod W = W ⁡ 0
26 7 25 eqtrd ⊢ W ∈ Word V ∧ N ∈ 1 … W → W cyclShift N ⁡ W − N = W ⁡ 0