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

Proof

Step Hyp Ref Expression
1 simpl ⊢W∈WordV∧N∈0..^W→W∈WordV
2 elfzoelz ⊢N∈0..^W→N∈ℤ
3 2 adantl ⊢W∈WordV∧N∈0..^W→N∈ℤ
4 ubmelm1fzo ⊢N∈0..^W→W-N-1∈0..^W
5 4 adantl ⊢W∈WordV∧N∈0..^W→W-N-1∈0..^W
6 cshwidxmod ⊢W∈WordV∧N∈ℤ∧W-N-1∈0..^W→WcyclShiftN⁡W-N-1=W⁡W−N-1+NmodW
7 1 3 5 6 syl3anc ⊢W∈WordV∧N∈0..^W→WcyclShiftN⁡W-N-1=W⁡W−N-1+NmodW
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+NmodW=W−1modW
15 14 adantl ⊢W∈WordV∧N∈0..^W→W−N-1+NmodW=W−1modW
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∈WordV∧N∈0..^W→W−1∈ℝ∧W∈ℝ+∧0≤W−1∧W−1<W
32 modid ⊢W−1∈ℝ∧W∈ℝ+∧0≤W−1∧W−1<W→W−1modW=W−1
33 31 32 syl ⊢W∈WordV∧N∈0..^W→W−1modW=W−1
34 15 33 eqtrd ⊢W∈WordV∧N∈0..^W→W−N-1+NmodW=W−1
35 34 fveq2d ⊢W∈WordV∧N∈0..^W→W⁡W−N-1+NmodW=W⁡W−1
36 7 35 eqtrd ⊢W∈WordV∧N∈0..^W→WcyclShiftN⁡W-N-1=W⁡W−1