# Metamath Proof Explorer

## Theorem cshwshashlem1

Description: If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018) (Revised by AV, 8-Jun-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Hypothesis cshwshash.0 ${⊢}{\phi }\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)$
Assertion 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 {L}\in \left(1..^\left|{W}\right|\right)\right)\to {W}\mathrm{cyclShift}{L}\ne {W}$

### Proof

Step Hyp Ref Expression
1 cshwshash.0 ${⊢}{\phi }\to \left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)$
2 df-ne ${⊢}{W}\left({i}\right)\ne {W}\left(0\right)↔¬{W}\left({i}\right)={W}\left(0\right)$
3 2 rexbii ${⊢}\exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)↔\exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}¬{W}\left({i}\right)={W}\left(0\right)$
4 rexnal ${⊢}\exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}¬{W}\left({i}\right)={W}\left(0\right)↔¬\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
5 3 4 bitri ${⊢}\exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)↔¬\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
6 simpll ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {\phi }$
7 fzo0ss1 ${⊢}\left(1..^\left|{W}\right|\right)\subseteq \left(0..^\left|{W}\right|\right)$
8 fzossfz ${⊢}\left(0..^\left|{W}\right|\right)\subseteq \left(0\dots \left|{W}\right|\right)$
9 7 8 sstri ${⊢}\left(1..^\left|{W}\right|\right)\subseteq \left(0\dots \left|{W}\right|\right)$
10 9 sseli ${⊢}{L}\in \left(1..^\left|{W}\right|\right)\to {L}\in \left(0\dots \left|{W}\right|\right)$
11 10 ad2antlr ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {L}\in \left(0\dots \left|{W}\right|\right)$
12 simpr ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to {W}\mathrm{cyclShift}{L}={W}$
13 simpll ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to {W}\in \mathrm{Word}{V}$
14 simpr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to \left|{W}\right|\in ℙ$
15 14 adantr ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to \left|{W}\right|\in ℙ$
16 elfzelz ${⊢}{L}\in \left(0\dots \left|{W}\right|\right)\to {L}\in ℤ$
17 16 adantl ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to {L}\in ℤ$
18 cshwsidrepswmod0 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\wedge {L}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)$
19 13 15 17 18 syl3anc ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)$
20 19 ex ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to \left({L}\in \left(0\dots \left|{W}\right|\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)\right)$
21 20 3imp ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
22 olc ${⊢}{L}=\left|{W}\right|\to \left({L}=0\vee {L}=\left|{W}\right|\right)$
23 22 a1d ${⊢}{L}=\left|{W}\right|\to \left(\left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\to \left({L}=0\vee {L}=\left|{W}\right|\right)\right)$
24 fzofzim ${⊢}\left({L}\ne \left|{W}\right|\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to {L}\in \left(0..^\left|{W}\right|\right)$
25 zmodidfzoimp ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to {L}\mathrm{mod}\left|{W}\right|={L}$
26 eqtr2 ${⊢}\left({L}\mathrm{mod}\left|{W}\right|={L}\wedge {L}\mathrm{mod}\left|{W}\right|=0\right)\to {L}=0$
27 26 a1d ${⊢}\left({L}\mathrm{mod}\left|{W}\right|={L}\wedge {L}\mathrm{mod}\left|{W}\right|=0\right)\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to {L}=0\right)$
28 27 ex ${⊢}{L}\mathrm{mod}\left|{W}\right|={L}\to \left({L}\mathrm{mod}\left|{W}\right|=0\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to {L}=0\right)\right)$
29 25 28 syl ${⊢}{L}\in \left(0..^\left|{W}\right|\right)\to \left({L}\mathrm{mod}\left|{W}\right|=0\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to {L}=0\right)\right)$
30 24 29 syl ${⊢}\left({L}\ne \left|{W}\right|\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to \left({L}\mathrm{mod}\left|{W}\right|=0\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to {L}=0\right)\right)$
31 30 expcom ${⊢}{L}\in \left(0\dots \left|{W}\right|\right)\to \left({L}\ne \left|{W}\right|\to \left({L}\mathrm{mod}\left|{W}\right|=0\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to {L}=0\right)\right)\right)$
32 31 com24 ${⊢}{L}\in \left(0\dots \left|{W}\right|\right)\to \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to \left({L}\mathrm{mod}\left|{W}\right|=0\to \left({L}\ne \left|{W}\right|\to {L}=0\right)\right)\right)$
33 32 impcom ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\right)\to \left({L}\mathrm{mod}\left|{W}\right|=0\to \left({L}\ne \left|{W}\right|\to {L}=0\right)\right)$
34 33 3adant3 ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}\mathrm{mod}\left|{W}\right|=0\to \left({L}\ne \left|{W}\right|\to {L}=0\right)\right)$
35 34 impcom ${⊢}\left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\to \left({L}\ne \left|{W}\right|\to {L}=0\right)$
36 35 impcom ${⊢}\left({L}\ne \left|{W}\right|\wedge \left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\right)\to {L}=0$
37 36 orcd ${⊢}\left({L}\ne \left|{W}\right|\wedge \left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\right)\to \left({L}=0\vee {L}=\left|{W}\right|\right)$
38 37 ex ${⊢}{L}\ne \left|{W}\right|\to \left(\left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\to \left({L}=0\vee {L}=\left|{W}\right|\right)\right)$
39 23 38 pm2.61ine ${⊢}\left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\to \left({L}=0\vee {L}=\left|{W}\right|\right)$
40 39 orcd ${⊢}\left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\to \left(\left({L}=0\vee {L}=\left|{W}\right|\right)\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
41 df-3or ${⊢}\left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)↔\left(\left({L}=0\vee {L}=\left|{W}\right|\right)\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
42 40 41 sylibr ${⊢}\left({L}\mathrm{mod}\left|{W}\right|=0\wedge \left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
43 42 ex ${⊢}{L}\mathrm{mod}\left|{W}\right|=0\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)$
44 3mix3 ${⊢}{W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\to \left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
45 44 a1d ${⊢}{W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)$
46 43 45 jaoi ${⊢}\left({L}\mathrm{mod}\left|{W}\right|=0\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\right)$
47 21 46 mpcom ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
48 1 47 syl3an1 ${⊢}\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)$
49 3mix1 ${⊢}{L}=0\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
50 49 a1d ${⊢}{L}=0\to \left(\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
51 3mix2 ${⊢}{L}=\left|{W}\right|\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
52 51 a1d ${⊢}{L}=\left|{W}\right|\to \left(\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
53 repswsymballbi ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
54 53 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|\in ℙ\right)\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
55 1 54 syl ${⊢}{\phi }\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
56 55 3ad2ant1 ${⊢}\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|↔\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
57 56 biimpa ${⊢}\left(\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\wedge {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
58 57 3mix3d ${⊢}\left(\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\wedge {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
59 58 expcom ${⊢}{W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\to \left(\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
60 50 52 59 3jaoi ${⊢}\left({L}=0\vee {L}=\left|{W}\right|\vee {W}={W}\left(0\right)\mathrm{repeatS}\left|{W}\right|\right)\to \left(\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\right)$
61 48 60 mpcom ${⊢}\left({\phi }\wedge {L}\in \left(0\dots \left|{W}\right|\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
62 6 11 12 61 syl3anc ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
63 elfzo1 ${⊢}{L}\in \left(1..^\left|{W}\right|\right)↔\left({L}\in ℕ\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)$
64 nnne0 ${⊢}{L}\in ℕ\to {L}\ne 0$
65 df-ne ${⊢}{L}\ne 0↔¬{L}=0$
66 pm2.21 ${⊢}¬{L}=0\to \left({L}=0\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
67 65 66 sylbi ${⊢}{L}\ne 0\to \left({L}=0\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
68 64 67 syl ${⊢}{L}\in ℕ\to \left({L}=0\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
69 68 3ad2ant1 ${⊢}\left({L}\in ℕ\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left({L}=0\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
70 63 69 sylbi ${⊢}{L}\in \left(1..^\left|{W}\right|\right)\to \left({L}=0\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
71 70 ad2antlr ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=0\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
72 71 com12 ${⊢}{L}=0\to \left(\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
73 nnre ${⊢}{L}\in ℕ\to {L}\in ℝ$
74 ltne ${⊢}\left({L}\in ℝ\wedge {L}<\left|{W}\right|\right)\to \left|{W}\right|\ne {L}$
75 73 74 sylan ${⊢}\left({L}\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left|{W}\right|\ne {L}$
76 df-ne ${⊢}\left|{W}\right|\ne {L}↔¬\left|{W}\right|={L}$
77 eqcom ${⊢}{L}=\left|{W}\right|↔\left|{W}\right|={L}$
78 pm2.21 ${⊢}¬\left|{W}\right|={L}\to \left(\left|{W}\right|={L}\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
79 77 78 syl5bi ${⊢}¬\left|{W}\right|={L}\to \left({L}=\left|{W}\right|\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
80 76 79 sylbi ${⊢}\left|{W}\right|\ne {L}\to \left({L}=\left|{W}\right|\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
81 75 80 syl ${⊢}\left({L}\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left({L}=\left|{W}\right|\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
82 81 3adant2 ${⊢}\left({L}\in ℕ\wedge \left|{W}\right|\in ℕ\wedge {L}<\left|{W}\right|\right)\to \left({L}=\left|{W}\right|\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
83 63 82 sylbi ${⊢}{L}\in \left(1..^\left|{W}\right|\right)\to \left({L}=\left|{W}\right|\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
84 83 ad2antlr ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left({L}=\left|{W}\right|\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
85 84 com12 ${⊢}{L}=\left|{W}\right|\to \left(\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
86 ax-1 ${⊢}\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\to \left(\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
87 72 85 86 3jaoi ${⊢}\left({L}=0\vee {L}=\left|{W}\right|\vee \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)\to \left(\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\right)$
88 62 87 mpcom ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)$
89 88 pm2.24d ${⊢}\left(\left({\phi }\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\wedge {W}\mathrm{cyclShift}{L}={W}\right)\to \left(¬\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\right)$
90 89 exp31 ${⊢}{\phi }\to \left({L}\in \left(1..^\left|{W}\right|\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to \left(¬\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\right)\right)\right)$
91 90 com34 ${⊢}{\phi }\to \left({L}\in \left(1..^\left|{W}\right|\right)\to \left(¬\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to {W}\mathrm{cyclShift}{L}\ne {W}\right)\right)\right)$
92 91 com23 ${⊢}{\phi }\to \left(¬\forall {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)={W}\left(0\right)\to \left({L}\in \left(1..^\left|{W}\right|\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to {W}\mathrm{cyclShift}{L}\ne {W}\right)\right)\right)$
93 5 92 syl5bi ${⊢}{\phi }\to \left(\exists {i}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)\ne {W}\left(0\right)\to \left({L}\in \left(1..^\left|{W}\right|\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to {W}\mathrm{cyclShift}{L}\ne {W}\right)\right)\right)$
94 93 3imp ${⊢}\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 {L}\in \left(1..^\left|{W}\right|\right)\right)\to \left({W}\mathrm{cyclShift}{L}={W}\to {W}\mathrm{cyclShift}{L}\ne {W}\right)$
95 94 com12 ${⊢}{W}\mathrm{cyclShift}{L}={W}\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)\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\right)$
96 ax-1 ${⊢}{W}\mathrm{cyclShift}{L}\ne {W}\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)\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\to {W}\mathrm{cyclShift}{L}\ne {W}\right)$
97 95 96 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)\wedge {L}\in \left(1..^\left|{W}\right|\right)\right)\to {W}\mathrm{cyclShift}{L}\ne {W}$