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∈WordV∧N∈1…W→WcyclShiftN⁡W−1=W⁡N−1

Proof

Step Hyp Ref Expression
1 simpl ⊢W∈WordV∧N∈1…W→W∈WordV
2 elfzelz ⊢N∈1…W→N∈ℤ
3 2 adantl ⊢W∈WordV∧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∈WordV∧N∈1…W→W∈ℕ
8 fzo0end ⊢W∈ℕ→W−1∈0..^W
9 7 8 syl ⊢W∈WordV∧N∈1…W→W−1∈0..^W
10 cshwidxmod ⊢W∈WordV∧N∈ℤ∧W−1∈0..^W→WcyclShiftN⁡W−1=W⁡W-1+NmodW
11 1 3 9 10 syl3anc ⊢W∈WordV∧N∈1…W→WcyclShiftN⁡W−1=W⁡W-1+NmodW
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+NmodW=W+N-1modW
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-1modW=N−1
36 34 35 syl ⊢N∈1…W→W+N-1modW=N−1
37 22 36 eqtrd ⊢N∈1…W→W-1+NmodW=N−1
38 37 fveq2d ⊢N∈1…W→W⁡W-1+NmodW=W⁡N−1
39 38 adantl ⊢W∈WordV∧N∈1…W→W⁡W-1+NmodW=W⁡N−1
40 11 39 eqtrd ⊢W∈WordV∧N∈1…W→WcyclShiftN⁡W−1=W⁡N−1