# 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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{N}\right)\left(\left|{W}\right|-{N}\right)={W}\left(0\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to {W}\in \mathrm{Word}{V}$
2 elfzelz ${⊢}{N}\in \left(1\dots \left|{W}\right|\right)\to {N}\in ℤ$
3 2 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to {N}\in ℤ$
4 ubmelfzo ${⊢}{N}\in \left(1\dots \left|{W}\right|\right)\to \left|{W}\right|-{N}\in \left(0..^\left|{W}\right|\right)$
5 4 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to \left|{W}\right|-{N}\in \left(0..^\left|{W}\right|\right)$
6 cshwidxmod ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\wedge \left|{W}\right|-{N}\in \left(0..^\left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{N}\right)\left(\left|{W}\right|-{N}\right)={W}\left(\left(\left|{W}\right|-{N}+{N}\right)\mathrm{mod}\left|{W}\right|\right)$
7 1 3 5 6 syl3anc ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{N}\right)\left(\left|{W}\right|-{N}\right)={W}\left(\left(\left|{W}\right|-{N}+{N}\right)\mathrm{mod}\left|{W}\right|\right)$
8 elfz1b ${⊢}{N}\in \left(1\dots \left|{W}\right|\right)↔\left({N}\in ℕ\wedge \left|{W}\right|\in ℕ\wedge {N}\le \left|{W}\right|\right)$
9 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
10 nncn ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\in ℂ$
11 9 10 anim12ci ${⊢}\left({N}\in ℕ\wedge \left|{W}\right|\in ℕ\right)\to \left(\left|{W}\right|\in ℂ\wedge {N}\in ℂ\right)$
12 11 3adant3 ${⊢}\left({N}\in ℕ\wedge \left|{W}\right|\in ℕ\wedge {N}\le \left|{W}\right|\right)\to \left(\left|{W}\right|\in ℂ\wedge {N}\in ℂ\right)$
13 8 12 sylbi ${⊢}{N}\in \left(1\dots \left|{W}\right|\right)\to \left(\left|{W}\right|\in ℂ\wedge {N}\in ℂ\right)$
14 npcan ${⊢}\left(\left|{W}\right|\in ℂ\wedge {N}\in ℂ\right)\to \left|{W}\right|-{N}+{N}=\left|{W}\right|$
15 13 14 syl ${⊢}{N}\in \left(1\dots \left|{W}\right|\right)\to \left|{W}\right|-{N}+{N}=\left|{W}\right|$
16 15 oveq1d ${⊢}{N}\in \left(1\dots \left|{W}\right|\right)\to \left(\left|{W}\right|-{N}+{N}\right)\mathrm{mod}\left|{W}\right|=\left|{W}\right|\mathrm{mod}\left|{W}\right|$
17 16 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to \left(\left|{W}\right|-{N}+{N}\right)\mathrm{mod}\left|{W}\right|=\left|{W}\right|\mathrm{mod}\left|{W}\right|$
18 nnrp ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\in {ℝ}^{+}$
19 modid0 ${⊢}\left|{W}\right|\in {ℝ}^{+}\to \left|{W}\right|\mathrm{mod}\left|{W}\right|=0$
20 18 19 syl ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\mathrm{mod}\left|{W}\right|=0$
21 20 3ad2ant2 ${⊢}\left({N}\in ℕ\wedge \left|{W}\right|\in ℕ\wedge {N}\le \left|{W}\right|\right)\to \left|{W}\right|\mathrm{mod}\left|{W}\right|=0$
22 8 21 sylbi ${⊢}{N}\in \left(1\dots \left|{W}\right|\right)\to \left|{W}\right|\mathrm{mod}\left|{W}\right|=0$
23 22 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to \left|{W}\right|\mathrm{mod}\left|{W}\right|=0$
24 17 23 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to \left(\left|{W}\right|-{N}+{N}\right)\mathrm{mod}\left|{W}\right|=0$
25 24 fveq2d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to {W}\left(\left(\left|{W}\right|-{N}+{N}\right)\mathrm{mod}\left|{W}\right|\right)={W}\left(0\right)$
26 7 25 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in \left(1\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{N}\right)\left(\left|{W}\right|-{N}\right)={W}\left(0\right)$