# Metamath Proof Explorer

## Theorem cshwshashlem2

Description: If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018) (Revised by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Hypothesis cshwshash.0 ${⊢}{\phi }\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)$
Assertion cshwshashlem2 ${⊢}\left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\to \left(\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\mathrm{cyclShift}{K}\right)$

### Proof

Step Hyp Ref Expression
1 cshwshash.0 ${⊢}{\phi }\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)$
2 oveq1 ${⊢}{W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\to \left({W}\mathrm{cyclShift}{L}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)=\left({W}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)$
3 2 eqcomd ${⊢}{W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\to \left({W}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)=\left({W}\mathrm{cyclShift}{L}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)$
4 3 ad2antrr ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to \left({W}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)=\left({W}\mathrm{cyclShift}{L}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)$
5 1 simpld ${⊢}{\phi }\to {W}\in \mathrm{Word}{V}$
6 5 adantr ${⊢}\left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\to {W}\in \mathrm{Word}{V}$
7 6 adantl ${⊢}\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\to {W}\in \mathrm{Word}{V}$
8 7 adantr ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {W}\in \mathrm{Word}{V}$
9 elfzofz ${⊢}{K}\in \left(0..^\left|{W}\right|\right)\to {K}\in \left(0\dots \left|{W}\right|\right)$
10 9 3ad2ant2 ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {K}\in \left(0\dots \left|{W}\right|\right)$
11 10 adantl ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {K}\in \left(0\dots \left|{W}\right|\right)$
12 elfzofz ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to {L}\in \left(0\dots \left|{W}\right|\right)$
13 fznn0sub2 ${⊢}{L}\in \left(0\dots \left|{W}\right|\right)\to \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)$
14 12 13 syl ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)$
15 14 3ad2ant1 ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)$
16 15 adantl ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)$
17 elfzo0 ${⊢}{L}\in \left(0..^\left|{W}\right|\right)↔\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)$
18 zre ${⊢}{K}\in ℤ\to {K}\in ℝ$
19 18 adantr ${⊢}\left({K}\in ℤ\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\right)\to {K}\in ℝ$
20 nnre ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\in ℝ$
21 nn0re ${⊢}{L}\in {ℕ}_{0}\to {L}\in ℝ$
22 resubcl ${⊢}\left(\left|{W}\right|\in ℝ\wedge {L}\in ℝ\right)\to \left|{W}\right|-{L}\in ℝ$
23 20 21 22 syl2anr ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\to \left|{W}\right|-{L}\in ℝ$
24 23 adantl ${⊢}\left({K}\in ℤ\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\right)\to \left|{W}\right|-{L}\in ℝ$
25 19 24 readdcld ${⊢}\left({K}\in ℤ\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\right)\to {K}+\left|{W}\right|-{L}\in ℝ$
26 20 adantl ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\to \left|{W}\right|\in ℝ$
27 26 adantl ${⊢}\left({K}\in ℤ\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\right)\to \left|{W}\right|\in ℝ$
28 25 27 jca ${⊢}\left({K}\in ℤ\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\right)\to \left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)$
29 28 ex ${⊢}{K}\in ℤ\to \left(\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\to \left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)\right)$
30 elfzoelz ${⊢}{K}\in \left(0..^\left|{W}\right|\right)\to {K}\in ℤ$
31 29 30 syl11 ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\to \left({K}\in \left(0..^\left|{W}\right|\right)\to \left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)\right)$
32 31 3adant3 ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left({K}\in \left(0..^\left|{W}\right|\right)\to \left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)\right)$
33 17 32 sylbi ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to \left({K}\in \left(0..^\left|{W}\right|\right)\to \left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)\right)$
34 33 imp ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\right)\to \left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)$
35 34 3adant3 ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to \left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)$
36 fzonmapblen ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {K}+\left|{W}\right|-{L}<\left|{W}\right|$
37 ltle ${⊢}\left({K}+\left|{W}\right|-{L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)\to \left({K}+\left|{W}\right|-{L}<\left|{W}\right|\to {K}+\left|{W}\right|-{L}\le \left|{W}\right|\right)$
38 35 36 37 sylc ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {K}+\left|{W}\right|-{L}\le \left|{W}\right|$
39 38 adantl ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {K}+\left|{W}\right|-{L}\le \left|{W}\right|$
40 simpl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({K}\in \left(0\dots \left|{W}\right|\right)\wedge \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)\wedge {K}+\left|{W}\right|-{L}\le \left|{W}\right|\right)\right)\to {W}\in \mathrm{Word}{V}$
41 elfzelz ${⊢}{K}\in \left(0\dots \left|{W}\right|\right)\to {K}\in ℤ$
42 41 3ad2ant1 ${⊢}\left({K}\in \left(0\dots \left|{W}\right|\right)\wedge \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)\wedge {K}+\left|{W}\right|-{L}\le \left|{W}\right|\right)\to {K}\in ℤ$
43 42 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({K}\in \left(0\dots \left|{W}\right|\right)\wedge \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)\wedge {K}+\left|{W}\right|-{L}\le \left|{W}\right|\right)\right)\to {K}\in ℤ$
44 elfzelz ${⊢}\left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)\to \left|{W}\right|-{L}\in ℤ$
45 44 3ad2ant2 ${⊢}\left({K}\in \left(0\dots \left|{W}\right|\right)\wedge \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)\wedge {K}+\left|{W}\right|-{L}\le \left|{W}\right|\right)\to \left|{W}\right|-{L}\in ℤ$
46 45 adantl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({K}\in \left(0\dots \left|{W}\right|\right)\wedge \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)\wedge {K}+\left|{W}\right|-{L}\le \left|{W}\right|\right)\right)\to \left|{W}\right|-{L}\in ℤ$
47 2cshw ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {K}\in ℤ\wedge \left|{W}\right|-{L}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)={W}\mathrm{cyclShift}\left({K}+\left|{W}\right|-{L}\right)$
48 40 43 46 47 syl3anc ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left({K}\in \left(0\dots \left|{W}\right|\right)\wedge \left|{W}\right|-{L}\in \left(0\dots \left|{W}\right|\right)\wedge {K}+\left|{W}\right|-{L}\le \left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)={W}\mathrm{cyclShift}\left({K}+\left|{W}\right|-{L}\right)$
49 8 11 16 39 48 syl13anc ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to \left({W}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)={W}\mathrm{cyclShift}\left({K}+\left|{W}\right|-{L}\right)$
50 12 3ad2ant1 ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {L}\in \left(0\dots \left|{W}\right|\right)$
51 elfzelz ${⊢}{L}\in \left(0\dots \left|{W}\right|\right)\to {L}\in ℤ$
52 2cshwid ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {L}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{L}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)={W}$
53 51 52 sylan2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{L}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)={W}$
54 7 50 53 syl2an ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to \left({W}\mathrm{cyclShift}{L}\right)\mathrm{cyclShift}\left(\left|{W}\right|-{L}\right)={W}$
55 4 49 54 3eqtr3d ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {W}\mathrm{cyclShift}\left({K}+\left|{W}\right|-{L}\right)={W}$
56 simplrl ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {\phi }$
57 simplrr ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)$
58 3simpa ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)$
59 17 58 sylbi ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)$
60 nnz ${⊢}\left|{W}\right|\in ℕ\to \left|{W}\right|\in ℤ$
61 nn0z ${⊢}{L}\in {ℕ}_{0}\to {L}\in ℤ$
62 zsubcl ${⊢}\left(\left|{W}\right|\in ℤ\wedge {L}\in ℤ\right)\to \left|{W}\right|-{L}\in ℤ$
63 60 61 62 syl2anr ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\to \left|{W}\right|-{L}\in ℤ$
64 63 anim1ci ${⊢}\left(\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\wedge {K}\in ℤ\right)\to \left({K}\in ℤ\wedge \left|{W}\right|-{L}\in ℤ\right)$
65 zaddcl ${⊢}\left({K}\in ℤ\wedge \left|{W}\right|-{L}\in ℤ\right)\to {K}+\left|{W}\right|-{L}\in ℤ$
66 64 65 syl ${⊢}\left(\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\wedge {K}\in ℤ\right)\to {K}+\left|{W}\right|-{L}\in ℤ$
67 59 30 66 syl2an ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\right)\to {K}+\left|{W}\right|-{L}\in ℤ$
68 67 3adant3 ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {K}+\left|{W}\right|-{L}\in ℤ$
69 elfzo0 ${⊢}{K}\in \left(0..^\left|{W}\right|\right)↔\left({K}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {K}<\left|{W}\right|\right)$
70 elnn0z ${⊢}{K}\in {ℕ}_{0}↔\left({K}\in ℤ\wedge 0\le {K}\right)$
71 18 ad2antrr ${⊢}\left(\left({K}\in ℤ\wedge 0\le {K}\right)\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\right)\to {K}\in ℝ$
72 23 3adant3 ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left|{W}\right|-{L}\in ℝ$
73 72 adantl ${⊢}\left(\left({K}\in ℤ\wedge 0\le {K}\right)\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\right)\to \left|{W}\right|-{L}\in ℝ$
74 simplr ${⊢}\left(\left({K}\in ℤ\wedge 0\le {K}\right)\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\right)\to 0\le {K}$
75 posdif ${⊢}\left({L}\in ℝ\wedge \left|{W}\right|\in ℝ\right)\to \left({L}<\left|{W}\right|↔0<\left|{W}\right|-{L}\right)$
76 21 20 75 syl2an ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\right)\to \left({L}<\left|{W}\right|↔0<\left|{W}\right|-{L}\right)$
77 76 biimp3a ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to 0<\left|{W}\right|-{L}$
78 77 adantl ${⊢}\left(\left({K}\in ℤ\wedge 0\le {K}\right)\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\right)\to 0<\left|{W}\right|-{L}$
79 71 73 74 78 addgegt0d ${⊢}\left(\left({K}\in ℤ\wedge 0\le {K}\right)\wedge \left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\right)\to 0<{K}+\left|{W}\right|-{L}$
80 79 ex ${⊢}\left({K}\in ℤ\wedge 0\le {K}\right)\to \left(\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to 0<{K}+\left|{W}\right|-{L}\right)$
81 70 80 sylbi ${⊢}{K}\in {ℕ}_{0}\to \left(\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to 0<{K}+\left|{W}\right|-{L}\right)$
82 81 3ad2ant1 ${⊢}\left({K}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {K}<\left|{W}\right|\right)\to \left(\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to 0<{K}+\left|{W}\right|-{L}\right)$
83 69 82 sylbi ${⊢}{K}\in \left(0..^\left|{W}\right|\right)\to \left(\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to 0<{K}+\left|{W}\right|-{L}\right)$
84 83 com12 ${⊢}\left({L}\in {ℕ}_{0}\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left({K}\in \left(0..^\left|{W}\right|\right)\to 0<{K}+\left|{W}\right|-{L}\right)$
85 17 84 sylbi ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to \left({K}\in \left(0..^\left|{W}\right|\right)\to 0<{K}+\left|{W}\right|-{L}\right)$
86 85 imp ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\right)\to 0<{K}+\left|{W}\right|-{L}$
87 86 3adant3 ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to 0<{K}+\left|{W}\right|-{L}$
88 elnnz ${⊢}{K}+\left|{W}\right|-{L}\in ℕ↔\left({K}+\left|{W}\right|-{L}\in ℤ\wedge 0<{K}+\left|{W}\right|-{L}\right)$
89 68 87 88 sylanbrc ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {K}+\left|{W}\right|-{L}\in ℕ$
90 17 simp2bi ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to \left|{W}\right|\in ℕ$
91 90 3ad2ant1 ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to \left|{W}\right|\in ℕ$
92 elfzo1 ${⊢}{K}+\left|{W}\right|-{L}\in \left(1..^\left|{W}\right|\right)↔\left({K}+\left|{W}\right|-{L}\in ℕ\wedge \left|{W}\right|\in ℕ\wedge {K}+\left|{W}\right|-{L}<\left|{W}\right|\right)$
93 89 91 36 92 syl3anbrc ${⊢}\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {K}+\left|{W}\right|-{L}\in \left(1..^\left|{W}\right|\right)$
94 93 adantl ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {K}+\left|{W}\right|-{L}\in \left(1..^\left|{W}\right|\right)$
95 1 cshwshashlem1 ${⊢}\left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\wedge {K}+\left|{W}\right|-{L}\in \left(1..^\left|{W}\right|\right)\right)\to {W}\mathrm{cyclShift}\left({K}+\left|{W}\right|-{L}\right)\ne {W}$
96 56 57 94 95 syl3anc ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {W}\mathrm{cyclShift}\left({K}+\left|{W}\right|-{L}\right)\ne {W}$
97 55 96 pm2.21ddne ${⊢}\left(\left({W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\wedge \left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\right)\wedge \left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\mathrm{cyclShift}{K}$
98 97 exp31 ${⊢}{W}\mathrm{cyclShift}{L}={W}\mathrm{cyclShift}{K}\to \left(\left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\to \left(\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\mathrm{cyclShift}{K}\right)\right)$
99 2a1 ${⊢}{W}\mathrm{cyclShift}{L}\ne {W}\mathrm{cyclShift}{K}\to \left(\left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\to \left(\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\mathrm{cyclShift}{K}\right)\right)$
100 98 99 pm2.61ine ${⊢}\left({\phi }\wedge \exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\right)\to \left(\left({L}\in \left(0..^\left|{W}\right|\right)\wedge {K}\in \left(0..^\left|{W}\right|\right)\wedge {K}<{L}\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\mathrm{cyclShift}{K}\right)$